Step | Hyp | Ref
| Expression |
1 | | oveq2 7285 |
. . . . . . . 8
⊢ (𝑗 = 𝑀 → (𝐴↑𝑗) = (𝐴↑𝑀)) |
2 | 1 | breq1d 5086 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑀))) |
3 | 2 | imbi2d 341 |
. . . . . 6
⊢ (𝑗 = 𝑀 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ≤ (𝐴↑𝑀)))) |
4 | | oveq2 7285 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
5 | 4 | breq1d 5086 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑘) ≤ (𝐴↑𝑀))) |
6 | 5 | imbi2d 341 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑘) ≤ (𝐴↑𝑀)))) |
7 | | oveq2 7285 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
8 | 7 | breq1d 5086 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
9 | 8 | imbi2d 341 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀)))) |
10 | | oveq2 7285 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
11 | 10 | breq1d 5086 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → ((𝐴↑𝑗) ≤ (𝐴↑𝑀) ↔ (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
12 | 11 | imbi2d 341 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑗) ≤ (𝐴↑𝑀)) ↔ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
13 | | reexpcl 13797 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝐴↑𝑀) ∈
ℝ) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ∈ ℝ) |
15 | 14 | leidd 11539 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑀) ≤ (𝐴↑𝑀)) |
16 | | simprll 776 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ∈ ℝ) |
17 | | 1red 10974 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 1 ∈
ℝ) |
18 | | simprlr 777 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑀 ∈
ℕ0) |
19 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑘 ∈ (ℤ≥‘𝑀)) |
20 | | eluznn0 12655 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
21 | 18, 19, 20 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝑘 ∈ ℕ0) |
22 | | reexpcl 13797 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℝ) |
23 | 16, 21, 22 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) ∈ ℝ) |
24 | | simprrl 778 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 0 ≤ 𝐴) |
25 | | expge0 13817 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0
∧ 0 ≤ 𝐴) → 0
≤ (𝐴↑𝑘)) |
26 | 16, 21, 24, 25 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 0 ≤ (𝐴↑𝑘)) |
27 | | simprrr 779 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ≤ 1) |
28 | 16, 17, 23, 26, 27 | lemul2ad 11913 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) · 𝐴) ≤ ((𝐴↑𝑘) · 1)) |
29 | 16 | recnd 11001 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → 𝐴 ∈ ℂ) |
30 | | expp1 13787 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
31 | 29, 21, 30 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
32 | 23 | recnd 11001 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) ∈ ℂ) |
33 | 32 | mulid1d 10990 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) · 1) = (𝐴↑𝑘)) |
34 | 33 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑘) = ((𝐴↑𝑘) · 1)) |
35 | 28, 31, 34 | 3brtr4d 5108 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘)) |
36 | | peano2nn0 12271 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝑘 + 1) ∈
ℕ0) |
38 | | reexpcl 13797 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝑘 + 1) ∈
ℕ0) → (𝐴↑(𝑘 + 1)) ∈ ℝ) |
39 | 16, 37, 38 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑(𝑘 + 1)) ∈ ℝ) |
40 | 13 | ad2antrl 725 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (𝐴↑𝑀) ∈ ℝ) |
41 | | letr 11067 |
. . . . . . . . . 10
⊢ (((𝐴↑(𝑘 + 1)) ∈ ℝ ∧ (𝐴↑𝑘) ∈ ℝ ∧ (𝐴↑𝑀) ∈ ℝ) → (((𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘) ∧ (𝐴↑𝑘) ≤ (𝐴↑𝑀)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
42 | 39, 23, 40, 41 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → (((𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑘) ∧ (𝐴↑𝑘) ≤ (𝐴↑𝑀)) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
43 | 35, 42 | mpand 692 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1))) → ((𝐴↑𝑘) ≤ (𝐴↑𝑀) → (𝐴↑(𝑘 + 1)) ≤ (𝐴↑𝑀))) |
44 | 43 | ex 413 |
. . . . . . 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 12648 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
47 | 46 | expd 416 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → ((0 ≤
𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
48 | 47 | com12 32 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
(ℤ≥‘𝑀) → ((0 ≤ 𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)))) |
49 | 48 | 3impia 1116 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑀)) → ((0 ≤ 𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑𝑁) ≤ (𝐴↑𝑀))) |
50 | 49 | imp 407 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) |