| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = 𝑀 → (𝐴↑𝑗) = (𝐴↑𝑀)) |
| 2 | 1 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑀))) |
| 3 | 2 | imbi2d 340 |
. . . . . 6
⊢ (𝑗 = 𝑀 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ≤ (𝐴↑𝑀)))) |
| 4 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
| 5 | 4 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑘) ≤ (𝐴↑𝑀))) |
| 6 | 5 | imbi2d 340 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑘) ≤ (𝐴↑𝑀)))) |
| 7 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
| 8 | 7 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
| 9 | 8 | imbi2d 340 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀)))) |
| 10 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
| 11 | 10 | breq1d 5153 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
| 12 | 11 | imbi2d 340 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
| 13 | | reexpcl 14119 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) ∈
ℝ) |
| 14 | 13 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ∈ ℝ) |
| 15 | 14 | leidd 11829 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ≤ (𝐴↑𝑀)) |
| 16 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ∈ ℝ) |
| 17 | | 1red 11262 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 1 ∈
ℝ) |
| 18 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑀 ∈
ℕ0) |
| 19 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 20 | | eluznn0 12959 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
| 21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑘 ∈ ℕ0) |
| 22 | | reexpcl 14119 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℝ) |
| 23 | 16, 21, 22 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) ∈ ℝ) |
| 24 | | simprrl 781 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 0 ≤ 𝐴) |
| 25 | | expge0 14139 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0
∧ 0 ≤ 𝐴) → 0
≤ (𝐴↑𝑘)) |
| 26 | 16, 21, 24, 25 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 0 ≤ (𝐴↑𝑘)) |
| 27 | | simprrr 782 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ≤ 1) |
| 28 | 16, 17, 23, 26, 27 | lemul2ad 12208 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐴↑𝑘) · 1)) |
| 29 | 16 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ∈ ℂ) |
| 30 | | expp1 14109 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
| 31 | 29, 21, 30 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
| 32 | 23 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) ∈ ℂ) |
| 33 | 32 | mulridd 11278 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) · 1) = (𝐴↑𝑘)) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) = ((𝐴↑𝑘) · 1)) |
| 35 | 28, 31, 34 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘)) |
| 36 | | peano2nn0 12566 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
| 37 | 21, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝑘 + 1) ∈
ℕ0) |
| 38 | | reexpcl 14119 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐴↑(𝑘 + 1)) ∈ ℝ) |
| 39 | 16, 37, 38 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) ∈ ℝ) |
| 40 | 13 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑀) ∈ ℝ) |
| 41 | | letr 11355 |
. . . . . . . . . 10
⊢ (((𝐴↑(𝑘 + 1)) ∈ ℝ ∧ (𝐴↑𝑘) ∈ ℝ ∧ (𝐴↑𝑀) ∈ ℝ) → (((𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘) ∧ (𝐴↑𝑘) ≤ (𝐴↑𝑀)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
| 42 | 39, 23, 40, 41 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (((𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘) ∧ (𝐴↑𝑘) ≤ (𝐴↑𝑀)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
| 43 | 35, 42 | mpand 695 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) ≤ (𝐴↑𝑀) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
| 44 | 43 | ex 412 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → ((𝐴↑𝑘) ≤ (𝐴↑𝑀) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀)))) |
| 45 | 44 | a2d 29 |
. . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑘) ≤ (𝐴↑𝑀)) → (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀)))) |
| 46 | 3, 6, 9, 12, 15, 45 | uzind4i 12952 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
| 47 | 46 | expd 415 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → ((0 ≤
𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
| 48 | 47 | com12 32 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
(ℤ≥‘𝑀) → ((0 ≤ 𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
| 49 | 48 | 3impia 1118 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑀)) → ((0 ≤ 𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
| 50 | 49 | imp 406 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) |