Proof of Theorem knoppndvlem7
| Step | Hyp | Ref
| Expression |
| 1 | | knoppndvlem7.f |
. . 3
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
| 2 | | knoppndvlem7.a |
. . . . 5
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) |
| 3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) |
| 4 | | knoppndvlem7.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 5 | | knoppndvlem7.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
| 6 | 5 | nn0zd 12639 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 7 | | knoppndvlem7.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 8 | 4, 6, 7 | knoppndvlem1 36513 |
. . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) |
| 9 | 3, 8 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 10 | 1, 9, 5 | knoppcnlem1 36494 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) = ((𝐶↑𝐽) · (𝑇‘(((2 · 𝑁)↑𝐽) · 𝐴)))) |
| 11 | 2 | oveq2i 7442 |
. . . . . 6
⊢ (((2
· 𝑁)↑𝐽) · 𝐴) = (((2 · 𝑁)↑𝐽) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) |
| 12 | 11 | a1i 11 |
. . . . 5
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · 𝐴) = (((2 · 𝑁)↑𝐽) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) |
| 13 | | 2cnd 12344 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℂ) |
| 14 | | nnz 12634 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 15 | 4, 14 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 16 | 15 | zcnd 12723 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 17 | 13, 16 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
| 18 | 17, 5 | expcld 14186 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ∈ ℂ) |
| 19 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 0) |
| 21 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
| 22 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
| 23 | 15 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 24 | | 0lt1 11785 |
. . . . . . . . . . . . . . 15
⊢ 0 <
1 |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 1) |
| 26 | | nnge1 12294 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
| 27 | 4, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ 𝑁) |
| 28 | 21, 22, 23, 25, 27 | ltletrd 11421 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑁) |
| 29 | 21, 28 | ltned 11397 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≠ 𝑁) |
| 30 | 29 | necomd 2996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) |
| 31 | 13, 16, 20, 30 | mulne0d 11915 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ≠ 0) |
| 32 | 6 | znegcld 12724 |
. . . . . . . . . 10
⊢ (𝜑 → -𝐽 ∈ ℤ) |
| 33 | 17, 31, 32 | expclzd 14191 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℂ) |
| 34 | 33, 13, 20 | divcld 12043 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℂ) |
| 35 | 7 | zcnd 12723 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 36 | 18, 34, 35 | mulassd 11284 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2)) · 𝑀) = (((2 · 𝑁)↑𝐽) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) |
| 37 | 36 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = ((((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2)) · 𝑀)) |
| 38 | 18, 33, 13, 20 | divassd 12078 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑𝐽) · ((2 · 𝑁)↑-𝐽)) / 2) = (((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2))) |
| 39 | 38 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2)) = ((((2 · 𝑁)↑𝐽) · ((2 · 𝑁)↑-𝐽)) / 2)) |
| 40 | 17, 31, 6 | expnegd 14193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) = (1 / ((2 · 𝑁)↑𝐽))) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · ((2 · 𝑁)↑-𝐽)) = (((2 · 𝑁)↑𝐽) · (1 / ((2 · 𝑁)↑𝐽)))) |
| 42 | 17, 31, 6 | expne0d 14192 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ≠ 0) |
| 43 | 18, 42 | recidd 12038 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · (1 / ((2 · 𝑁)↑𝐽))) = 1) |
| 44 | 41, 43 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · ((2 · 𝑁)↑-𝐽)) = 1) |
| 45 | 44 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑𝐽) · ((2 · 𝑁)↑-𝐽)) / 2) = (1 / 2)) |
| 46 | 39, 45 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2)) = (1 / 2)) |
| 47 | 46 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁)↑𝐽) · (((2 · 𝑁)↑-𝐽) / 2)) · 𝑀) = ((1 / 2) · 𝑀)) |
| 48 | 35, 13, 20 | divrec2d 12047 |
. . . . . . 7
⊢ (𝜑 → (𝑀 / 2) = ((1 / 2) · 𝑀)) |
| 49 | 48 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((1 / 2) · 𝑀) = (𝑀 / 2)) |
| 50 | 37, 47, 49 | 3eqtrd 2781 |
. . . . 5
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = (𝑀 / 2)) |
| 51 | 12, 50 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · 𝐴) = (𝑀 / 2)) |
| 52 | 51 | fveq2d 6910 |
. . 3
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝐽) · 𝐴)) = (𝑇‘(𝑀 / 2))) |
| 53 | 52 | oveq2d 7447 |
. 2
⊢ (𝜑 → ((𝐶↑𝐽) · (𝑇‘(((2 · 𝑁)↑𝐽) · 𝐴))) = ((𝐶↑𝐽) · (𝑇‘(𝑀 / 2)))) |
| 54 | 10, 53 | eqtrd 2777 |
1
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) = ((𝐶↑𝐽) · (𝑇‘(𝑀 / 2)))) |