Step | Hyp | Ref
| Expression |
1 | | tanrpcl 25076 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(tan‘𝐴) ∈
ℝ+) |
2 | 1 | adantl 484 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) ∈
ℝ+) |
3 | 2 | rpreccld 12428 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ+) |
4 | 3 | rpcnd 12420 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℂ) |
5 | | ax-icn 10582 |
. . . . . 6
⊢ i ∈
ℂ |
6 | 5 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
i ∈ ℂ) |
7 | | basel.n |
. . . . . . 7
⊢ 𝑁 = ((2 · 𝑀) + 1) |
8 | | 2nn 11697 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
9 | | simpl 485 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑀 ∈
ℕ) |
10 | | nnmulcl 11648 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
11 | 8, 9, 10 | sylancr 589 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℕ) |
12 | 11 | peano2nnd 11641 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((2 · 𝑀) + 1) ∈
ℕ) |
13 | 7, 12 | eqeltrid 2917 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ) |
14 | 13 | nnnn0d 11942 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℕ0) |
15 | | binom 15170 |
. . . . 5
⊢ (((1 /
(tan‘𝐴)) ∈
ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 /
(tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
16 | 4, 6, 14, 15 | syl3anc 1367 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) |
17 | | elioore 12755 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (0(,)(π / 2)) →
𝐴 ∈
ℝ) |
18 | 17 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℝ) |
19 | 18 | recoscld 15482 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℝ) |
20 | 19 | recnd 10655 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ∈
ℂ) |
21 | 18 | resincld 15481 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ) |
22 | 21 | recnd 10655 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℂ) |
23 | | mulcl 10607 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i ·
(sin‘𝐴)) ∈
ℂ) |
24 | 5, 22, 23 | sylancr 589 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘𝐴))
∈ ℂ) |
25 | 20, 24 | addcld 10646 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) + (i
· (sin‘𝐴)))
∈ ℂ) |
26 | | sincosq1sgn 25070 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
27 | 26 | adantl 484 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
28 | 27 | simpld 497 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (sin‘𝐴)) |
29 | 28 | gt0ne0d 11190 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ≠
0) |
30 | 25, 22, 29, 14 | expdivd 13514 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁))) |
31 | 20, 24, 22, 29 | divdird 11440 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) =
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴)))) |
32 | 18 | recnd 10655 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝐴 ∈
ℂ) |
33 | 27 | simprd 498 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
0 < (cos‘𝐴)) |
34 | 33 | gt0ne0d 11190 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘𝐴) ≠
0) |
35 | | tanval 15466 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(cos‘𝐴) ≠ 0)
→ (tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
36 | 32, 34, 35 | syl2anc 586 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(tan‘𝐴) =
((sin‘𝐴) /
(cos‘𝐴))) |
37 | 36 | oveq2d 7158 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) = (1 /
((sin‘𝐴) /
(cos‘𝐴)))) |
38 | 22, 20, 29, 34 | recdivd 11419 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / ((sin‘𝐴) /
(cos‘𝐴))) =
((cos‘𝐴) /
(sin‘𝐴))) |
39 | 37, 38 | eqtr2d 2857 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘𝐴) /
(sin‘𝐴)) = (1 /
(tan‘𝐴))) |
40 | 6, 22, 29 | divcan4d 11408 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘𝐴))
/ (sin‘𝐴)) =
i) |
41 | 39, 40 | oveq12d 7160 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) /
(sin‘𝐴)) + ((i
· (sin‘𝐴)) /
(sin‘𝐴))) = ((1 /
(tan‘𝐴)) +
i)) |
42 | 31, 41 | eqtrd 2856 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴)) = ((1 /
(tan‘𝐴)) +
i)) |
43 | 42 | oveq1d 7157 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴))) /
(sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁)) |
44 | 13 | nnzd 12073 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℤ) |
45 | | demoivre 15538 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
46 | 32, 44, 45 | syl2anc 586 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴))))) |
47 | 46 | oveq1d 7157 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((((cos‘𝐴) + (i
· (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁))) |
48 | 30, 43, 47 | 3eqtr3d 2864 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁))) |
49 | 13 | nnred 11639 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℝ) |
50 | 49, 18 | remulcld 10657 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑁 · 𝐴) ∈
ℝ) |
51 | 50 | recoscld 15482 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℝ) |
52 | 51 | recnd 10655 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(cos‘(𝑁 ·
𝐴)) ∈
ℂ) |
53 | 50 | resincld 15481 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℝ) |
54 | 53 | recnd 10655 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘(𝑁 ·
𝐴)) ∈
ℂ) |
55 | | mulcl 10607 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i ·
(sin‘(𝑁 ·
𝐴))) ∈
ℂ) |
56 | 5, 54, 55 | sylancr 589 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(i · (sin‘(𝑁
· 𝐴))) ∈
ℂ) |
57 | 21, 28 | elrpd 12415 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(sin‘𝐴) ∈
ℝ+) |
58 | 57, 44 | rpexpcld 13598 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℝ+) |
59 | 58 | rpcnd 12420 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ∈
ℂ) |
60 | 58 | rpne0d 12423 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘𝐴)↑𝑁) ≠ 0) |
61 | 52, 56, 59, 60 | divdird 11440 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) + (i ·
(sin‘(𝑁 ·
𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)))) |
62 | 6, 54, 59, 60 | divassd 11437 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((i · (sin‘(𝑁
· 𝐴))) /
((sin‘𝐴)↑𝑁)) = (i ·
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)))) |
63 | 62 | oveq2d 7158 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
64 | 48, 61, 63 | 3eqtrd 2860 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(((1 / (tan‘𝐴)) +
i)↑𝑁) =
(((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
65 | 16, 64 | eqtr3d 2858 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) |
66 | 65 | fveq2d 6660 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))) |
67 | | oveq2 7150 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗)))) |
68 | | oveq2 7150 |
. . . . . . . . 9
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗)))) |
69 | 68 | oveq2d 7158 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗))))) |
70 | | oveq2 7150 |
. . . . . . . 8
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗)))) |
71 | 69, 70 | oveq12d 7160 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
72 | 67, 71 | oveq12d 7160 |
. . . . . 6
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
73 | 72 | fveq2d 6660 |
. . . . 5
⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
74 | | fzfid 13331 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑀) ∈
Fin) |
75 | | 2nn0 11901 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
76 | | elfznn0 12990 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
77 | 76 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0) |
78 | | nn0mulcl 11920 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝑘 ∈ ℕ0) → (2
· 𝑘) ∈
ℕ0) |
79 | 75, 77, 78 | sylancr 589 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℕ0) |
80 | 79 | nn0red 11943 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
ℝ) |
81 | 11 | nnred 11639 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℝ) |
82 | 81 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℝ) |
83 | 49 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ) |
84 | | elfzle2 12901 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀) |
85 | 84 | adantl 484 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀) |
86 | 77 | nn0red 11943 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ) |
87 | | nnre 11631 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
88 | 87 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ) |
89 | | 2re 11698 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
90 | | 2pos 11727 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
91 | 89, 90 | pm3.2i 473 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ 0 < 2) |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ
∧ 0 < 2)) |
93 | | lemul2 11479 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
94 | 86, 88, 92, 93 | syl3anc 1367 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀))) |
95 | 85, 94 | mpbid 234 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀)) |
96 | 82 | lep1d 11557 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1)) |
97 | 96, 7 | breqtrrdi 5094 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁) |
98 | 80, 82, 83, 95, 97 | letrd 10783 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁) |
99 | | nn0uz 12267 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
100 | 79, 99 | eleqtrdi 2923 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈
(ℤ≥‘0)) |
101 | 44 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ) |
102 | | elfz5 12890 |
. . . . . . . . . . 11
⊢ (((2
· 𝑘) ∈
(ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
103 | 100, 101,
102 | syl2anc 586 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁)) |
104 | 98, 103 | mpbird 259 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁)) |
105 | | fznn0sub2 13004 |
. . . . . . . . 9
⊢ ((2
· 𝑘) ∈
(0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)) |
107 | 106 | ex 415 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))) |
108 | 13 | nncnd 11640 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
𝑁 ∈
ℂ) |
109 | 108 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ) |
110 | | 2cn 11699 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
111 | | elfzelz 12898 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ) |
112 | 111 | zcnd 12075 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ) |
113 | 112 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ) |
114 | | mulcl 10607 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ) → (2 · 𝑘) ∈ ℂ) |
115 | 110, 113,
114 | sylancr 589 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ) |
116 | 112 | ssriv 3959 |
. . . . . . . . . . . 12
⊢
(0...𝑀) ⊆
ℂ |
117 | | simprr 771 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀)) |
118 | 116, 117 | sseldi 3953 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ) |
119 | | mulcl 10607 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑚
∈ ℂ) → (2 · 𝑚) ∈ ℂ) |
120 | 110, 118,
119 | sylancr 589 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ) |
121 | 109, 115,
120 | subcanad 11026 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚))) |
122 | | 2cnne0 11834 |
. . . . . . . . . . 11
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠
0)) |
124 | | mulcan 11263 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
125 | 113, 118,
123, 124 | syl3anc 1367 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚)) |
126 | 121, 125 | bitrd 281 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)) |
127 | 126 | ex 415 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))) |
128 | 107, 127 | dom2lem 8535 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁)) |
129 | | f1f1orn 6612 |
. . . . . 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 7150 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗)) |
132 | 131 | oveq2d 7158 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗))) |
133 | | eqid 2821 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) |
134 | | ovex 7175 |
. . . . . . 7
⊢ (𝑁 − (2 · 𝑗)) ∈ V |
135 | 132, 133,
134 | fvmpt 6754 |
. . . . . 6
⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
136 | 135 | adantl 484 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗))) |
137 | 106 | fmpttd 6865 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁)) |
138 | 137 | frnd 6507 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁)) |
139 | 138 | sselda 3955 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
140 | | bccl2 13673 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ) |
141 | 140 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ) |
142 | 141 | nncnd 11640 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ) |
143 | 2 | rprecred 12429 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(1 / (tan‘𝐴)) ∈
ℝ) |
144 | | fznn0sub 12929 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈
ℕ0) |
145 | | reexpcl 13436 |
. . . . . . . . . . . 12
⊢ (((1 /
(tan‘𝐴)) ∈
ℝ ∧ (𝑁 −
𝑚) ∈
ℕ0) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
146 | 143, 144,
145 | syl2an 597 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
147 | 146 | recnd 10655 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ) |
148 | | elfznn0 12990 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0) |
149 | 148 | adantl 484 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0) |
150 | | expcl 13437 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ 𝑚
∈ ℕ0) → (i↑𝑚) ∈ ℂ) |
151 | 5, 149, 150 | sylancr 589 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈
ℂ) |
152 | 147, 151 | mulcld 10647 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((1 /
(tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ) |
153 | 142, 152 | mulcld 10647 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
154 | 139, 153 | syldan 593 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ) |
155 | 154 | imcld 14539 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ) |
156 | 155 | recnd 10655 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ) |
157 | 73, 74, 130, 136, 156 | fsumf1o 15065 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
158 | | eldifi 4091 |
. . . . . . . 8
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁)) |
159 | 141 | nnred 11639 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ) |
160 | 158, 159 | sylan2 594 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ) |
161 | 158, 146 | sylan2 594 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ) |
162 | | eldif 3934 |
. . . . . . . . 9
⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
163 | | elfzelz 12898 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ) |
164 | 163 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ) |
165 | | zeo 12055 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨
((𝑚 + 1) / 2) ∈
ℤ)) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈
ℤ)) |
167 | | i2 13555 |
. . . . . . . . . . . . . . . . . 18
⊢
(i↑2) = -1 |
168 | 167 | oveq1i 7152 |
. . . . . . . . . . . . . . . . 17
⊢
((i↑2)↑(𝑚
/ 2)) = (-1↑(𝑚 /
2)) |
169 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℤ) |
170 | 148 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
171 | | nn0re 11893 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
172 | | nn0ge0 11909 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ 𝑚) |
173 | | divge0 11495 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) ∧ (2 ∈ ℝ
∧ 0 < 2)) → 0 ≤ (𝑚 / 2)) |
174 | 89, 90, 173 | mpanr12 703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 ∈ ℝ ∧ 0 ≤
𝑚) → 0 ≤ (𝑚 / 2)) |
175 | 171, 172,
174 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ (𝑚 /
2)) |
176 | 170, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2)) |
177 | | elnn0z 11981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 / 2) ∈ ℕ0
↔ ((𝑚 / 2) ∈
ℤ ∧ 0 ≤ (𝑚 /
2))) |
178 | 169, 176,
177 | sylanbrc 585 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈
ℕ0) |
179 | | expmul 13464 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) →
(i↑(2 · (𝑚 /
2))) = ((i↑2)↑(𝑚
/ 2))) |
180 | 5, 75, 178, 179 | mp3an12i 1461 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
((i↑2)↑(𝑚 /
2))) |
181 | 170 | nn0cnd 11944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
182 | | 2ne0 11728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ≠
0 |
183 | | divcan2 11292 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚) |
184 | 110, 182,
183 | mp3an23 1449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℂ → (2
· (𝑚 / 2)) = 𝑚) |
185 | 181, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 ·
(𝑚 / 2)) = 𝑚) |
186 | 185 | oveq2d 7158 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2
· (𝑚 / 2))) =
(i↑𝑚)) |
187 | 180, 186 | eqtr3d 2858 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) →
((i↑2)↑(𝑚 / 2)) =
(i↑𝑚)) |
188 | 168, 187 | syl5eqr 2870 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚)) |
189 | | neg1rr 11739 |
. . . . . . . . . . . . . . . . 17
⊢ -1 ∈
ℝ |
190 | | reexpcl 13436 |
. . . . . . . . . . . . . . . . 17
⊢ ((-1
∈ ℝ ∧ (𝑚 /
2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ) |
191 | 189, 178,
190 | sylancr 589 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈
ℝ) |
192 | 188, 191 | eqeltrrd 2914 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈
ℝ) |
193 | 192 | expr 459 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈
ℝ)) |
194 | 144 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈
ℕ0) |
195 | | nn0re 11893 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → (𝑁 − 𝑚) ∈ ℝ) |
196 | | nn0ge0 11909 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
(𝑁 − 𝑚)) |
197 | | divge0 11495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 ≤ ((𝑁 −
𝑚) / 2)) |
198 | 89, 90, 197 | mpanr12 703 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2)) |
199 | 195, 196,
198 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 − 𝑚) ∈ ℕ0 → 0 ≤
((𝑁 − 𝑚) / 2)) |
200 | 194, 199 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
((𝑁 − 𝑚) / 2)) |
201 | 194 | nn0red 11943 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ) |
202 | 49 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℝ) |
203 | | peano2re 10799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) |
204 | 202, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈
ℝ) |
205 | 148 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℕ0) |
206 | 205, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤
𝑚) |
207 | 205 | nn0red 11943 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℝ) |
208 | 202, 207 | subge02d 11218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤
𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁)) |
209 | 206, 208 | mpbid 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁) |
210 | 202 | ltp1d 11556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1)) |
211 | 201, 202,
204, 209, 210 | lelttrd 10784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1)) |
212 | | 2t1e2 11787 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2
· 1) = 2 |
213 | | df-2 11687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 = (1 +
1) |
214 | 212, 213 | eqtr2i 2845 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 + 1) =
(2 · 1) |
215 | 214 | oveq2i 7153 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
· 𝑀) + (1 + 1)) =
((2 · 𝑀) + (2
· 1)) |
216 | 7 | oveq1i 7152 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1) |
217 | 11 | nncnd 11640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(2 · 𝑀) ∈
ℂ) |
218 | 217 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· 𝑀) ∈
ℂ) |
219 | | 1cnd 10622 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈
ℂ) |
220 | 218, 219,
219 | addassd 10649 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· 𝑀) + 1) + 1) = ((2
· 𝑀) + (1 +
1))) |
221 | 216, 220 | syl5eq 2868 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1))) |
222 | | 2cnd 11702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈
ℂ) |
223 | | nncn 11632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
224 | 223 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℂ) |
225 | 222, 224,
219 | adddid 10651 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) = ((2
· 𝑀) + (2 ·
1))) |
226 | 215, 221,
225 | 3eqtr4a 2882 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1))) |
227 | 211, 226 | breqtrd 5078 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1))) |
228 | | nnz 11991 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
229 | 228 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈
ℤ) |
230 | 229 | peano2zd 12077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℤ) |
231 | 230 | zred 12074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℝ) |
232 | 91 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℝ ∧ 0 < 2)) |
233 | | ltdivmul 11501 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
234 | 201, 231,
232, 233 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1)))) |
235 | 227, 234 | mpbird 259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1)) |
236 | 108 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈
ℂ) |
237 | 205 | nn0cnd 11944 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈
ℂ) |
238 | 236, 237,
219 | pnpcan2d 11021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚)) |
239 | 226 | oveq1d 7157 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
240 | 238, 239 | eqtr3d 2858 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1))) |
241 | 240 | oveq1d 7157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2)) |
242 | 230 | zcnd 12075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈
ℂ) |
243 | | mulcl 10607 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℂ ∧ (𝑀 +
1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ) |
244 | 110, 242,
243 | sylancr 589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· (𝑀 + 1)) ∈
ℂ) |
245 | | peano2cn 10798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℂ → (𝑚 + 1) ∈
ℂ) |
246 | 237, 245 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈
ℂ) |
247 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈
ℂ ∧ 2 ≠ 0)) |
248 | | divsubdir 11320 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((2
· (𝑀 + 1)) ∈
ℂ ∧ (𝑚 + 1)
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 ·
(𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 ·
(𝑀 + 1)) / 2) −
((𝑚 + 1) /
2))) |
249 | 244, 246,
247, 248 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) −
(𝑚 + 1)) / 2) = (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) /
2))) |
250 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠
0) |
251 | 242, 222,
250 | divcan3d 11407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2
· (𝑀 + 1)) / 2) =
(𝑀 + 1)) |
252 | 251 | oveq1d 7157 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2
· (𝑀 + 1)) / 2)
− ((𝑚 + 1) / 2)) =
((𝑀 + 1) − ((𝑚 + 1) / 2))) |
253 | 241, 249,
252 | 3eqtrd 2860 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2))) |
254 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈
ℤ) |
255 | 230, 254 | zsubcld 12079 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈
ℤ) |
256 | 253, 255 | eqeltrd 2913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ) |
257 | | zleltp1 12020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
258 | 256, 229,
257 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1))) |
259 | 235, 258 | mpbird 259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀) |
260 | | 0zd 11980 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈
ℤ) |
261 | | elfz 12888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁 − 𝑚) / 2) ∧ ((𝑁 − 𝑚) / 2) ≤ 𝑀))) |
262 | 256, 260,
229, 261 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁 − 𝑚) / 2) ∧ ((𝑁 − 𝑚) / 2) ≤ 𝑀))) |
263 | 200, 259,
262 | mpbir2and 711 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) |
264 | | oveq2 7150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2))) |
265 | 264 | oveq2d 7158 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
266 | | ovex 7175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V |
267 | 265, 133,
266 | fvmpt 6754 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
268 | 263, 267 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2)))) |
269 | 194 | nn0cnd 11944 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ) |
270 | 269, 222,
250 | divcan2d 11404 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2
· ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚)) |
271 | 270 | oveq2d 7158 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚))) |
272 | 236, 237 | nncand 10988 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚) |
273 | 268, 271,
272 | 3eqtrd 2860 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚) |
274 | 137 | ffnd 6501 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀)) |
275 | | fnfvelrn 6834 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
276 | 274, 263,
275 | syl2an2r 683 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
277 | 273, 276 | eqeltrrd 2914 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) |
278 | 277 | expr 459 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
279 | 193, 278 | orim12d 961 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ)
→ ((i↑𝑚) ∈
ℝ ∨ 𝑚 ∈ ran
(𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))) |
280 | 166, 279 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) |
281 | 280 | orcomd 867 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ)) |
282 | 281 | ord 860 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ)) |
283 | 282 | impr 457 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
(𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
284 | 162, 283 | sylan2b 595 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ) |
285 | 161, 284 | remulcld 10657 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ) |
286 | 160, 285 | remulcld 10657 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ) |
287 | 286 | reim0d 14569 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0) |
288 | | fzfid 13331 |
. . . . 5
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(0...𝑁) ∈
Fin) |
289 | 138, 156,
287, 288 | fsumss 15067 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
290 | | elfznn0 12990 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0) |
291 | 290 | adantl 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0) |
292 | | nn0mulcl 11920 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ0 ∧ 𝑗 ∈ ℕ0) → (2
· 𝑗) ∈
ℕ0) |
293 | 75, 291, 292 | sylancr 589 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℕ0) |
294 | 293 | nn0zd 12072 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℤ) |
295 | | bccl 13672 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) ∈
ℕ0) |
296 | 14, 294, 295 | syl2an2r 683 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈
ℕ0) |
297 | 296 | nn0red 11943 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ) |
298 | | fznn0sub 12929 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈
ℕ0) |
299 | 298 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈
ℕ0) |
300 | | reexpcl 13436 |
. . . . . . . . . . . . . 14
⊢ ((-1
∈ ℝ ∧ (𝑀
− 𝑗) ∈
ℕ0) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
301 | 189, 299,
300 | sylancr 589 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ) |
302 | 297, 301 | remulcld 10657 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ) |
303 | | 2z 12001 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
304 | | znegcl 12004 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℤ → -2 ∈ ℤ) |
305 | 303, 304 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ -2 ∈
ℤ |
306 | | rpexpcl 13438 |
. . . . . . . . . . . . . . 15
⊢
(((tan‘𝐴)
∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈
ℝ+) |
307 | 2, 305, 306 | sylancl 588 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ+) |
308 | 307 | rpred 12418 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℝ) |
309 | | reexpcl 13436 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0)
→ (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ) |
310 | 308, 290,
309 | syl2an 597 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℝ) |
311 | 302, 310 | remulcld 10657 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) |
312 | 311 | recnd 10655 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
313 | | mulcl 10607 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
314 | 5, 312, 313 | sylancr 589 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ) |
315 | 314 | addid2d 10827 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) |
316 | 296 | nn0cnd 11944 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ) |
317 | 301 | recnd 10655 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ) |
318 | 310 | recnd 10655 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈
ℂ) |
319 | 316, 317,
318 | mulassd 10650 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
320 | 319 | oveq2d 7158 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
321 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → i ∈
ℂ) |
322 | 317, 318 | mulcld 10647 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) |
323 | 321, 316,
322 | mul12d 10835 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
324 | 320, 323 | eqtrd 2856 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))) |
325 | | bccmpl 13659 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · 𝑗) ∈
ℤ) → (𝑁C(2
· 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
326 | 14, 294, 325 | syl2an2r 683 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗)))) |
327 | 108 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ) |
328 | 293 | nn0cnd 11944 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈
ℂ) |
329 | 327, 328 | nncand 10988 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗)) |
330 | 329 | oveq2d 7158 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
331 | 2 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℝ+) |
332 | 331 | rpcnd 12420 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈
ℂ) |
333 | | expneg 13427 |
. . . . . . . . . . . . . 14
⊢
(((tan‘𝐴)
∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) →
((tan‘𝐴)↑-(2
· 𝑗)) = (1 /
((tan‘𝐴)↑(2
· 𝑗)))) |
334 | 332, 293,
333 | syl2anc 586 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
335 | 291 | nn0cnd 11944 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ) |
336 | | mulneg1 11062 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑗
∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗)) |
337 | 110, 335,
336 | sylancr 589 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗)) |
338 | 337 | oveq2d 7158 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗))) |
339 | 331 | rpne0d 12423 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0) |
340 | 332, 339,
294 | exprecd 13508 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗)))) |
341 | 334, 338,
340 | 3eqtr4d 2866 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗))) |
342 | 305 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → -2 ∈
ℤ) |
343 | 291 | nn0zd 12072 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ) |
344 | | expmulz 13465 |
. . . . . . . . . . . . 13
⊢
((((tan‘𝐴)
∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧
𝑗 ∈ ℤ)) →
((tan‘𝐴)↑(-2
· 𝑗)) =
(((tan‘𝐴)↑-2)↑𝑗)) |
345 | 332, 339,
342, 343, 344 | syl22anc 836 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗)) |
346 | 330, 341,
345 | 3eqtr2d 2862 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗)) |
347 | 7 | oveq1i 7152 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗)) |
348 | 11 | adantr 483 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℕ) |
349 | 348 | nncnd 11640 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈
ℂ) |
350 | | 1cnd 10622 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 1 ∈
ℂ) |
351 | 349, 350,
328 | addsubd 11004 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
352 | | 2cnd 11702 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℂ) |
353 | 223 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ) |
354 | 352, 353,
335 | subdid 11082 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗))) |
355 | 354 | oveq1d 7157 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1)) |
356 | 351, 355 | eqtr4d 2859 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
357 | 347, 356 | syl5eq 2868 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1)) |
358 | 357 | oveq2d 7158 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 ·
(𝑀 − 𝑗)) + 1))) |
359 | | nn0mulcl 11920 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ (𝑀 − 𝑗) ∈ ℕ0) → (2
· (𝑀 − 𝑗)) ∈
ℕ0) |
360 | 75, 299, 359 | sylancr 589 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈
ℕ0) |
361 | | expp1 13426 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ0) →
(i↑((2 · (𝑀
− 𝑗)) + 1)) =
((i↑(2 · (𝑀
− 𝑗))) ·
i)) |
362 | 5, 360, 361 | sylancr 589 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑((2 ·
(𝑀 − 𝑗)) + 1)) = ((i↑(2 ·
(𝑀 − 𝑗))) ·
i)) |
363 | 75 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → 2 ∈
ℕ0) |
364 | 321, 299,
363 | expmuld 13503 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗))) |
365 | 167 | oveq1i 7152 |
. . . . . . . . . . . . . . 15
⊢
((i↑2)↑(𝑀
− 𝑗)) =
(-1↑(𝑀 − 𝑗)) |
366 | 364, 365 | syl6eq 2872 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(2 ·
(𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗))) |
367 | 366 | oveq1d 7157 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i↑(2 ·
(𝑀 − 𝑗))) · i) =
((-1↑(𝑀 − 𝑗)) · i)) |
368 | 358, 362,
367 | 3eqtrd 2860 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i)) |
369 | | mulcom 10609 |
. . . . . . . . . . . . 13
⊢
(((-1↑(𝑀
− 𝑗)) ∈ ℂ
∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
370 | 317, 5, 369 | sylancl 588 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗)))) |
371 | 368, 370 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i ·
(-1↑(𝑀 − 𝑗)))) |
372 | 346, 371 | oveq12d 7160 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (((1 /
(tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗))))) |
373 | | mulcl 10607 |
. . . . . . . . . . . 12
⊢ ((i
∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
374 | 5, 317, 373 | sylancr 589 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
(-1↑(𝑀 − 𝑗))) ∈
ℂ) |
375 | 374, 318 | mulcomd 10648 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i ·
(-1↑(𝑀 − 𝑗))))) |
376 | 321, 317,
318 | mulassd 10650 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((i ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) |
377 | 372, 375,
376 | 3eqtr2rd 2863 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (i ·
((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))) |
378 | 326, 377 | oveq12d 7160 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
379 | 315, 324,
378 | 3eqtrd 2860 |
. . . . . . 7
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (0 + (i ·
(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) |
380 | 379 | fveq2d 6660 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))) |
381 | | 0re 10629 |
. . . . . . 7
⊢ 0 ∈
ℝ |
382 | | crim 14459 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 +
(i · (((𝑁C(2
· 𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
383 | 381, 311,
382 | sylancr 589 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i
· (((𝑁C(2 ·
𝑗)) ·
(-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
384 | 380, 383 | eqtr3d 2858 |
. . . . 5
⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧
𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
385 | 384 | sumeq2dv 15045 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
386 | 157, 289,
385 | 3eqtr3d 2864 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
387 | 288, 153 | fsumim 15149 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))) |
388 | 307 | rpcnd 12420 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((tan‘𝐴)↑-2)
∈ ℂ) |
389 | | oveq1 7149 |
. . . . . . 7
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗)) |
390 | 389 | oveq2d 7158 |
. . . . . 6
⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
391 | 390 | sumeq2sdv 15046 |
. . . . 5
⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
392 | | basel.p |
. . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
393 | | sumex 15029 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V |
394 | 391, 392,
393 | fvmpt 6754 |
. . . 4
⊢
(((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
395 | 388, 394 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) |
396 | 386, 387,
395 | 3eqtr4d 2866 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘Σ𝑚
∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2))) |
397 | 51, 58 | rerpdivcld 12449 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((cos‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
398 | 53, 58 | rerpdivcld 12449 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
((sin‘(𝑁 ·
𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ) |
399 | 397, 398 | crimd 14576 |
. 2
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |
400 | 66, 396, 399 | 3eqtr3d 2864 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) →
(𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))) |