| Step | Hyp | Ref
| Expression |
| 1 | | tanrpcl 26546 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) ∈
ℝ+) |
| 2 | 1 | adantl 481 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) ∈
ℝ+) |
| 3 | 2 | rpreccld 13087 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ+) |
| 4 | 3 | rpcnd 13079 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℂ) |
| 5 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
i ∈ ℂ) |
| 7 | | basel.n |
. . . . . . 7
⊢ 𝑁 = ((2 · 𝑀) + 1) |
| 8 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 9 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑀 ∈
ℕ) |
| 10 | | nnmulcl 12290 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
| 11 | 8, 9, 10 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℕ) |
| 12 | 11 | peano2nnd 12283 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((2 · 𝑀) + 1) ∈
ℕ) |
| 13 | 7, 12 | eqeltrid 2845 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ) |
| 14 | 13 | nnnn0d 12587 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ0) |
| 15 | | binom 15866 |
. . . . 5
⊢ (((1 /
(tan‘𝐴)) ∈
ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 /
(tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
| 16 | 4, 6, 14, 15 | syl3anc 1373 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
| 17 | | elioore 13417 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℝ) |
| 18 | 17 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℝ) |
| 19 | 18 | recoscld 16180 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℝ) |
| 20 | 19 | recnd 11289 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℂ) |
| 21 | 18 | resincld 16179 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ) |
| 22 | 21 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℂ) |
| 23 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
| 24 | 5, 22, 23 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘𝐴))
∈ ℂ) |
| 25 | 20, 24 | addcld 11280 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) + (i
· (sin‘𝐴)))
∈ ℂ) |
| 26 | | sincosq1sgn 26540 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
| 27 | 26 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
| 28 | 27 | simpld 494 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (sin‘𝐴)) |
| 29 | 28 | gt0ne0d 11827 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ≠
0) |
| 30 | 25, 22, 29, 14 | expdivd 14200 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁))) |
| 31 | 20, 24, 22, 29 | divdird 12081 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) =
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴)))) |
| 32 | 18 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℂ) |
| 33 | 27 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (cos‘𝐴)) |
| 34 | 33 | gt0ne0d 11827 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ≠
0) |
| 35 | | tanval 16164 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
| 36 | 32, 34, 35 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) = (1 /
((sin‘𝐴) /
(cos‘𝐴)))) |
| 38 | 22, 20, 29, 34 | recdivd 12060 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / ((sin‘𝐴) /
(cos‘𝐴))) =
((cos‘𝐴) /
(sin‘𝐴))) |
| 39 | 37, 38 | eqtr2d 2778 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) /
(sin‘𝐴)) = (1 /
(tan‘𝐴))) |
| 40 | 6, 22, 29 | divcan4d 12049 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘𝐴))
/ (sin‘𝐴)) =
i) |
| 41 | 39, 40 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴))) = ((1 /
(tan‘𝐴)) +
i)) |
| 42 | 31, 41 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) = ((1 /
(tan‘𝐴)) +
i)) |
| 43 | 42 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁)) |
| 44 | 13 | nnzd 12640 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℤ) |
| 45 | | demoivre 16236 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
| 46 | 32, 44, 45 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
| 47 | 46 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁))) |
| 48 | 30, 43, 47 | 3eqtr3d 2785 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁))) |
| 49 | 13 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℝ) |
| 50 | 49, 18 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑁 · 𝐴) ∈
ℝ) |
| 51 | 50 | recoscld 16180 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℝ) |
| 52 | 51 | recnd 11289 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℂ) |
| 53 | 50 | resincld 16179 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℝ) |
| 54 | 53 | recnd 11289 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℂ) |
| 55 | | mulcl 11239 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i ·
(sin‘(𝑁 ·
𝐴))) ∈
ℂ) |
| 56 | 5, 54, 55 | sylancr 587 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘(𝑁
· 𝐴))) ∈
ℂ) |
| 57 | 21, 28 | elrpd 13074 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ+) |
| 58 | 57, 44 | rpexpcld 14286 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℝ+) |
| 59 | 58 | rpcnd 13079 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℂ) |
| 60 | 58 | rpne0d 13082 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ≠ 0) |
| 61 | 52, 56, 59, 60 | divdird 12081 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)))) |
| 62 | 6, 54, 59, 60 | divassd 12078 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘(𝑁
· 𝐴))) /
((sin‘𝐴)↑𝑁)) = (i ·
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)))) |
| 63 | 62 | oveq2d 7447 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
| 64 | 48, 61, 63 | 3eqtrd 2781 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
| 65 | 16, 64 | eqtr3d 2779 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
| 66 | 65 | fveq2d 6910 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))) |
| 67 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗)))) |
| 68 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗)))) |
| 69 | 68 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗))))) |
| 70 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗)))) |
| 71 | 69, 70 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
| 72 | 67, 71 | oveq12d 7449 |
. . . . . 6
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
| 73 | 72 | fveq2d 6910 |
. . . . 5
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
| 74 | | fzfid 14014 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑀) ∈
Fin) |
| 75 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 76 | | elfznn0 13660 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
| 77 | 76 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0) |
| 78 | | nn0mulcl 12562 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
| 79 | 75, 77, 78 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℕ0) |
| 80 | 79 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℝ) |
| 81 | 11 | nnred 12281 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℝ) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℝ) |
| 83 | 49 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ) |
| 84 | | elfzle2 13568 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀) |
| 85 | 84 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀) |
| 86 | 77 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ) |
| 87 | | nnre 12273 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 88 | 87 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ) |
| 89 | | 2re 12340 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
| 90 | | 2pos 12369 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
| 91 | 89, 90 | pm3.2i 470 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ
∧ 0 < 2)) |
| 93 | | lemul2 12120 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
| 94 | 86, 88, 92, 93 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
| 95 | 85, 94 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀)) |
| 96 | 82 | lep1d 12199 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1)) |
| 97 | 96, 7 | breqtrrdi 5185 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁) |
| 98 | 80, 82, 83, 95, 97 | letrd 11418 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁) |
| 99 | | nn0uz 12920 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
| 100 | 79, 99 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
(ℤ≥‘0)) |
| 101 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ) |
| 102 | | elfz5 13556 |
. . . . . . . . . . 11
⊢ (((2
· 𝑘) ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
| 103 | 100, 101,
102 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
| 104 | 98, 103 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁)) |
| 105 | | fznn0sub2 13675 |
. . . . . . . . 9
⊢ ((2
· 𝑘) ∈
(0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
| 106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
| 107 | 106 | ex 412 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))) |
| 108 | 13 | nncnd 12282 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℂ) |
| 109 | 108 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ) |
| 110 | | 2cn 12341 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
| 111 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ) |
| 112 | 111 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ) |
| 113 | 112 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ) |
| 114 | | mulcl 11239 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ) → (2 · 𝑘) ∈ ℂ) |
| 115 | 110, 113,
114 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ) |
| 116 | 112 | ssriv 3987 |
. . . . . . . . . . . 12
⊢
(0...𝑀) ⊆
ℂ |
| 117 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀)) |
| 118 | 116, 117 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ) |
| 119 | | mulcl 11239 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑚
∈ ℂ) → (2 · 𝑚) ∈ ℂ) |
| 120 | 110, 118,
119 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ) |
| 121 | 109, 115,
120 | subcanad 11663 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚))) |
| 122 | | 2cnne0 12476 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠
0)) |
| 124 | | mulcan 11900 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
| 125 | 113, 118,
123, 124 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
| 126 | 121, 125 | bitrd 279 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)) |
| 127 | 126 | ex 412 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))) |
| 128 | 107, 127 | dom2lem 9032 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁)) |
| 129 | | f1f1orn 6859 |
. . . . . 6
⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
| 130 | 128, 129 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
| 131 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
| 132 | 131 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗))) |
| 133 | | eqid 2737 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) |
| 134 | | ovex 7464 |
. . . . . . 7
⊢ (𝑁 − (2 · 𝑗)) ∈ V |
| 135 | 132, 133,
134 | fvmpt 7016 |
. . . . . 6
⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
| 136 | 135 | adantl 481 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
| 137 | 106 | fmpttd 7135 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁)) |
| 138 | 137 | frnd 6744 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁)) |
| 139 | 138 | sselda 3983 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
| 140 | | bccl2 14362 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ) |
| 141 | 140 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ) |
| 142 | 141 | nncnd 12282 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ) |
| 143 | 2 | rprecred 13088 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ) |
| 144 | | fznn0sub 13596 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈
ℕ0) |
| 145 | | reexpcl 14119 |
. . . . . . . . . . . 12
⊢ (((1 /
(tan‘𝐴)) ∈
ℝ ∧ (𝑁 −
𝑚) ∈
ℕ0) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
| 146 | 143, 144,
145 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
| 147 | 146 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ) |
| 148 | | elfznn0 13660 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0) |
| 149 | 148 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0) |
| 150 | | expcl 14120 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ 𝑚
∈ ℕ0) → (i↑𝑚) ∈ ℂ) |
| 151 | 5, 149, 150 | sylancr 587 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈
ℂ) |
| 152 | 147, 151 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((1 /
(tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ) |
| 153 | 142, 152 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
| 154 | 139, 153 | syldan 591 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
| 155 | 154 | imcld 15234 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ) |
| 156 | 155 | recnd 11289 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ) |
| 157 | 73, 74, 130, 136, 156 | fsumf1o 15759 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
| 158 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
| 159 | 141 | nnred 12281 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ) |
| 160 | 158, 159 | sylan2 593 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ) |
| 161 | 158, 146 | sylan2 593 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
| 162 | | eldif 3961 |
. . . . . . . . 9
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
| 163 | | elfzelz 13564 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ) |
| 164 | 163 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ) |
| 165 | | zeo 12704 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨
((𝑚 + 1) / 2) ∈
ℤ)) |
| 166 | 164, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈
ℤ)) |
| 167 | | i2 14241 |
. . . . . . . . . . . . . . . . . 18
⊢
(i↑2) = -1 |
| 168 | 167 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢
((i↑2)↑(𝑚
/ 2)) = (-1↑(𝑚 /
2)) |
| 169 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℤ) |
| 170 | 148 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
| 171 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
| 172 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ 𝑚) |
| 173 | | divge0 12137 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 ≤ (𝑚 / 2)) |
| 174 | 89, 90, 173 | mpanr12 705 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) → 0 ≤ (𝑚 / 2)) |
| 175 | 171, 172,
174 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ (𝑚 /
2)) |
| 176 | 170, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2)) |
| 177 | | elnn0z 12626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 / 2) ∈ ℕ0
↔ ((𝑚 / 2) ∈
ℤ ∧ 0 ≤ (𝑚 /
2))) |
| 178 | 169, 176,
177 | sylanbrc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℕ0) |
| 179 | | expmul 14148 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) →
(i↑(2 · (𝑚 /
2))) = ((i↑2)↑(𝑚
/ 2))) |
| 180 | 5, 75, 178, 179 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
((i↑2)↑(𝑚 /
2))) |
| 181 | 170 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
| 182 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ≠
0 |
| 183 | | divcan2 11930 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚) |
| 184 | 110, 182,
183 | mp3an23 1455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℂ → (2
· (𝑚 / 2)) = 𝑚) |
| 185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 ·
(𝑚 / 2)) = 𝑚) |
| 186 | 185 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
(i↑𝑚)) |
| 187 | 180, 186 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) →
((i↑2)↑(𝑚 / 2)) =
(i↑𝑚)) |
| 188 | 168, 187 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚)) |
| 189 | | neg1rr 12381 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
ℝ |
| 190 | | reexpcl 14119 |
. . . . . . . . . . . . . . . . 17
⊢ ((-1
∈ ℝ ∧ (𝑚 /
2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ) |
| 191 | 189, 178,
190 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈
ℝ) |
| 192 | 188, 191 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈
ℝ) |
| 193 | 192 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈
ℝ)) |
| 194 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈
ℤ) |
| 195 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 196 | 195 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℤ) |
| 197 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℂ) |
| 198 | 148 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
| 199 | 198 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
| 200 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈
ℂ) |
| 201 | 197, 199,
200 | pnpcan2d 11658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚)) |
| 202 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2
· 1) = 2 |
| 203 | | df-2 12329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 = (1 +
1) |
| 204 | 202, 203 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 + 1) =
(2 · 1) |
| 205 | 204 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
· 𝑀) + (1 + 1)) =
((2 · 𝑀) + (2
· 1)) |
| 206 | 7 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1) |
| 207 | 11 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℂ) |
| 208 | 207 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· 𝑀) ∈
ℂ) |
| 209 | 208, 200,
200 | addassd 11283 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· 𝑀) + 1) + 1) = ((2
· 𝑀) + (1 +
1))) |
| 210 | 206, 209 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1))) |
| 211 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈
ℂ) |
| 212 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
| 213 | 212 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℂ) |
| 214 | 211, 213,
200 | adddid 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) = ((2
· 𝑀) + (2 ·
1))) |
| 215 | 205, 210,
214 | 3eqtr4a 2803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1))) |
| 216 | 215 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
| 217 | 201, 216 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
| 218 | 217 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2)) |
| 219 | 196 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℤ) |
| 220 | 219 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℂ) |
| 221 | | mulcl 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ ℂ ∧ (𝑀 +
1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ) |
| 222 | 110, 220,
221 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) ∈
ℂ) |
| 223 | | peano2cn 11433 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℂ → (𝑚 + 1) ∈
ℂ) |
| 224 | 199, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈
ℂ) |
| 225 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℂ ∧ 2 ≠ 0)) |
| 226 | | divsubdir 11961 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((2
· (𝑀 + 1)) ∈
ℂ ∧ (𝑚 + 1)
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 ·
(𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 ·
(𝑀 + 1)) / 2) −
((𝑚 + 1) /
2))) |
| 227 | 222, 224,
225, 226 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) −
(𝑚 + 1)) / 2) = (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) /
2))) |
| 228 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠
0) |
| 229 | 220, 211,
228 | divcan3d 12048 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2
· (𝑀 + 1)) / 2) =
(𝑀 + 1)) |
| 230 | 229 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) / 2)) =
((𝑀 + 1) − ((𝑚 + 1) / 2))) |
| 231 | 218, 227,
230 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2))) |
| 232 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈
ℤ) |
| 233 | 219, 232 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈
ℤ) |
| 234 | 231, 233 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ) |
| 235 | 144 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈
ℕ0) |
| 236 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → (𝑁 − 𝑚) ∈ ℝ) |
| 237 | | nn0ge0 12551 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
(𝑁 − 𝑚)) |
| 238 | | divge0 12137 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ ((𝑁 −
𝑚) / 2)) |
| 239 | 89, 90, 238 | mpanr12 705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2)) |
| 240 | 236, 237,
239 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
((𝑁 − 𝑚) / 2)) |
| 241 | 235, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
((𝑁 − 𝑚) / 2)) |
| 242 | 235 | nn0red 12588 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ) |
| 243 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℝ) |
| 244 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
| 245 | 243, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈
ℝ) |
| 246 | 198, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
𝑚) |
| 247 | 198 | nn0red 12588 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℝ) |
| 248 | 243, 247 | subge02d 11855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤
𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁)) |
| 249 | 246, 248 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁) |
| 250 | 243 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1)) |
| 251 | 242, 243,
245, 249, 250 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1)) |
| 252 | 251, 215 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1))) |
| 253 | 219 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℝ) |
| 254 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℝ ∧ 0 < 2)) |
| 255 | | ltdivmul 12143 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
| 256 | 242, 253,
254, 255 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
| 257 | 252, 256 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1)) |
| 258 | | zleltp1 12668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
| 259 | 234, 196,
258 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
| 260 | 257, 259 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀) |
| 261 | 194, 196,
234, 241, 260 | elfzd 13555 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) |
| 262 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2))) |
| 263 | 262 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
| 264 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V |
| 265 | 263, 133,
264 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
| 266 | 261, 265 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
| 267 | 235 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ) |
| 268 | 267, 211,
228 | divcan2d 12045 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚)) |
| 269 | 268 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚))) |
| 270 | 197, 199 | nncand 11625 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚) |
| 271 | 266, 269,
270 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚) |
| 272 | 137 | ffnd 6737 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀)) |
| 273 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
| 274 | 272, 261,
273 | syl2an2r 685 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
| 275 | 271, 274 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
| 276 | 275 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
| 277 | 193, 276 | orim12d 967 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ)
→ ((i↑𝑚) ∈
ℝ ∨ 𝑚 ∈ ran
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))) |
| 278 | 166, 277 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
| 279 | 278 | orcomd 872 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ)) |
| 280 | 279 | ord 865 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ)) |
| 281 | 280 | impr 454 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
| 282 | 162, 281 | sylan2b 594 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
| 283 | 161, 282 | remulcld 11291 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ) |
| 284 | 160, 283 | remulcld 11291 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ) |
| 285 | 284 | reim0d 15264 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0) |
| 286 | | fzfid 14014 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑁) ∈
Fin) |
| 287 | 138, 156,
285, 286 | fsumss 15761 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
| 288 | | elfznn0 13660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
| 289 | 288 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) |
| 290 | | nn0mulcl 12562 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ0 ∧ 𝑗 ∈ ℕ0) → (2
· 𝑗) ∈
ℕ0) |
| 291 | 75, 289, 290 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℕ0) |
| 292 | 291 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℤ) |
| 293 | | bccl 14361 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) ∈
ℕ0) |
| 294 | 14, 292, 293 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈
ℕ0) |
| 295 | 294 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ) |
| 296 | | fznn0sub 13596 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈
ℕ0) |
| 297 | 296 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈
ℕ0) |
| 298 | | reexpcl 14119 |
. . . . . . . . . . . . . 14
⊢ ((-1
∈ ℝ ∧ (𝑀
− 𝑗) ∈
ℕ0) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
| 299 | 189, 297,
298 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
| 300 | 295, 299 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ) |
| 301 | | 2z 12649 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
| 302 | | znegcl 12652 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
| 303 | 301, 302 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ -2 ∈
ℤ |
| 304 | | rpexpcl 14121 |
. . . . . . . . . . . . . . 15
⊢
(((tan‘𝐴)
∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈
ℝ+) |
| 305 | 2, 303, 304 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ+) |
| 306 | 305 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ) |
| 307 | | reexpcl 14119 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0)
→ (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ) |
| 308 | 306, 288,
307 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℝ) |
| 309 | 300, 308 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) |
| 310 | 309 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
| 311 | | mulcl 11239 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
| 312 | 5, 310, 311 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
| 313 | 312 | addlidd 11462 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) |
| 314 | 294 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ) |
| 315 | 299 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ) |
| 316 | 308 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℂ) |
| 317 | 314, 315,
316 | mulassd 11284 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
| 318 | 317 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
| 319 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → i ∈
ℂ) |
| 320 | 315, 316 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
| 321 | 319, 314,
320 | mul12d 11470 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
| 322 | 318, 321 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
| 323 | | bccmpl 14348 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
| 324 | 14, 292, 323 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
| 325 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ) |
| 326 | 291 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℂ) |
| 327 | 325, 326 | nncand 11625 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗)) |
| 328 | 327 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
| 329 | 2 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℝ+) |
| 330 | 329 | rpcnd 13079 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℂ) |
| 331 | | expneg 14110 |
. . . . . . . . . . . . . 14
⊢
(((tan‘𝐴)
∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) →
((tan‘𝐴)↑-(2
· 𝑗)) = (1 /
((tan‘𝐴)↑(2
· 𝑗)))) |
| 332 | 330, 291,
331 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
| 333 | 289 | nn0cnd 12589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ) |
| 334 | | mulneg1 11699 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗)) |
| 335 | 110, 333,
334 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗)) |
| 336 | 335 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗))) |
| 337 | 329 | rpne0d 13082 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0) |
| 338 | 330, 337,
292 | exprecd 14194 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
| 339 | 332, 336,
338 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
| 340 | 303 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → -2 ∈
ℤ) |
| 341 | 289 | nn0zd 12639 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ) |
| 342 | | expmulz 14149 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)
∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧
𝑗 ∈ ℤ)) →
((tan‘𝐴)↑(-2
· 𝑗)) =
(((tan‘𝐴)↑-2)↑𝑗)) |
| 343 | 330, 337,
340, 341, 342 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗)) |
| 344 | 328, 339,
343 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗)) |
| 345 | 7 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗)) |
| 346 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℕ) |
| 347 | 346 | nncnd 12282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℂ) |
| 348 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 1 ∈
ℂ) |
| 349 | 347, 348,
326 | addsubd 11641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
| 350 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℂ) |
| 351 | 212 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ) |
| 352 | 350, 351,
333 | subdid 11719 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗))) |
| 353 | 352 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
| 354 | 349, 353 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
| 355 | 345, 354 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
| 356 | 355 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 ·
(𝑀 − 𝑗)) + 1))) |
| 357 | | nn0mulcl 12562 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (𝑀 − 𝑗) ∈ ℕ0) → (2
· (𝑀 − 𝑗)) ∈
ℕ0) |
| 358 | 75, 297, 357 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈
ℕ0) |
| 359 | | expp1 14109 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ0) →
(i↑((2 · (𝑀
− 𝑗)) + 1)) =
((i↑(2 · (𝑀
− 𝑗))) ·
i)) |
| 360 | 5, 358, 359 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑((2 ·
(𝑀 − 𝑗)) + 1)) = ((i↑(2 ·
(𝑀 − 𝑗))) ·
i)) |
| 361 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℕ0) |
| 362 | 319, 297,
361 | expmuld 14189 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗))) |
| 363 | 167 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢
((i↑2)↑(𝑀
− 𝑗)) =
(-1↑(𝑀 − 𝑗)) |
| 364 | 362, 363 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗))) |
| 365 | 364 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i↑(2 ·
(𝑀 − 𝑗))) · i) =
((-1↑(𝑀 − 𝑗)) · i)) |
| 366 | 356, 360,
365 | 3eqtrd 2781 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i)) |
| 367 | | mulcom 11241 |
. . . . . . . . . . . . 13
⊢
(((-1↑(𝑀
− 𝑗)) ∈ ℂ
∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
| 368 | 315, 5, 367 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
| 369 | 366, 368 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i ·
(-1↑(𝑀 − 𝑗)))) |
| 370 | 344, 369 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((1 /
(tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗))))) |
| 371 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
| 372 | 5, 315, 371 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
| 373 | 372, 316 | mulcomd 11282 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i ·
(-1↑(𝑀 − 𝑗))))) |
| 374 | 319, 315,
316 | mulassd 11284 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
| 375 | 370, 373,
374 | 3eqtr2rd 2784 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
| 376 | 324, 375 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
| 377 | 313, 322,
376 | 3eqtrd 2781 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
| 378 | 377 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
| 379 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 380 | | crim 15154 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 +
(i · (((𝑁C(2
· 𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 381 | 379, 309,
380 | sylancr 587 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 382 | 378, 381 | eqtr3d 2779 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 383 | 382 | sumeq2dv 15738 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 384 | 157, 287,
383 | 3eqtr3d 2785 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 385 | 286, 153 | fsumim 15845 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
| 386 | 305 | rpcnd 13079 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℂ) |
| 387 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗)) |
| 388 | 387 | oveq2d 7447 |
. . . . . 6
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 389 | 388 | sumeq2sdv 15739 |
. . . . 5
⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 390 | | basel.p |
. . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
| 391 | | sumex 15724 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V |
| 392 | 389, 390,
391 | fvmpt 7016 |
. . . 4
⊢
(((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 393 | 386, 392 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
| 394 | 384, 385,
393 | 3eqtr4d 2787 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2))) |
| 395 | 51, 58 | rerpdivcld 13108 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
| 396 | 53, 58 | rerpdivcld 13108 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
| 397 | 395, 396 | crimd 15271 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |
| 398 | 66, 394, 397 | 3eqtr3d 2785 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |