Metamath Proof Explorer


Theorem expgt1

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

Ref Expression
Assertion expgt1 A N 1 < A 1 < A N

Proof

Step Hyp Ref Expression
1 1re 1
2 1 a1i A N 1 < A 1
3 simp1 A N 1 < A A
4 simp2 A N 1 < A N
5 4 nnnn0d A N 1 < A N 0
6 reexpcl A N 0 A N
7 3 5 6 syl2anc A N 1 < A A N
8 simp3 A N 1 < A 1 < A
9 nnm1nn0 N N 1 0
10 4 9 syl A N 1 < A N 1 0
11 ltle 1 A 1 < A 1 A
12 1 3 11 sylancr A N 1 < A 1 < A 1 A
13 8 12 mpd A N 1 < A 1 A
14 expge1 A N 1 0 1 A 1 A N 1
15 3 10 13 14 syl3anc A N 1 < A 1 A N 1
16 reexpcl A N 1 0 A N 1
17 3 10 16 syl2anc A N 1 < A A N 1
18 0red A N 1 < A 0
19 0lt1 0 < 1
20 19 a1i A N 1 < A 0 < 1
21 18 2 3 20 8 lttrd A N 1 < A 0 < A
22 lemul1 1 A N 1 A 0 < A 1 A N 1 1 A A N 1 A
23 2 17 3 21 22 syl112anc A N 1 < A 1 A N 1 1 A A N 1 A
24 15 23 mpbid A N 1 < A 1 A A N 1 A
25 recn A A
26 25 3ad2ant1 A N 1 < A A
27 26 mulid2d A N 1 < A 1 A = A
28 27 eqcomd A N 1 < A A = 1 A
29 expm1t A N A N = A N 1 A
30 26 4 29 syl2anc A N 1 < A A N = A N 1 A
31 24 28 30 3brtr4d A N 1 < A A A N
32 2 3 7 8 31 ltletrd A N 1 < A 1 < A N