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