Metamath Proof Explorer


Theorem exple1

Description: A real between 0 and 1 inclusive raised to a nonnegative integer power is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Assertion exple1 A0AA1N0AN1

Proof

Step Hyp Ref Expression
1 simpl1 A0AA1N0A
2 0nn0 00
3 2 a1i A0AA1N000
4 simpr A0AA1N0N0
5 nn0uz 0=0
6 4 5 eleqtrdi A0AA1N0N0
7 simpl2 A0AA1N00A
8 simpl3 A0AA1N0A1
9 leexp2r A00N00AA1ANA0
10 1 3 6 7 8 9 syl32anc A0AA1N0ANA0
11 1 recnd A0AA1N0A
12 exp0 AA0=1
13 11 12 syl A0AA1N0A0=1
14 10 13 breqtrd A0AA1N0AN1