| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑎 = 0 → (((2 · 𝐴) − 1)↑𝑎) = (((2 · 𝐴) −
1)↑0)) |
| 2 | | oveq1 7438 |
. . . . . 6
⊢ (𝑎 = 0 → (𝑎 + 1) = (0 + 1)) |
| 3 | 2 | oveq2d 7447 |
. . . . 5
⊢ (𝑎 = 0 → (𝐴 Yrm (𝑎 + 1)) = (𝐴 Yrm (0 + 1))) |
| 4 | 1, 3 | breq12d 5156 |
. . . 4
⊢ (𝑎 = 0 → ((((2 · 𝐴) − 1)↑𝑎) ≤ (𝐴 Yrm (𝑎 + 1)) ↔ (((2 · 𝐴) − 1)↑0) ≤ (𝐴 Yrm (0 + 1)))) |
| 5 | 4 | imbi2d 340 |
. . 3
⊢ (𝑎 = 0 → ((𝐴 ∈ (ℤ≥‘2)
→ (((2 · 𝐴)
− 1)↑𝑎) ≤
(𝐴 Yrm (𝑎 + 1))) ↔ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑0) ≤ (𝐴 Yrm (0 + 1))))) |
| 6 | | oveq2 7439 |
. . . . 5
⊢ (𝑎 = 𝑏 → (((2 · 𝐴) − 1)↑𝑎) = (((2 · 𝐴) − 1)↑𝑏)) |
| 7 | | oveq1 7438 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝑎 + 1) = (𝑏 + 1)) |
| 8 | 7 | oveq2d 7447 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝐴 Yrm (𝑎 + 1)) = (𝐴 Yrm (𝑏 + 1))) |
| 9 | 6, 8 | breq12d 5156 |
. . . 4
⊢ (𝑎 = 𝑏 → ((((2 · 𝐴) − 1)↑𝑎) ≤ (𝐴 Yrm (𝑎 + 1)) ↔ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1)))) |
| 10 | 9 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝐴 ∈ (ℤ≥‘2)
→ (((2 · 𝐴)
− 1)↑𝑎) ≤
(𝐴 Yrm (𝑎 + 1))) ↔ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))))) |
| 11 | | oveq2 7439 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (((2 · 𝐴) − 1)↑𝑎) = (((2 · 𝐴) − 1)↑(𝑏 + 1))) |
| 12 | | oveq1 7438 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝑎 + 1) = ((𝑏 + 1) + 1)) |
| 13 | 12 | oveq2d 7447 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → (𝐴 Yrm (𝑎 + 1)) = (𝐴 Yrm ((𝑏 + 1) + 1))) |
| 14 | 11, 13 | breq12d 5156 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → ((((2 · 𝐴) − 1)↑𝑎) ≤ (𝐴 Yrm (𝑎 + 1)) ↔ (((2 · 𝐴) − 1)↑(𝑏 + 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1)))) |
| 15 | 14 | imbi2d 340 |
. . 3
⊢ (𝑎 = (𝑏 + 1) → ((𝐴 ∈ (ℤ≥‘2)
→ (((2 · 𝐴)
− 1)↑𝑎) ≤
(𝐴 Yrm (𝑎 + 1))) ↔ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1))))) |
| 16 | | oveq2 7439 |
. . . . 5
⊢ (𝑎 = 𝑁 → (((2 · 𝐴) − 1)↑𝑎) = (((2 · 𝐴) − 1)↑𝑁)) |
| 17 | | oveq1 7438 |
. . . . . 6
⊢ (𝑎 = 𝑁 → (𝑎 + 1) = (𝑁 + 1)) |
| 18 | 17 | oveq2d 7447 |
. . . . 5
⊢ (𝑎 = 𝑁 → (𝐴 Yrm (𝑎 + 1)) = (𝐴 Yrm (𝑁 + 1))) |
| 19 | 16, 18 | breq12d 5156 |
. . . 4
⊢ (𝑎 = 𝑁 → ((((2 · 𝐴) − 1)↑𝑎) ≤ (𝐴 Yrm (𝑎 + 1)) ↔ (((2 · 𝐴) − 1)↑𝑁) ≤ (𝐴 Yrm (𝑁 + 1)))) |
| 20 | 19 | imbi2d 340 |
. . 3
⊢ (𝑎 = 𝑁 → ((𝐴 ∈ (ℤ≥‘2)
→ (((2 · 𝐴)
− 1)↑𝑎) ≤
(𝐴 Yrm (𝑎 + 1))) ↔ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑𝑁) ≤ (𝐴 Yrm (𝑁 + 1))))) |
| 21 | | 1le1 11891 |
. . . . 5
⊢ 1 ≤
1 |
| 22 | 21 | a1i 11 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → 1 ≤ 1) |
| 23 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 24 | | eluzelcn 12890 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℂ) |
| 25 | | mulcl 11239 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ 𝐴
∈ ℂ) → (2 · 𝐴) ∈ ℂ) |
| 26 | 23, 24, 25 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈
(ℤ≥‘2) → (2 · 𝐴) ∈ ℂ) |
| 27 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 28 | | subcl 11507 |
. . . . . 6
⊢ (((2
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → ((2 · 𝐴) − 1) ∈
ℂ) |
| 29 | 26, 27, 28 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → ((2 · 𝐴) − 1) ∈
ℂ) |
| 30 | 29 | exp0d 14180 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑0) = 1) |
| 31 | | 0p1e1 12388 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 32 | 31 | oveq2i 7442 |
. . . . 5
⊢ (𝐴 Yrm (0 + 1)) =
(𝐴 Yrm
1) |
| 33 | | rmy1 42942 |
. . . . 5
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 1) = 1) |
| 34 | 32, 33 | eqtrid 2789 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm (0 + 1)) =
1) |
| 35 | 22, 30, 34 | 3brtr4d 5175 |
. . 3
⊢ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑0) ≤ (𝐴 Yrm (0 + 1))) |
| 36 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 37 | | eluzelre 12889 |
. . . . . . . . . . 11
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℝ) |
| 38 | 37 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℝ) |
| 39 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ 𝐴
∈ ℝ) → (2 · 𝐴) ∈ ℝ) |
| 40 | 36, 38, 39 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · 𝐴) ∈ ℝ) |
| 41 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 42 | | resubcl 11573 |
. . . . . . . . 9
⊢ (((2
· 𝐴) ∈ ℝ
∧ 1 ∈ ℝ) → ((2 · 𝐴) − 1) ∈
ℝ) |
| 43 | 40, 41, 42 | sylancl 586 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((2 · 𝐴) − 1) ∈
ℝ) |
| 44 | | peano2nn0 12566 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ (𝑏 + 1) ∈
ℕ0) |
| 45 | 44 | adantr 480 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 + 1) ∈
ℕ0) |
| 46 | 43, 45 | reexpcld 14203 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ∈ ℝ) |
| 47 | 46 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ∈
ℝ) |
| 48 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈
(ℤ≥‘2)) |
| 49 | | nn0z 12638 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℤ) |
| 50 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℤ) |
| 51 | 50 | peano2zd 12725 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 + 1) ∈ ℤ) |
| 52 | | frmy 42926 |
. . . . . . . . . . 11
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
| 53 | 52 | fovcl 7561 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 + 1) ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) ∈
ℤ) |
| 54 | 53 | zred 12722 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 + 1) ∈ ℤ) → (𝐴 Yrm (𝑏 + 1)) ∈
ℝ) |
| 55 | 48, 51, 54 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 + 1)) ∈ ℝ) |
| 56 | 55, 43 | remulcld 11291 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) ∈
ℝ) |
| 57 | 56 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) ∈
ℝ) |
| 58 | 51 | peano2zd 12725 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝑏 + 1) + 1) ∈ ℤ) |
| 59 | 52 | fovcl 7561 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ ((𝑏 + 1) + 1) ∈ ℤ) → (𝐴 Yrm ((𝑏 + 1) + 1)) ∈
ℤ) |
| 60 | 59 | zred 12722 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ ((𝑏 + 1) + 1) ∈ ℤ) → (𝐴 Yrm ((𝑏 + 1) + 1)) ∈
ℝ) |
| 61 | 48, 58, 60 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm ((𝑏 + 1) + 1)) ∈ ℝ) |
| 62 | 61 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (𝐴 Yrm ((𝑏 + 1) + 1)) ∈ ℝ) |
| 63 | 29 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → ((2 · 𝐴) − 1) ∈
ℂ) |
| 64 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → 𝑏 ∈ ℕ0) |
| 65 | 63, 64 | expp1d 14187 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) = ((((2 · 𝐴) − 1)↑𝑏) · ((2 · 𝐴) − 1))) |
| 66 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℕ0) |
| 67 | 43, 66 | reexpcld 14203 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (((2 · 𝐴) − 1)↑𝑏) ∈ ℝ) |
| 68 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 69 | | eluz2nn 12924 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
| 70 | 69 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝐴 ∈ ℕ) |
| 71 | | nnmulcl 12290 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝐴
∈ ℕ) → (2 · 𝐴) ∈ ℕ) |
| 72 | 68, 70, 71 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · 𝐴) ∈ ℕ) |
| 73 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ ((2
· 𝐴) ∈ ℕ
→ ((2 · 𝐴)
− 1) ∈ ℕ0) |
| 74 | | nn0ge0 12551 |
. . . . . . . . . . 11
⊢ (((2
· 𝐴) − 1)
∈ ℕ0 → 0 ≤ ((2 · 𝐴) − 1)) |
| 75 | 72, 73, 74 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 0 ≤ ((2 · 𝐴) − 1)) |
| 76 | 43, 75 | jca 511 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (((2 · 𝐴) − 1) ∈ ℝ ∧ 0 ≤ ((2
· 𝐴) −
1))) |
| 77 | 67, 55, 76 | 3jca 1129 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((((2 · 𝐴) − 1)↑𝑏) ∈ ℝ ∧ (𝐴 Yrm (𝑏 + 1)) ∈ ℝ ∧ (((2 ·
𝐴) − 1) ∈
ℝ ∧ 0 ≤ ((2 · 𝐴) − 1)))) |
| 78 | | lemul1a 12121 |
. . . . . . . 8
⊢ ((((((2
· 𝐴) −
1)↑𝑏) ∈ ℝ
∧ (𝐴 Yrm
(𝑏 + 1)) ∈ ℝ
∧ (((2 · 𝐴)
− 1) ∈ ℝ ∧ 0 ≤ ((2 · 𝐴) − 1))) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → ((((2 · 𝐴) − 1)↑𝑏) · ((2 · 𝐴) − 1)) ≤ ((𝐴 Yrm (𝑏 + 1)) · ((2 ·
𝐴) −
1))) |
| 79 | 77, 78 | stoic3 1776 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → ((((2 · 𝐴) − 1)↑𝑏) · ((2 · 𝐴) − 1)) ≤ ((𝐴 Yrm (𝑏 + 1)) · ((2 ·
𝐴) −
1))) |
| 80 | 65, 79 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ≤ ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1))) |
| 81 | | nn0cn 12536 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℂ) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℂ) |
| 83 | | pncan 11514 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑏 + 1)
− 1) = 𝑏) |
| 84 | 82, 27, 83 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝑏 + 1) − 1) = 𝑏) |
| 85 | 84 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm ((𝑏 + 1) − 1)) = (𝐴 Yrm 𝑏)) |
| 86 | 52 | fovcl 7561 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℤ) |
| 87 | 86 | zred 12722 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ) → (𝐴 Yrm 𝑏) ∈ ℝ) |
| 88 | 48, 50, 87 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm 𝑏) ∈ ℝ) |
| 89 | 85, 88 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm ((𝑏 + 1) − 1)) ∈
ℝ) |
| 90 | | remulcl 11240 |
. . . . . . . . . 10
⊢ (((𝐴 Yrm (𝑏 + 1)) ∈ ℝ ∧ 1
∈ ℝ) → ((𝐴
Yrm (𝑏 + 1))
· 1) ∈ ℝ) |
| 91 | 55, 41, 90 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · 1) ∈
ℝ) |
| 92 | 40, 55 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1))) ∈ ℝ) |
| 93 | | nn0re 12535 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℕ0
→ 𝑏 ∈
ℝ) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ∈ ℝ) |
| 95 | 94 | lep1d 12199 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 𝑏 ≤ (𝑏 + 1)) |
| 96 | | lermy 42967 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑏 ∈ ℤ ∧ (𝑏 + 1) ∈ ℤ) → (𝑏 ≤ (𝑏 + 1) ↔ (𝐴 Yrm 𝑏) ≤ (𝐴 Yrm (𝑏 + 1)))) |
| 97 | 48, 50, 51, 96 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝑏 ≤ (𝑏 + 1) ↔ (𝐴 Yrm 𝑏) ≤ (𝐴 Yrm (𝑏 + 1)))) |
| 98 | 95, 97 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm 𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) |
| 99 | 55 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm (𝑏 + 1)) ∈ ℂ) |
| 100 | 99 | mulridd 11278 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · 1) = (𝐴 Yrm (𝑏 + 1))) |
| 101 | 98, 85, 100 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm ((𝑏 + 1) − 1)) ≤ ((𝐴 Yrm (𝑏 + 1)) · 1)) |
| 102 | 89, 91, 92, 101 | lesub2dd 11880 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1))) − ((𝐴 Yrm (𝑏 + 1)) · 1)) ≤ (((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1))) − (𝐴 Yrm ((𝑏 + 1) − 1)))) |
| 103 | 40 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (2 · 𝐴) ∈ ℂ) |
| 104 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → 1 ∈ ℂ) |
| 105 | 99, 103, 104 | subdid 11719 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) = (((𝐴 Yrm (𝑏 + 1)) · (2 ·
𝐴)) − ((𝐴 Yrm (𝑏 + 1)) ·
1))) |
| 106 | 99, 103 | mulcomd 11282 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · (2 · 𝐴)) = ((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1)))) |
| 107 | 106 | oveq1d 7446 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (((𝐴 Yrm (𝑏 + 1)) · (2 · 𝐴)) − ((𝐴 Yrm (𝑏 + 1)) · 1)) = (((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1))) − ((𝐴 Yrm (𝑏 + 1)) · 1))) |
| 108 | 105, 107 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) = (((2 ·
𝐴) · (𝐴 Yrm (𝑏 + 1))) − ((𝐴 Yrm (𝑏 + 1)) ·
1))) |
| 109 | | rmyluc2 42950 |
. . . . . . . . 9
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (𝑏 + 1) ∈ ℤ) → (𝐴 Yrm ((𝑏 + 1) + 1)) = (((2 ·
𝐴) · (𝐴 Yrm (𝑏 + 1))) − (𝐴 Yrm ((𝑏 + 1) −
1)))) |
| 110 | 48, 51, 109 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → (𝐴 Yrm ((𝑏 + 1) + 1)) = (((2 · 𝐴) · (𝐴 Yrm (𝑏 + 1))) − (𝐴 Yrm ((𝑏 + 1) − 1)))) |
| 111 | 102, 108,
110 | 3brtr4d 5175 |
. . . . . . 7
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2)) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1))) |
| 112 | 111 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → ((𝐴 Yrm (𝑏 + 1)) · ((2 · 𝐴) − 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1))) |
| 113 | 47, 57, 62, 80, 112 | letrd 11418 |
. . . . 5
⊢ ((𝑏 ∈ ℕ0
∧ 𝐴 ∈
(ℤ≥‘2) ∧ (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1))) |
| 114 | 113 | 3exp 1120 |
. . . 4
⊢ (𝑏 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → ((((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1)) → (((2 · 𝐴) − 1)↑(𝑏 + 1)) ≤ (𝐴 Yrm ((𝑏 + 1) + 1))))) |
| 115 | 114 | a2d 29 |
. . 3
⊢ (𝑏 ∈ ℕ0
→ ((𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑𝑏) ≤ (𝐴 Yrm (𝑏 + 1))) → (𝐴 ∈ (ℤ≥‘2)
→ (((2 · 𝐴)
− 1)↑(𝑏 + 1))
≤ (𝐴 Yrm
((𝑏 + 1) +
1))))) |
| 116 | 5, 10, 15, 20, 35, 115 | nn0ind 12713 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(ℤ≥‘2) → (((2 · 𝐴) − 1)↑𝑁) ≤ (𝐴 Yrm (𝑁 + 1)))) |
| 117 | 116 | impcom 407 |
1
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (((2
· 𝐴) −
1)↑𝑁) ≤ (𝐴 Yrm (𝑁 + 1))) |