Proof of Theorem ltexp2a
Step | Hyp | Ref
| Expression |
1 | | simpl1 1190 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝐴 ∈ ℝ) |
2 | | 0red 10978 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 0 ∈ ℝ) |
3 | | 1red 10976 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 1 ∈ ℝ) |
4 | | 0lt1 11497 |
. . . . . . . . 9
⊢ 0 <
1 |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 0 < 1) |
6 | | simprl 768 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 1 < 𝐴) |
7 | 2, 3, 1, 5, 6 | lttrd 11136 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 0 < 𝐴) |
8 | 1, 7 | elrpd 12769 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝐴 ∈
ℝ+) |
9 | | simpl2 1191 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝑀 ∈ ℤ) |
10 | | rpexpcl 13801 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑀 ∈ ℤ)
→ (𝐴↑𝑀) ∈
ℝ+) |
11 | 8, 9, 10 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) ∈
ℝ+) |
12 | 11 | rpred 12772 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) ∈ ℝ) |
13 | 12 | recnd 11003 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) ∈ ℂ) |
14 | 13 | mulid2d 10993 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (1 · (𝐴↑𝑀)) = (𝐴↑𝑀)) |
15 | | simprr 770 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝑀 < 𝑁) |
16 | | simpl3 1192 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝑁 ∈ ℤ) |
17 | | znnsub 12366 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
18 | 9, 16, 17 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ)) |
19 | 15, 18 | mpbid 231 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝑁 − 𝑀) ∈ ℕ) |
20 | | expgt1 13821 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (𝑁 − 𝑀) ∈ ℕ ∧ 1 < 𝐴) → 1 < (𝐴↑(𝑁 − 𝑀))) |
21 | 1, 19, 6, 20 | syl3anc 1370 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 1 < (𝐴↑(𝑁 − 𝑀))) |
22 | 1 | recnd 11003 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝐴 ∈ ℂ) |
23 | 7 | gt0ne0d 11539 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 𝐴 ≠ 0) |
24 | | expsub 13831 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝐴↑(𝑁 − 𝑀)) = ((𝐴↑𝑁) / (𝐴↑𝑀))) |
25 | 22, 23, 16, 9, 24 | syl22anc 836 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑(𝑁 − 𝑀)) = ((𝐴↑𝑁) / (𝐴↑𝑀))) |
26 | 21, 25 | breqtrd 5100 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → 1 < ((𝐴↑𝑁) / (𝐴↑𝑀))) |
27 | | rpexpcl 13801 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈ ℤ)
→ (𝐴↑𝑁) ∈
ℝ+) |
28 | 8, 16, 27 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑁) ∈
ℝ+) |
29 | 28 | rpred 12772 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑁) ∈ ℝ) |
30 | 3, 29, 11 | ltmuldivd 12819 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → ((1 · (𝐴↑𝑀)) < (𝐴↑𝑁) ↔ 1 < ((𝐴↑𝑁) / (𝐴↑𝑀)))) |
31 | 26, 30 | mpbird 256 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (1 · (𝐴↑𝑀)) < (𝐴↑𝑁)) |
32 | 14, 31 | eqbrtrrd 5098 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 <
𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁)) |