Step | Hyp | Ref
| Expression |
1 | | tanrpcl 24256 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) ∈
ℝ+) |
2 | 1 | adantl 482 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) ∈
ℝ+) |
3 | 2 | rpreccld 11882 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ+) |
4 | 3 | rpcnd 11874 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℂ) |
5 | | ax-icn 9995 |
. . . . . 6
⊢ i ∈
ℂ |
6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
i ∈ ℂ) |
7 | | basel.n |
. . . . . . 7
⊢ 𝑁 = ((2 · 𝑀) + 1) |
8 | | 2nn 11185 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
9 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑀 ∈
ℕ) |
10 | | nnmulcl 11043 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
11 | 8, 9, 10 | sylancr 695 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℕ) |
12 | 11 | peano2nnd 11037 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((2 · 𝑀) + 1) ∈
ℕ) |
13 | 7, 12 | syl5eqel 2705 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ) |
14 | 13 | nnnn0d 11351 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ0) |
15 | | binom 14562 |
. . . . 5
⊢ (((1 /
(tan‘𝐴)) ∈
ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 /
(tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
16 | 4, 6, 14, 15 | syl3anc 1326 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
17 | | elioore 12205 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℝ) |
18 | 17 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℝ) |
19 | 18 | recoscld 14874 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℝ) |
20 | 19 | recnd 10068 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℂ) |
21 | 18 | resincld 14873 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ) |
22 | 21 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℂ) |
23 | | mulcl 10020 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
24 | 5, 22, 23 | sylancr 695 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘𝐴))
∈ ℂ) |
25 | 20, 24 | addcld 10059 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) + (i
· (sin‘𝐴)))
∈ ℂ) |
26 | | sincosq1sgn 24250 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
27 | 26 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
28 | 27 | simpld 475 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (sin‘𝐴)) |
29 | 28 | gt0ne0d 10592 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ≠
0) |
30 | 25, 22, 29, 14 | expdivd 13022 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁))) |
31 | 20, 24, 22, 29 | divdird 10839 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) =
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴)))) |
32 | 18 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℂ) |
33 | 27 | simprd 479 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (cos‘𝐴)) |
34 | 33 | gt0ne0d 10592 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ≠
0) |
35 | | tanval 14858 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
36 | 32, 34, 35 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
37 | 36 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) = (1 /
((sin‘𝐴) /
(cos‘𝐴)))) |
38 | 22, 20, 29, 34 | recdivd 10818 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / ((sin‘𝐴) /
(cos‘𝐴))) =
((cos‘𝐴) /
(sin‘𝐴))) |
39 | 37, 38 | eqtr2d 2657 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) /
(sin‘𝐴)) = (1 /
(tan‘𝐴))) |
40 | 6, 22, 29 | divcan4d 10807 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘𝐴))
/ (sin‘𝐴)) =
i) |
41 | 39, 40 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴))) = ((1 /
(tan‘𝐴)) +
i)) |
42 | 31, 41 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) = ((1 /
(tan‘𝐴)) +
i)) |
43 | 42 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁)) |
44 | 13 | nnzd 11481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℤ) |
45 | | demoivre 14930 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
46 | 32, 44, 45 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
47 | 46 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁))) |
48 | 30, 43, 47 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁))) |
49 | 13 | nnred 11035 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℝ) |
50 | 49, 18 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑁 · 𝐴) ∈
ℝ) |
51 | 50 | recoscld 14874 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℝ) |
52 | 51 | recnd 10068 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℂ) |
53 | 50 | resincld 14873 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℝ) |
54 | 53 | recnd 10068 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℂ) |
55 | | mulcl 10020 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i ·
(sin‘(𝑁 ·
𝐴))) ∈
ℂ) |
56 | 5, 54, 55 | sylancr 695 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘(𝑁
· 𝐴))) ∈
ℂ) |
57 | 21, 28 | elrpd 11869 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ+) |
58 | 57, 44 | rpexpcld 13032 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℝ+) |
59 | 58 | rpcnd 11874 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℂ) |
60 | 58 | rpne0d 11877 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ≠ 0) |
61 | 52, 56, 59, 60 | divdird 10839 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)))) |
62 | 6, 54, 59, 60 | divassd 10836 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘(𝑁
· 𝐴))) /
((sin‘𝐴)↑𝑁)) = (i ·
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)))) |
63 | 62 | oveq2d 6666 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
64 | 48, 61, 63 | 3eqtrd 2660 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
65 | 16, 64 | eqtr3d 2658 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
66 | 65 | fveq2d 6195 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))) |
67 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗)))) |
68 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗)))) |
69 | 68 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗))))) |
70 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗)))) |
71 | 69, 70 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
72 | 67, 71 | oveq12d 6668 |
. . . . . 6
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
73 | 72 | fveq2d 6195 |
. . . . 5
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
74 | | fzfid 12772 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑀) ∈
Fin) |
75 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
76 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
77 | 76 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0) |
78 | | nn0mulcl 11329 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
79 | 75, 77, 78 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℕ0) |
80 | 79 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℝ) |
81 | 11 | nnred 11035 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℝ) |
82 | 81 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℝ) |
83 | 49 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ) |
84 | | elfzle2 12345 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀) |
85 | 84 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀) |
86 | 77 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ) |
87 | | nnre 11027 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
88 | 87 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ) |
89 | | 2re 11090 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
90 | | 2pos 11112 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
91 | 89, 90 | pm3.2i 471 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ 0 < 2) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ
∧ 0 < 2)) |
93 | | lemul2 10876 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
94 | 86, 88, 92, 93 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
95 | 85, 94 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀)) |
96 | 82 | lep1d 10955 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1)) |
97 | 96, 7 | syl6breqr 4695 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁) |
98 | 80, 82, 83, 95, 97 | letrd 10194 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁) |
99 | | nn0uz 11722 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
100 | 79, 99 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
(ℤ≥‘0)) |
101 | 44 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ) |
102 | | elfz5 12334 |
. . . . . . . . . . 11
⊢ (((2
· 𝑘) ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
103 | 100, 101,
102 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
104 | 98, 103 | mpbird 247 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁)) |
105 | | fznn0sub2 12446 |
. . . . . . . . 9
⊢ ((2
· 𝑘) ∈
(0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
107 | 106 | ex 450 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))) |
108 | 13 | nncnd 11036 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℂ) |
109 | 108 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ) |
110 | | 2cn 11091 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
111 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ) |
112 | 111 | zcnd 11483 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ) |
113 | 112 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ) |
114 | | mulcl 10020 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ) → (2 · 𝑘) ∈ ℂ) |
115 | 110, 113,
114 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ) |
116 | 112 | ssriv 3607 |
. . . . . . . . . . . 12
⊢
(0...𝑀) ⊆
ℂ |
117 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀)) |
118 | 116, 117 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ) |
119 | | mulcl 10020 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑚
∈ ℂ) → (2 · 𝑚) ∈ ℂ) |
120 | 110, 118,
119 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ) |
121 | 109, 115,
120 | subcanad 10435 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚))) |
122 | | 2cnne0 11242 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠
0)) |
124 | | mulcan 10664 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
125 | 113, 118,
123, 124 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
126 | 121, 125 | bitrd 268 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)) |
127 | 126 | ex 450 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))) |
128 | 107, 127 | dom2lem 7995 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁)) |
129 | | f1f1orn 6148 |
. . . . . 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 6658 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
132 | 131 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗))) |
133 | | eqid 2622 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) |
134 | | ovex 6678 |
. . . . . . 7
⊢ (𝑁 − (2 · 𝑗)) ∈ V |
135 | 132, 133,
134 | fvmpt 6282 |
. . . . . 6
⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
136 | 135 | adantl 482 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
137 | | f1f 6101 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁)) |
138 | 128, 137 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁)) |
139 | | frn 6053 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁)) |
140 | 138, 139 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁)) |
141 | 140 | sselda 3603 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
142 | | bccl2 13110 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ) |
143 | 142 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ) |
144 | 143 | nncnd 11036 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ) |
145 | 2 | rprecred 11883 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ) |
146 | | fznn0sub 12373 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈
ℕ0) |
147 | | reexpcl 12877 |
. . . . . . . . . . . 12
⊢ (((1 /
(tan‘𝐴)) ∈
ℝ ∧ (𝑁 −
𝑚) ∈
ℕ0) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
148 | 145, 146,
147 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
149 | 148 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ) |
150 | | elfznn0 12433 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0) |
151 | 150 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0) |
152 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ 𝑚
∈ ℕ0) → (i↑𝑚) ∈ ℂ) |
153 | 5, 151, 152 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈
ℂ) |
154 | 149, 153 | mulcld 10060 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((1 /
(tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ) |
155 | 144, 154 | mulcld 10060 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
156 | 141, 155 | syldan 487 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
157 | 156 | imcld 13935 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ) |
158 | 157 | recnd 10068 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ) |
159 | 73, 74, 130, 136, 158 | fsumf1o 14454 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
160 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
161 | 143 | nnred 11035 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ) |
162 | 160, 161 | sylan2 491 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ) |
163 | 160, 148 | sylan2 491 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
164 | | eldif 3584 |
. . . . . . . . 9
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
165 | | elfzelz 12342 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ) |
166 | 165 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ) |
167 | | zeo 11463 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨
((𝑚 + 1) / 2) ∈
ℤ)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈
ℤ)) |
169 | | i2 12965 |
. . . . . . . . . . . . . . . . . 18
⊢
(i↑2) = -1 |
170 | 169 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢
((i↑2)↑(𝑚
/ 2)) = (-1↑(𝑚 /
2)) |
171 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℤ) |
172 | 150 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
173 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
174 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ 𝑚) |
175 | | divge0 10892 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 ≤ (𝑚 / 2)) |
176 | 89, 90, 175 | mpanr12 721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) → 0 ≤ (𝑚 / 2)) |
177 | 173, 174,
176 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ (𝑚 /
2)) |
178 | 172, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2)) |
179 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 / 2) ∈ ℕ0
↔ ((𝑚 / 2) ∈
ℤ ∧ 0 ≤ (𝑚 /
2))) |
180 | 171, 178,
179 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℕ0) |
181 | | expmul 12905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) →
(i↑(2 · (𝑚 /
2))) = ((i↑2)↑(𝑚
/ 2))) |
182 | 5, 75, 181 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 / 2) ∈ ℕ0
→ (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2))) |
183 | 180, 182 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
((i↑2)↑(𝑚 /
2))) |
184 | 172 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
185 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ≠
0 |
186 | | divcan2 10693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚) |
187 | 110, 185,
186 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℂ → (2
· (𝑚 / 2)) = 𝑚) |
188 | 184, 187 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 ·
(𝑚 / 2)) = 𝑚) |
189 | 188 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
(i↑𝑚)) |
190 | 183, 189 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) →
((i↑2)↑(𝑚 / 2)) =
(i↑𝑚)) |
191 | 170, 190 | syl5eqr 2670 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚)) |
192 | | neg1rr 11125 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
ℝ |
193 | | reexpcl 12877 |
. . . . . . . . . . . . . . . . 17
⊢ ((-1
∈ ℝ ∧ (𝑚 /
2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ) |
194 | 192, 180,
193 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈
ℝ) |
195 | 191, 194 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈
ℝ) |
196 | 195 | expr 643 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈
ℝ)) |
197 | 146 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈
ℕ0) |
198 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → (𝑁 − 𝑚) ∈ ℝ) |
199 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
(𝑁 − 𝑚)) |
200 | | divge0 10892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ ((𝑁 −
𝑚) / 2)) |
201 | 89, 90, 200 | mpanr12 721 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2)) |
202 | 198, 199,
201 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
((𝑁 − 𝑚) / 2)) |
203 | 197, 202 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
((𝑁 − 𝑚) / 2)) |
204 | 197 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ) |
205 | 49 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℝ) |
206 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈
ℝ) |
208 | 150 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
209 | 208, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
𝑚) |
210 | 208 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℝ) |
211 | 205, 210 | subge02d 10619 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤
𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁)) |
212 | 209, 211 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁) |
213 | 205 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1)) |
214 | 204, 205,
207, 212, 213 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1)) |
215 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
· 1) = 2 |
216 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 = (1 +
1) |
217 | 215, 216 | eqtr2i 2645 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 + 1) =
(2 · 1) |
218 | 217 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
· 𝑀) + (1 + 1)) =
((2 · 𝑀) + (2
· 1)) |
219 | 7 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1) |
220 | 11 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℂ) |
221 | 220 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· 𝑀) ∈
ℂ) |
222 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈
ℂ) |
223 | 221, 222,
222 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· 𝑀) + 1) + 1) = ((2
· 𝑀) + (1 +
1))) |
224 | 219, 223 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1))) |
225 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈
ℂ) |
226 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
227 | 226 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℂ) |
228 | 225, 227,
222 | adddid 10064 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) = ((2
· 𝑀) + (2 ·
1))) |
229 | 218, 224,
228 | 3eqtr4a 2682 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1))) |
230 | 214, 229 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1))) |
231 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
232 | 231 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℤ) |
233 | 232 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℤ) |
234 | 233 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℝ) |
235 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℝ ∧ 0 < 2)) |
236 | | ltdivmul 10898 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
237 | 204, 234,
235, 236 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
238 | 230, 237 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1)) |
239 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℂ) |
240 | 208 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
241 | 239, 240,
222 | pnpcan2d 10430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚)) |
242 | 229 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
243 | 241, 242 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
244 | 243 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2)) |
245 | 233 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℂ) |
246 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℂ ∧ (𝑀 +
1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ) |
247 | 110, 245,
246 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) ∈
ℂ) |
248 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℂ → (𝑚 + 1) ∈
ℂ) |
249 | 240, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈
ℂ) |
250 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℂ ∧ 2 ≠ 0)) |
251 | | divsubdir 10721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· (𝑀 + 1)) ∈
ℂ ∧ (𝑚 + 1)
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 ·
(𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 ·
(𝑀 + 1)) / 2) −
((𝑚 + 1) /
2))) |
252 | 247, 249,
250, 251 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) −
(𝑚 + 1)) / 2) = (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) /
2))) |
253 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠
0) |
254 | 245, 225,
253 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2
· (𝑀 + 1)) / 2) =
(𝑀 + 1)) |
255 | 254 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) / 2)) =
((𝑀 + 1) − ((𝑚 + 1) / 2))) |
256 | 244, 252,
255 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2))) |
257 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈
ℤ) |
258 | 233, 257 | zsubcld 11487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈
ℤ) |
259 | 256, 258 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ) |
260 | | zleltp1 11428 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
261 | 259, 232,
260 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
262 | 238, 261 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀) |
263 | | 0zd 11389 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈
ℤ) |
264 | | elfz 12332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁 − 𝑚) / 2) ∧ ((𝑁 − 𝑚) / 2) ≤ 𝑀))) |
265 | 259, 263,
232, 264 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁 − 𝑚) / 2) ∧ ((𝑁 − 𝑚) / 2) ≤ 𝑀))) |
266 | 203, 262,
265 | mpbir2and 957 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) |
267 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2))) |
268 | 267 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
269 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V |
270 | 268, 133,
269 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
271 | 266, 270 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
272 | 197 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ) |
273 | 272, 225,
253 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚)) |
274 | 273 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚))) |
275 | 239, 240 | nncand 10397 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚) |
276 | 271, 274,
275 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚) |
277 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀)) |
278 | 138, 277 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀)) |
279 | 278 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀)) |
280 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
281 | 279, 266,
280 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
282 | 276, 281 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
283 | 282 | expr 643 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
284 | 196, 283 | orim12d 883 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ)
→ ((i↑𝑚) ∈
ℝ ∨ 𝑚 ∈ ran
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))) |
285 | 168, 284 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
286 | 285 | orcomd 403 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ)) |
287 | 286 | ord 392 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ)) |
288 | 287 | impr 649 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
289 | 164, 288 | sylan2b 492 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
290 | 163, 289 | remulcld 10070 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ) |
291 | 162, 290 | remulcld 10070 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ) |
292 | 291 | reim0d 13965 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0) |
293 | | fzfid 12772 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑁) ∈
Fin) |
294 | 140, 158,
292, 293 | fsumss 14456 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
295 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑁 ∈
ℕ0) |
296 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
297 | 296 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) |
298 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ0 ∧ 𝑗 ∈ ℕ0) → (2
· 𝑗) ∈
ℕ0) |
299 | 75, 297, 298 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℕ0) |
300 | 299 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℤ) |
301 | | bccl 13109 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) ∈
ℕ0) |
302 | 295, 300,
301 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈
ℕ0) |
303 | 302 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ) |
304 | | fznn0sub 12373 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈
ℕ0) |
305 | 304 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈
ℕ0) |
306 | | reexpcl 12877 |
. . . . . . . . . . . . . 14
⊢ ((-1
∈ ℝ ∧ (𝑀
− 𝑗) ∈
ℕ0) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
307 | 192, 305,
306 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
308 | 303, 307 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ) |
309 | | 2z 11409 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
310 | | znegcl 11412 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
311 | 309, 310 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ -2 ∈
ℤ |
312 | | rpexpcl 12879 |
. . . . . . . . . . . . . . 15
⊢
(((tan‘𝐴)
∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈
ℝ+) |
313 | 2, 311, 312 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ+) |
314 | 313 | rpred 11872 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ) |
315 | | reexpcl 12877 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0)
→ (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ) |
316 | 314, 296,
315 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℝ) |
317 | 308, 316 | remulcld 10070 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) |
318 | 317 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
319 | | mulcl 10020 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
320 | 5, 318, 319 | sylancr 695 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
321 | 320 | addid2d 10237 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) |
322 | 302 | nn0cnd 11353 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ) |
323 | 307 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ) |
324 | 316 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℂ) |
325 | 322, 323,
324 | mulassd 10063 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
326 | 325 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
327 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → i ∈
ℂ) |
328 | 323, 324 | mulcld 10060 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
329 | 327, 322,
328 | mul12d 10245 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
330 | 326, 329 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
331 | | bccmpl 13096 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
332 | 295, 300,
331 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
333 | 108 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ) |
334 | 299 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℂ) |
335 | 333, 334 | nncand 10397 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗)) |
336 | 335 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
337 | 2 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℝ+) |
338 | 337 | rpcnd 11874 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℂ) |
339 | | expneg 12868 |
. . . . . . . . . . . . . 14
⊢
(((tan‘𝐴)
∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) →
((tan‘𝐴)↑-(2
· 𝑗)) = (1 /
((tan‘𝐴)↑(2
· 𝑗)))) |
340 | 338, 299,
339 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
341 | 297 | nn0cnd 11353 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ) |
342 | | mulneg1 10466 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗)) |
343 | 110, 341,
342 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗)) |
344 | 343 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗))) |
345 | 337 | rpne0d 11877 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0) |
346 | 338, 345,
300 | exprecd 13016 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
347 | 340, 344,
346 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
348 | 311 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → -2 ∈
ℤ) |
349 | 297 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ) |
350 | | expmulz 12906 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)
∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧
𝑗 ∈ ℤ)) →
((tan‘𝐴)↑(-2
· 𝑗)) =
(((tan‘𝐴)↑-2)↑𝑗)) |
351 | 338, 345,
348, 349, 350 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗)) |
352 | 336, 347,
351 | 3eqtr2d 2662 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗)) |
353 | 7 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗)) |
354 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℕ) |
355 | 354 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℂ) |
356 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 1 ∈
ℂ) |
357 | 355, 356,
334 | addsubd 10413 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
358 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℂ) |
359 | 226 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ) |
360 | 358, 359,
341 | subdid 10486 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗))) |
361 | 360 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
362 | 357, 361 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
363 | 353, 362 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
364 | 363 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 ·
(𝑀 − 𝑗)) + 1))) |
365 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (𝑀 − 𝑗) ∈ ℕ0) → (2
· (𝑀 − 𝑗)) ∈
ℕ0) |
366 | 75, 305, 365 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈
ℕ0) |
367 | | expp1 12867 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ0) →
(i↑((2 · (𝑀
− 𝑗)) + 1)) =
((i↑(2 · (𝑀
− 𝑗))) ·
i)) |
368 | 5, 366, 367 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑((2 ·
(𝑀 − 𝑗)) + 1)) = ((i↑(2 ·
(𝑀 − 𝑗))) ·
i)) |
369 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℕ0) |
370 | 327, 305,
369 | expmuld 13011 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗))) |
371 | 169 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢
((i↑2)↑(𝑀
− 𝑗)) =
(-1↑(𝑀 − 𝑗)) |
372 | 370, 371 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗))) |
373 | 372 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i↑(2 ·
(𝑀 − 𝑗))) · i) =
((-1↑(𝑀 − 𝑗)) · i)) |
374 | 364, 368,
373 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i)) |
375 | | mulcom 10022 |
. . . . . . . . . . . . 13
⊢
(((-1↑(𝑀
− 𝑗)) ∈ ℂ
∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
376 | 323, 5, 375 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
377 | 374, 376 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i ·
(-1↑(𝑀 − 𝑗)))) |
378 | 352, 377 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((1 /
(tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗))))) |
379 | | mulcl 10020 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
380 | 5, 323, 379 | sylancr 695 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
381 | 380, 324 | mulcomd 10061 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i ·
(-1↑(𝑀 − 𝑗))))) |
382 | 327, 323,
324 | mulassd 10063 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
383 | 378, 381,
382 | 3eqtr2rd 2663 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
384 | 332, 383 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
385 | 321, 330,
384 | 3eqtrd 2660 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
386 | 385 | fveq2d 6195 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
387 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
388 | | crim 13855 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 +
(i · (((𝑁C(2
· 𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
389 | 387, 317,
388 | sylancr 695 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
390 | 386, 389 | eqtr3d 2658 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
391 | 390 | sumeq2dv 14433 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
392 | 159, 294,
391 | 3eqtr3d 2664 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
393 | 293, 155 | fsumim 14541 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
394 | 313 | rpcnd 11874 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℂ) |
395 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗)) |
396 | 395 | oveq2d 6666 |
. . . . . 6
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
397 | 396 | sumeq2sdv 14435 |
. . . . 5
⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
398 | | basel.p |
. . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
399 | | sumex 14418 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V |
400 | 397, 398,
399 | fvmpt 6282 |
. . . 4
⊢
(((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
401 | 394, 400 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
402 | 392, 393,
401 | 3eqtr4d 2666 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2))) |
403 | 51, 58 | rerpdivcld 11903 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
404 | 53, 58 | rerpdivcld 11903 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
405 | 403, 404 | crimd 13972 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |
406 | 66, 402, 405 | 3eqtr3d 2664 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |