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 N 0 1 A 1 A N

Proof

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