MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem3 Structured version   Visualization version   GIF version

Theorem basellem3 25006
Description: Lemma for basel 25013. Using the binomial theorem and de Moivre's formula, we have the identity e↑i𝑁𝑥 / (sin𝑥)↑𝑛 = Σ𝑚 ∈ (0...𝑁)(𝑁C𝑚)(i↑𝑚)(cot𝑥)↑(𝑁𝑚), so taking imaginary parts yields sin(𝑁𝑥) / (sin𝑥)↑𝑁 = Σ𝑗 ∈ (0...𝑀)(𝑁C2𝑗)(-1)↑(𝑀𝑗) (cot𝑥)↑(-2𝑗) = 𝑃((cot𝑥)↑2), where 𝑁 = 2𝑀 + 1. (Contributed by Mario Carneiro, 30-Jul-2014.)
Hypotheses
Ref Expression
basel.n 𝑁 = ((2 · 𝑀) + 1)
basel.p 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
Assertion
Ref Expression
basellem3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Distinct variable groups:   𝑡,𝑗,𝐴   𝑗,𝑀,𝑡   𝑗,𝑁,𝑡
Allowed substitution hints:   𝑃(𝑡,𝑗)

Proof of Theorem basellem3
Dummy variables 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tanrpcl 24453 . . . . . . . 8 (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
21adantl 473 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ+)
32rpreccld 12073 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ+)
43rpcnd 12065 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5 ax-icn 10185 . . . . . 6 i ∈ ℂ
65a1i 11 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7 basel.n . . . . . . 7 𝑁 = ((2 · 𝑀) + 1)
8 2nn 11375 . . . . . . . . 9 2 ∈ ℕ
9 simpl 474 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10 nnmulcl 11233 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
118, 9, 10sylancr 698 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
1211peano2nnd 11227 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
137, 12syl5eqel 2841 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
1413nnnn0d 11541 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ0)
15 binom 14759 . . . . 5 (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
164, 6, 14, 15syl3anc 1477 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
17 elioore 12396 . . . . . . . . . . 11 (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
1817adantl 473 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
1918recoscld 15071 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
2019recnd 10258 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
2118resincld 15070 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
2221recnd 10258 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23 mulcl 10210 . . . . . . . . 9 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
245, 22, 23sylancr 698 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
2520, 24addcld 10249 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26 sincosq1sgn 24447 . . . . . . . . . 10 (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2726adantl 473 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2827simpld 477 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
2928gt0ne0d 10782 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
3025, 22, 29, 14expdivd 13214 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
3120, 24, 22, 29divdird 11029 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
3218recnd 10258 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
3327simprd 482 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
3433gt0ne0d 10782 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35 tanval 15055 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3632, 34, 35syl2anc 696 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3736oveq2d 6827 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
3822, 20, 29, 34recdivd 11008 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
3937, 38eqtr2d 2793 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
406, 22, 29divcan4d 10997 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
4139, 40oveq12d 6829 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
4231, 41eqtrd 2792 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
4342oveq1d 6826 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
4413nnzd 11671 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45 demoivre 15127 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4632, 44, 45syl2anc 696 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4746oveq1d 6826 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4830, 43, 473eqtr3d 2800 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4913nnred 11225 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
5049, 18remulcld 10260 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
5150recoscld 15071 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
5251recnd 10258 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
5350resincld 15070 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
5453recnd 10258 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55 mulcl 10210 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
565, 54, 55sylancr 698 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
5721, 28elrpd 12060 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ+)
5857, 44rpexpcld 13224 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ+)
5958rpcnd 12065 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
6058rpne0d 12068 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
6152, 56, 59, 60divdird 11029 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
626, 54, 59, 60divassd 11026 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
6362oveq2d 6827 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6448, 61, 633eqtrd 2796 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6516, 64eqtr3d 2794 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6665fveq2d 6354 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67 oveq2 6819 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68 oveq2 6819 . . . . . . . . 9 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
6968oveq2d 6827 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70 oveq2 6819 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
7169, 70oveq12d 6829 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
7267, 71oveq12d 6829 . . . . . 6 (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
7372fveq2d 6354 . . . . 5 (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74 fzfid 12964 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75 2nn0 11499 . . . . . . . . . . . . 13 2 ∈ ℕ0
76 elfznn0 12624 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0)
7776adantl 473 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0)
78 nn0mulcl 11519 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
7975, 77, 78sylancr 698 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ0)
8079nn0red 11542 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
8111nnred 11225 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
8281adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
8349adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84 elfzle2 12536 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘𝑀)
8584adantl 473 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘𝑀)
8677nn0red 11542 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87 nnre 11217 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8887ad2antrr 764 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89 2re 11280 . . . . . . . . . . . . . . 15 2 ∈ ℝ
90 2pos 11302 . . . . . . . . . . . . . . 15 0 < 2
9189, 90pm3.2i 470 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
9291a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93 lemul2 11066 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9486, 88, 92, 93syl3anc 1477 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9585, 94mpbid 222 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
9682lep1d 11145 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
9796, 7syl6breqr 4844 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
9880, 82, 83, 95, 97letrd 10384 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99 nn0uz 11913 . . . . . . . . . . . 12 0 = (ℤ‘0)
10079, 99syl6eleq 2847 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ‘0))
10144adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102 elfz5 12525 . . . . . . . . . . 11 (((2 · 𝑘) ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103100, 101, 102syl2anc 696 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
10498, 103mpbird 247 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105 fznn0sub2 12638 . . . . . . . . 9 ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106104, 105syl 17 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107106ex 449 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
10813nncnd 11226 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109108adantr 472 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110 2cn 11281 . . . . . . . . . . 11 2 ∈ ℂ
111 elfzelz 12533 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112111zcnd 11673 . . . . . . . . . . . 12 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113112ad2antrl 766 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114 mulcl 10210 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115110, 113, 114sylancr 698 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116112ssriv 3746 . . . . . . . . . . . 12 (0...𝑀) ⊆ ℂ
117 simprr 813 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118116, 117sseldi 3740 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119 mulcl 10210 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120110, 118, 119sylancr 698 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121109, 115, 120subcanad 10625 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122 2cnne0 11432 . . . . . . . . . . 11 (2 ∈ ℂ ∧ 2 ≠ 0)
123122a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124 mulcan 10854 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125113, 118, 123, 124syl3anc 1477 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126121, 125bitrd 268 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127126ex 449 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128107, 127dom2lem 8159 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129 f1f1orn 6307 . . . . . 6 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
130128, 129syl 17 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
131 oveq2 6819 . . . . . . . 8 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132131oveq2d 6827 . . . . . . 7 (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133 eqid 2758 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134 ovex 6839 . . . . . . 7 (𝑁 − (2 · 𝑗)) ∈ V
135132, 133, 134fvmpt 6442 . . . . . 6 (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136135adantl 473 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137 f1f 6260 . . . . . . . . . . 11 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138128, 137syl 17 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
139 frn 6212 . . . . . . . . . 10 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
140138, 139syl 17 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
141140sselda 3742 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
142 bccl2 13302 . . . . . . . . . . 11 (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
143142adantl 473 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
144143nncnd 11226 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
1452rprecred 12074 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
146 fznn0sub 12564 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑁𝑚) ∈ ℕ0)
147 reexpcl 13069 . . . . . . . . . . . 12 (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁𝑚) ∈ ℕ0) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
148145, 146, 147syl2an 495 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
149148recnd 10258 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℂ)
150 elfznn0 12624 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
151150adantl 473 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0)
152 expcl 13070 . . . . . . . . . . 11 ((i ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (i↑𝑚) ∈ ℂ)
1535, 151, 152sylancr 698 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
154149, 153mulcld 10250 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℂ)
155144, 154mulcld 10250 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
156141, 155syldan 488 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
157156imcld 14132 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℝ)
158157recnd 10258 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℂ)
15973, 74, 130, 136, 158fsumf1o 14651 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
160 eldifi 3873 . . . . . . . 8 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
161143nnred 11225 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
162160, 161sylan2 492 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
163160, 148sylan2 492 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
164 eldif 3723 . . . . . . . . 9 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
165 elfzelz 12533 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
166165adantl 473 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
167 zeo 11653 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
168166, 167syl 17 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
169 i2 13157 . . . . . . . . . . . . . . . . . 18 (i↑2) = -1
170169oveq1i 6821 . . . . . . . . . . . . . . . . 17 ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
171 simprr 813 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
172150ad2antrl 766 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
173 nn0re 11491 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0𝑚 ∈ ℝ)
174 nn0ge0 11508 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
175 divge0 11082 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
17689, 90, 175mpanr12 723 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
177173, 174, 176syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → 0 ≤ (𝑚 / 2))
178172, 177syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
179 elnn0z 11580 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 / 2) ∈ ℕ0 ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
180171, 178, 179sylanbrc 701 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ0)
181 expmul 13097 . . . . . . . . . . . . . . . . . . . 20 ((i ∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
1825, 75, 181mp3an12 1561 . . . . . . . . . . . . . . . . . . 19 ((𝑚 / 2) ∈ ℕ0 → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
183180, 182syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
184172nn0cnd 11543 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
185 2ne0 11303 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
186 divcan2 10883 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
187110, 185, 186mp3an23 1563 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
188184, 187syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
189188oveq2d 6827 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
190183, 189eqtr3d 2794 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
191170, 190syl5eqr 2806 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
192 neg1rr 11315 . . . . . . . . . . . . . . . . 17 -1 ∈ ℝ
193 reexpcl 13069 . . . . . . . . . . . . . . . . 17 ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ)
194192, 180, 193sylancr 698 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
195191, 194eqeltrrd 2838 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
196195expr 644 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
197146ad2antrl 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℕ0)
198 nn0re 11491 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → (𝑁𝑚) ∈ ℝ)
199 nn0ge0 11508 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ (𝑁𝑚))
200 divge0 11082 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁𝑚) / 2))
20189, 90, 200mpanr12 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) → 0 ≤ ((𝑁𝑚) / 2))
202198, 199, 201syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ ((𝑁𝑚) / 2))
203197, 202syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁𝑚) / 2))
204197nn0red 11542 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℝ)
20549adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
206 peano2re 10399 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
207205, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
208150ad2antrl 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
209208, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
210208nn0red 11542 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
211205, 210subge02d 10809 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁𝑚) ≤ 𝑁))
212209, 211mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ≤ 𝑁)
213205ltp1d 11144 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
214204, 205, 207, 212, 213lelttrd 10385 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (𝑁 + 1))
215 2t1e2 11366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 · 1) = 2
216 df-2 11269 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 = (1 + 1)
217215, 216eqtr2i 2781 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) = (2 · 1)
218217oveq2i 6822 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
2197oveq1i 6821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
22011nncnd 11226 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
221220adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
222 1cnd 10246 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
223221, 222, 222addassd 10252 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
224219, 223syl5eq 2804 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
225 2cnd 11283 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
226 nncn 11218 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
227226ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
228225, 227, 222adddid 10254 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
229218, 224, 2283eqtr4a 2818 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
230214, 229breqtrd 4828 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (2 · (𝑀 + 1)))
231 nnz 11589 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
232231ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
233232peano2zd 11675 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
234233zred 11672 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
23591a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
236 ltdivmul 11088 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
237204, 234, 235, 236syl3anc 1477 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
238230, 237mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) < (𝑀 + 1))
239108adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
240208nn0cnd 11543 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
241239, 240, 222pnpcan2d 10620 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁𝑚))
242229oveq1d 6826 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
243241, 242eqtr3d 2794 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
244243oveq1d 6826 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
245233zcnd 11673 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
246 mulcl 10210 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
247110, 245, 246sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
248 peano2cn 10398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → (𝑚 + 1) ∈ ℂ)
249240, 248syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈ ℂ)
250122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℂ ∧ 2 ≠ 0))
251 divsubdir 10911 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
252247, 249, 250, 251syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
253185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠ 0)
254245, 225, 253divcan3d 10996 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
255254oveq1d 6826 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
256244, 252, 2553eqtrd 2796 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
257 simprr 813 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
258233, 257zsubcld 11677 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
259256, 258eqeltrd 2837 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ ℤ)
260 zleltp1 11618 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
261259, 232, 260syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
262238, 261mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ≤ 𝑀)
263 0zd 11579 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
264 elfz 12523 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
265259, 263, 232, 264syl3anc 1477 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
266203, 262, 265mpbir2and 995 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ (0...𝑀))
267 oveq2 6819 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = ((𝑁𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁𝑚) / 2)))
268267oveq2d 6827 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
269 ovex 6839 . . . . . . . . . . . . . . . . . . 19 (𝑁 − (2 · ((𝑁𝑚) / 2))) ∈ V
270268, 133, 269fvmpt 6442 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
271266, 270syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
272197nn0cnd 11543 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℂ)
273272, 225, 253divcan2d 10993 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁𝑚) / 2)) = (𝑁𝑚))
274273oveq2d 6827 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁𝑚) / 2))) = (𝑁 − (𝑁𝑚)))
275239, 240nncand 10587 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁𝑚)) = 𝑚)
276271, 274, 2753eqtrd 2796 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = 𝑚)
277 ffn 6204 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
278138, 277syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
279278adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
280 fnfvelrn 6517 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
281279, 266, 280syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
282276, 281eqeltrrd 2838 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
283282expr 644 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
284196, 283orim12d 919 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
285168, 284mpd 15 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
286285orcomd 402 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
287286ord 391 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
288287impr 650 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
289164, 288sylan2b 493 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
290163, 289remulcld 10260 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℝ)
291162, 290remulcld 10260 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℝ)
292291reim0d 14162 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = 0)
293 fzfid 12964 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
294140, 158, 292, 293fsumss 14653 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
29514adantr 472 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℕ0)
296 elfznn0 12624 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
297296adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
298 nn0mulcl 11519 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ0𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
29975, 297, 298sylancr 698 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ0)
300299nn0zd 11670 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
301 bccl 13301 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
302295, 300, 301syl2anc 696 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
303302nn0red 11542 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
304 fznn0sub 12564 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑀𝑗) ∈ ℕ0)
305304adantl 473 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀𝑗) ∈ ℕ0)
306 reexpcl 13069 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ (𝑀𝑗) ∈ ℕ0) → (-1↑(𝑀𝑗)) ∈ ℝ)
307192, 305, 306sylancr 698 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℝ)
308303, 307remulcld 10260 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) ∈ ℝ)
309 2z 11599 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
310 znegcl 11602 . . . . . . . . . . . . . . . 16 (2 ∈ ℤ → -2 ∈ ℤ)
311309, 310ax-mp 5 . . . . . . . . . . . . . . 15 -2 ∈ ℤ
312 rpexpcl 13071 . . . . . . . . . . . . . . 15 (((tan‘𝐴) ∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ+)
3132, 311, 312sylancl 697 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ+)
314313rpred 12063 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
315 reexpcl 13069 . . . . . . . . . . . . 13 ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
316314, 296, 315syl2an 495 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
317308, 316remulcld 10260 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
318317recnd 10258 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
319 mulcl 10210 . . . . . . . . . 10 ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
3205, 318, 319sylancr 698 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
321320addid2d 10427 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
322302nn0cnd 11543 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
323307recnd 10258 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℂ)
324316recnd 10258 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
325322, 323, 324mulassd 10253 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
326325oveq2d 6827 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
3275a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → i ∈ ℂ)
328323, 324mulcld 10250 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
329327, 322, 328mul12d 10435 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
330326, 329eqtrd 2792 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
331 bccmpl 13288 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
332295, 300, 331syl2anc 696 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
333108adantr 472 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
334299nn0cnd 11543 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
335333, 334nncand 10587 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
336335oveq2d 6827 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
3372adantr 472 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ+)
338337rpcnd 12065 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
339 expneg 13060 . . . . . . . . . . . . . 14 (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
340338, 299, 339syl2anc 696 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
341297nn0cnd 11543 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
342 mulneg1 10656 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
343110, 341, 342sylancr 698 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
344343oveq2d 6827 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
345337rpne0d 12068 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
346338, 345, 300exprecd 13208 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
347340, 344, 3463eqtr4d 2802 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
348311a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
349297nn0zd 11670 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
350 expmulz 13098 . . . . . . . . . . . . 13 ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
351338, 345, 348, 349, 350syl22anc 1478 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
352336, 347, 3513eqtr2d 2798 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
3537oveq1i 6821 . . . . . . . . . . . . . . 15 (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
35411adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
355354nncnd 11226 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
356 1cnd 10246 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
357355, 356, 334addsubd 10603 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
358 2cnd 11283 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
359226ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
360358, 359, 341subdid 10676 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
361360oveq1d 6826 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
362357, 361eqtr4d 2795 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
363353, 362syl5eq 2804 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
364363oveq2d 6827 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀𝑗)) + 1)))
365 nn0mulcl 11519 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑀𝑗) ∈ ℕ0) → (2 · (𝑀𝑗)) ∈ ℕ0)
36675, 305, 365sylancr 698 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) ∈ ℕ0)
367 expp1 13059 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑀𝑗)) ∈ ℕ0) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
3685, 366, 367sylancr 698 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
36975a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ0)
370327, 305, 369expmuld 13203 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = ((i↑2)↑(𝑀𝑗)))
371169oveq1i 6821 . . . . . . . . . . . . . . 15 ((i↑2)↑(𝑀𝑗)) = (-1↑(𝑀𝑗))
372370, 371syl6eq 2808 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = (-1↑(𝑀𝑗)))
373372oveq1d 6826 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀𝑗))) · i) = ((-1↑(𝑀𝑗)) · i))
374364, 368, 3733eqtrd 2796 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀𝑗)) · i))
375 mulcom 10212 . . . . . . . . . . . . 13 (((-1↑(𝑀𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
376323, 5, 375sylancl 697 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
377374, 376eqtrd 2792 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀𝑗))))
378352, 377oveq12d 6829 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
379 mulcl 10210 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (-1↑(𝑀𝑗)) ∈ ℂ) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
3805, 323, 379sylancr 698 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
381380, 324mulcomd 10251 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
382327, 323, 324mulassd 10253 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
383378, 381, 3823eqtr2rd 2799 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
384332, 383oveq12d 6829 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
385321, 330, 3843eqtrd 2796 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
386385fveq2d 6354 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
387 0re 10230 . . . . . . 7 0 ∈ ℝ
388 crim 14052 . . . . . . 7 ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389387, 317, 388sylancr 698 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390386, 389eqtr3d 2794 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
391390sumeq2dv 14630 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
392159, 294, 3913eqtr3d 2800 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
393293, 155fsumim 14738 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
394313rpcnd 12065 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
395 oveq1 6818 . . . . . . 7 (𝑡 = ((tan‘𝐴)↑-2) → (𝑡𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
396395oveq2d 6827 . . . . . 6 (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
397396sumeq2sdv 14632 . . . . 5 (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
398 basel.p . . . . 5 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
399 sumex 14615 . . . . 5 Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
400397, 398, 399fvmpt 6442 . . . 4 (((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
401394, 400syl 17 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
402392, 393, 4013eqtr4d 2802 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
40351, 58rerpdivcld 12094 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
40453, 58rerpdivcld 12094 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
405403, 404crimd 14169 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
40666, 402, 4053eqtr3d 2800 1 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1630  wcel 2137  wne 2930  cdif 3710  wss 3713   class class class wbr 4802  cmpt 4879  ran crn 5265   Fn wfn 6042  wf 6043  1-1wf1 6044  1-1-ontowf1o 6046  cfv 6047  (class class class)co 6811  cc 10124  cr 10125  0cc0 10126  1c1 10127  ici 10128   + caddc 10129   · cmul 10131   < clt 10264  cle 10265  cmin 10456  -cneg 10457   / cdiv 10874  cn 11210  2c2 11260  0cn0 11482  cz 11567  cuz 11877  +crp 12023  (,)cioo 12366  ...cfz 12517  cexp 13052  Ccbc 13281  cim 14035  Σcsu 14613  sincsin 14991  cosccos 14992  tanctan 14993  πcpi 14994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204  ax-addf 10205  ax-mulf 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-of 7060  df-om 7229  df-1st 7331  df-2nd 7332  df-supp 7462  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-ixp 8073  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fsupp 8439  df-fi 8480  df-sup 8511  df-inf 8512  df-oi 8578  df-card 8953  df-cda 9180  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276  df-n0 11483  df-z 11568  df-dec 11684  df-uz 11878  df-q 11980  df-rp 12024  df-xneg 12137  df-xadd 12138  df-xmul 12139  df-ioo 12370  df-ioc 12371  df-ico 12372  df-icc 12373  df-fz 12518  df-fzo 12658  df-fl 12785  df-seq 12994  df-exp 13053  df-fac 13253  df-bc 13282  df-hash 13310  df-shft 14004  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-limsup 14399  df-clim 14416  df-rlim 14417  df-sum 14614  df-ef 14995  df-sin 14997  df-cos 14998  df-tan 14999  df-pi 15000  df-struct 16059  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16154  df-mulr 16155  df-starv 16156  df-sca 16157  df-vsca 16158  df-ip 16159  df-tset 16160  df-ple 16161  df-ds 16164  df-unif 16165  df-hom 16166  df-cco 16167  df-rest 16283  df-topn 16284  df-0g 16302  df-gsum 16303  df-topgen 16304  df-pt 16305  df-prds 16308  df-xrs 16362  df-qtop 16367  df-imas 16368  df-xps 16370  df-mre 16446  df-mrc 16447  df-acs 16449  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-submnd 17535  df-mulg 17740  df-cntz 17948  df-cmn 18393  df-psmet 19938  df-xmet 19939  df-met 19940  df-bl 19941  df-mopn 19942  df-fbas 19943  df-fg 19944  df-cnfld 19947  df-top 20899  df-topon 20916  df-topsp 20937  df-bases 20950  df-cld 21023  df-ntr 21024  df-cls 21025  df-nei 21102  df-lp 21140  df-perf 21141  df-cn 21231  df-cnp 21232  df-haus 21319  df-tx 21565  df-hmeo 21758  df-fil 21849  df-fm 21941  df-flim 21942  df-flf 21943  df-xms 22324  df-ms 22325  df-tms 22326  df-cncf 22880  df-limc 23827  df-dv 23828
This theorem is referenced by:  basellem4  25007
  Copyright terms: Public domain W3C validator