Step | Hyp | Ref
| Expression |
1 | | oveq2 5463 |
. . . . . . . 8
⊢ (𝑗 = 𝑀 → (A↑𝑗) = (A↑𝑀)) |
2 | 1 | breq1d 3765 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → ((A↑𝑗) ≤ (A↑𝑀) ↔ (A↑𝑀) ≤ (A↑𝑀))) |
3 | 2 | imbi2d 219 |
. . . . . 6
⊢ (𝑗 = 𝑀 → ((((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑗) ≤ (A↑𝑀)) ↔ (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑀) ≤ (A↑𝑀)))) |
4 | | oveq2 5463 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (A↑𝑗) = (A↑𝑘)) |
5 | 4 | breq1d 3765 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((A↑𝑗) ≤ (A↑𝑀) ↔ (A↑𝑘) ≤ (A↑𝑀))) |
6 | 5 | imbi2d 219 |
. . . . . 6
⊢ (𝑗 = 𝑘 → ((((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑗) ≤ (A↑𝑀)) ↔ (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑘) ≤ (A↑𝑀)))) |
7 | | oveq2 5463 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 + 1) → (A↑𝑗) = (A↑(𝑘 + 1))) |
8 | 7 | breq1d 3765 |
. . . . . . 7
⊢ (𝑗 = (𝑘 + 1) → ((A↑𝑗) ≤ (A↑𝑀) ↔ (A↑(𝑘 + 1)) ≤ (A↑𝑀))) |
9 | 8 | imbi2d 219 |
. . . . . 6
⊢ (𝑗 = (𝑘 + 1) → ((((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑗) ≤ (A↑𝑀)) ↔ (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑(𝑘 + 1)) ≤ (A↑𝑀)))) |
10 | | oveq2 5463 |
. . . . . . . 8
⊢ (𝑗 = 𝑁 → (A↑𝑗) = (A↑𝑁)) |
11 | 10 | breq1d 3765 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → ((A↑𝑗) ≤ (A↑𝑀) ↔ (A↑𝑁) ≤ (A↑𝑀))) |
12 | 11 | imbi2d 219 |
. . . . . 6
⊢ (𝑗 = 𝑁 → ((((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑗) ≤ (A↑𝑀)) ↔ (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑁) ≤ (A↑𝑀)))) |
13 | | reexpcl 8926 |
. . . . . . . . 9
⊢
((A ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (A↑𝑀) ∈
ℝ) |
14 | 13 | adantr 261 |
. . . . . . . 8
⊢
(((A ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤ A
∧ A ≤
1)) → (A↑𝑀) ∈
ℝ) |
15 | 14 | leidd 7301 |
. . . . . . 7
⊢
(((A ∈ ℝ ∧ 𝑀 ∈ ℕ0) ∧ (0 ≤ A
∧ A ≤
1)) → (A↑𝑀) ≤ (A↑𝑀)) |
16 | 15 | a1i 9 |
. . . . . 6
⊢ (𝑀 ∈ ℤ → (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑀) ≤ (A↑𝑀))) |
17 | | simprll 489 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → A ∈
ℝ) |
18 | | 1red 6840 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 1 ∈ ℝ) |
19 | | simprlr 490 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 𝑀 ∈
ℕ0) |
20 | | simpl 102 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 𝑘 ∈
(ℤ≥‘𝑀)) |
21 | | eluznn0 8313 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑘
∈ (ℤ≥‘𝑀)) → 𝑘 ∈
ℕ0) |
22 | 19, 20, 21 | syl2anc 391 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 𝑘 ∈
ℕ0) |
23 | | reexpcl 8926 |
. . . . . . . . . . . 12
⊢
((A ∈ ℝ ∧ 𝑘 ∈ ℕ0) → (A↑𝑘) ∈
ℝ) |
24 | 17, 22, 23 | syl2anc 391 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑𝑘) ∈
ℝ) |
25 | | simprrl 491 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 0 ≤ A) |
26 | | expge0 8945 |
. . . . . . . . . . . 12
⊢
((A ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ A)
→ 0 ≤ (A↑𝑘)) |
27 | 17, 22, 25, 26 | syl3anc 1134 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → 0 ≤ (A↑𝑘)) |
28 | | simprrr 492 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → A ≤ 1) |
29 | 17, 18, 24, 27, 28 | lemul2ad 7687 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → ((A↑𝑘) · A) ≤ ((A↑𝑘) · 1)) |
30 | 17 | recnd 6851 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → A ∈
ℂ) |
31 | | expp1 8916 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (A↑(𝑘 + 1)) = ((A↑𝑘) · A)) |
32 | 30, 22, 31 | syl2anc 391 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑(𝑘 + 1)) = ((A↑𝑘) · A)) |
33 | 24 | recnd 6851 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑𝑘) ∈
ℂ) |
34 | 33 | mulid1d 6842 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → ((A↑𝑘) · 1) = (A↑𝑘)) |
35 | 34 | eqcomd 2042 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑𝑘) = ((A↑𝑘) · 1)) |
36 | 29, 32, 35 | 3brtr4d 3785 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑(𝑘 + 1)) ≤ (A↑𝑘)) |
37 | | peano2nn0 7998 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈
ℕ0) |
38 | 22, 37 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (𝑘 + 1) ∈
ℕ0) |
39 | | reexpcl 8926 |
. . . . . . . . . . 11
⊢
((A ∈ ℝ ∧ (𝑘 + 1) ∈ ℕ0) → (A↑(𝑘 + 1)) ∈
ℝ) |
40 | 17, 38, 39 | syl2anc 391 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑(𝑘 + 1)) ∈
ℝ) |
41 | 13 | ad2antrl 459 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (A↑𝑀) ∈
ℝ) |
42 | | letr 6898 |
. . . . . . . . . 10
⊢
(((A↑(𝑘 + 1)) ∈
ℝ ∧ (A↑𝑘) ∈ ℝ
∧ (A↑𝑀) ∈
ℝ) → (((A↑(𝑘 + 1)) ≤ (A↑𝑘) ∧
(A↑𝑘) ≤ (A↑𝑀)) → (A↑(𝑘 + 1)) ≤ (A↑𝑀))) |
43 | 40, 24, 41, 42 | syl3anc 1134 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → (((A↑(𝑘 + 1)) ≤ (A↑𝑘) ∧
(A↑𝑘) ≤ (A↑𝑀)) → (A↑(𝑘 + 1)) ≤ (A↑𝑀))) |
44 | 36, 43 | mpand 405 |
. . . . . . . 8
⊢ ((𝑘 ∈ (ℤ≥‘𝑀) ∧
((A ∈
ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1))) → ((A↑𝑘) ≤ (A↑𝑀) → (A↑(𝑘 + 1)) ≤ (A↑𝑀))) |
45 | 44 | ex 108 |
. . . . . . 7
⊢ (𝑘 ∈ (ℤ≥‘𝑀) → (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → ((A↑𝑘) ≤ (A↑𝑀) → (A↑(𝑘 + 1)) ≤ (A↑𝑀)))) |
46 | 45 | a2d 23 |
. . . . . 6
⊢ (𝑘 ∈ (ℤ≥‘𝑀) → ((((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑘) ≤ (A↑𝑀)) → (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑(𝑘 + 1)) ≤ (A↑𝑀)))) |
47 | 3, 6, 9, 12, 16, 46 | uzind4 8307 |
. . . . 5
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑁) ≤ (A↑𝑀))) |
48 | 47 | expd 245 |
. . . 4
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((A ∈ ℝ ∧ 𝑀 ∈
ℕ0) → ((0 ≤ A
∧ A ≤
1) → (A↑𝑁) ≤ (A↑𝑀)))) |
49 | 48 | com12 27 |
. . 3
⊢
((A ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈
(ℤ≥‘𝑀) → ((0 ≤ A ∧ A ≤ 1) → (A↑𝑁) ≤ (A↑𝑀)))) |
50 | 49 | 3impia 1100 |
. 2
⊢
((A ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → ((0 ≤ A ∧ A ≤ 1) → (A↑𝑁) ≤ (A↑𝑀))) |
51 | 50 | imp 115 |
1
⊢
(((A ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ (0
≤ A ∧
A ≤ 1)) → (A↑𝑁) ≤ (A↑𝑀)) |