Metamath Proof Explorer

Theorem expge1

Description: A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by NM, 21-Feb-2005) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expge1 
|- ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( z = A -> ( 1 <_ z <-> 1 <_ A ) )
2 1 elrab 
 |-  ( A e. { z e. RR | 1 <_ z } <-> ( A e. RR /\ 1 <_ A ) )
3 ssrab2 
 |-  { z e. RR | 1 <_ z } C_ RR
4 ax-resscn 
 |-  RR C_ CC
5 3 4 sstri 
 |-  { z e. RR | 1 <_ z } C_ CC
6 breq2 
 |-  ( z = x -> ( 1 <_ z <-> 1 <_ x ) )
7 6 elrab 
 |-  ( x e. { z e. RR | 1 <_ z } <-> ( x e. RR /\ 1 <_ x ) )
8 breq2 
 |-  ( z = y -> ( 1 <_ z <-> 1 <_ y ) )
9 8 elrab 
 |-  ( y e. { z e. RR | 1 <_ z } <-> ( y e. RR /\ 1 <_ y ) )
10 breq2 
 |-  ( z = ( x x. y ) -> ( 1 <_ z <-> 1 <_ ( x x. y ) ) )
11 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
12 11 ad2ant2r 
 |-  ( ( ( x e. RR /\ 1 <_ x ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( x x. y ) e. RR )
13 1t1e1 
 |-  ( 1 x. 1 ) = 1
14 1re 
 |-  1 e. RR
15 0le1 
 |-  0 <_ 1
16 14 15 pm3.2i 
 |-  ( 1 e. RR /\ 0 <_ 1 )
17 16 jctl 
 |-  ( x e. RR -> ( ( 1 e. RR /\ 0 <_ 1 ) /\ x e. RR ) )
18 16 jctl 
 |-  ( y e. RR -> ( ( 1 e. RR /\ 0 <_ 1 ) /\ y e. RR ) )
19 lemul12a 
 |-  ( ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ x e. RR ) /\ ( ( 1 e. RR /\ 0 <_ 1 ) /\ y e. RR ) ) -> ( ( 1 <_ x /\ 1 <_ y ) -> ( 1 x. 1 ) <_ ( x x. y ) ) )
20 17 18 19 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( 1 <_ x /\ 1 <_ y ) -> ( 1 x. 1 ) <_ ( x x. y ) ) )
21 20 imp 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( 1 <_ x /\ 1 <_ y ) ) -> ( 1 x. 1 ) <_ ( x x. y ) )
22 13 21 eqbrtrrid 
 |-  ( ( ( x e. RR /\ y e. RR ) /\ ( 1 <_ x /\ 1 <_ y ) ) -> 1 <_ ( x x. y ) )
23 22 an4s 
 |-  ( ( ( x e. RR /\ 1 <_ x ) /\ ( y e. RR /\ 1 <_ y ) ) -> 1 <_ ( x x. y ) )
24 10 12 23 elrabd 
 |-  ( ( ( x e. RR /\ 1 <_ x ) /\ ( y e. RR /\ 1 <_ y ) ) -> ( x x. y ) e. { z e. RR | 1 <_ z } )
25 7 9 24 syl2anb 
 |-  ( ( x e. { z e. RR | 1 <_ z } /\ y e. { z e. RR | 1 <_ z } ) -> ( x x. y ) e. { z e. RR | 1 <_ z } )
26 1le1 
 |-  1 <_ 1
27 breq2 
 |-  ( z = 1 -> ( 1 <_ z <-> 1 <_ 1 ) )
28 27 elrab 
 |-  ( 1 e. { z e. RR | 1 <_ z } <-> ( 1 e. RR /\ 1 <_ 1 ) )
29 14 26 28 mpbir2an 
 |-  1 e. { z e. RR | 1 <_ z }
30 5 25 29 expcllem 
 |-  ( ( A e. { z e. RR | 1 <_ z } /\ N e. NN0 ) -> ( A ^ N ) e. { z e. RR | 1 <_ z } )
31 2 30 sylanbr 
 |-  ( ( ( A e. RR /\ 1 <_ A ) /\ N e. NN0 ) -> ( A ^ N ) e. { z e. RR | 1 <_ z } )
32 31 3impa 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. NN0 ) -> ( A ^ N ) e. { z e. RR | 1 <_ z } )
33 32 3com23 
 |-  ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> ( A ^ N ) e. { z e. RR | 1 <_ z } )
34 breq2 
 |-  ( z = ( A ^ N ) -> ( 1 <_ z <-> 1 <_ ( A ^ N ) ) )
35 34 elrab 
 |-  ( ( A ^ N ) e. { z e. RR | 1 <_ z } <-> ( ( A ^ N ) e. RR /\ 1 <_ ( A ^ N ) ) )
36 35 simprbi 
 |-  ( ( A ^ N ) e. { z e. RR | 1 <_ z } -> 1 <_ ( A ^ N ) )
37 33 36 syl 
 |-  ( ( A e. RR /\ N e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ N ) )