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

Theorem basellem3 25099
Description: Lemma for basel 25106. 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 24547 . . . . . . . 8 (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
21adantl 473 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ+)
32rpreccld 12079 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ+)
43rpcnd 12071 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5 ax-icn 10247 . . . . . 6 i ∈ ℂ
65a1i 11 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7 basel.n . . . . . . 7 𝑁 = ((2 · 𝑀) + 1)
8 2nn 11344 . . . . . . . . 9 2 ∈ ℕ
9 simpl 474 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10 nnmulcl 11298 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
118, 9, 10sylancr 581 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
1211peano2nnd 11292 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
137, 12syl5eqel 2847 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
1413nnnn0d 11597 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ0)
15 binom 14847 . . . . 5 (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
164, 6, 14, 15syl3anc 1490 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
17 elioore 12406 . . . . . . . . . . 11 (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
1817adantl 473 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
1918recoscld 15157 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
2019recnd 10321 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
2118resincld 15156 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
2221recnd 10321 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23 mulcl 10272 . . . . . . . . 9 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
245, 22, 23sylancr 581 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
2520, 24addcld 10312 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26 sincosq1sgn 24541 . . . . . . . . . 10 (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2726adantl 473 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2827simpld 488 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
2928gt0ne0d 10845 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
3025, 22, 29, 14expdivd 13228 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
3120, 24, 22, 29divdird 11092 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
3218recnd 10321 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
3327simprd 489 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
3433gt0ne0d 10845 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35 tanval 15141 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3632, 34, 35syl2anc 579 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3736oveq2d 6857 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
3822, 20, 29, 34recdivd 11071 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
3937, 38eqtr2d 2799 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
406, 22, 29divcan4d 11060 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
4139, 40oveq12d 6859 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
4231, 41eqtrd 2798 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
4342oveq1d 6856 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
4413nnzd 11727 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45 demoivre 15213 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4632, 44, 45syl2anc 579 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4746oveq1d 6856 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4830, 43, 473eqtr3d 2806 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4913nnred 11290 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
5049, 18remulcld 10323 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
5150recoscld 15157 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
5251recnd 10321 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
5350resincld 15156 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
5453recnd 10321 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55 mulcl 10272 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
565, 54, 55sylancr 581 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
5721, 28elrpd 12066 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ+)
5857, 44rpexpcld 13238 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ+)
5958rpcnd 12071 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
6058rpne0d 12074 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
6152, 56, 59, 60divdird 11092 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
626, 54, 59, 60divassd 11089 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
6362oveq2d 6857 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6448, 61, 633eqtrd 2802 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6516, 64eqtr3d 2800 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6665fveq2d 6378 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67 oveq2 6849 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68 oveq2 6849 . . . . . . . . 9 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
6968oveq2d 6857 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70 oveq2 6849 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
7169, 70oveq12d 6859 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
7267, 71oveq12d 6859 . . . . . 6 (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
7372fveq2d 6378 . . . . 5 (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74 fzfid 12979 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75 2nn0 11556 . . . . . . . . . . . . 13 2 ∈ ℕ0
76 elfznn0 12639 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0)
7776adantl 473 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0)
78 nn0mulcl 11575 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
7975, 77, 78sylancr 581 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ0)
8079nn0red 11598 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
8111nnred 11290 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
8281adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
8349adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84 elfzle2 12551 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘𝑀)
8584adantl 473 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘𝑀)
8677nn0red 11598 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87 nnre 11281 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8887ad2antrr 717 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89 2re 11345 . . . . . . . . . . . . . . 15 2 ∈ ℝ
90 2pos 11381 . . . . . . . . . . . . . . 15 0 < 2
9189, 90pm3.2i 462 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
9291a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93 lemul2 11129 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9486, 88, 92, 93syl3anc 1490 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9585, 94mpbid 223 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
9682lep1d 11208 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
9796, 7syl6breqr 4850 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
9880, 82, 83, 95, 97letrd 10447 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99 nn0uz 11921 . . . . . . . . . . . 12 0 = (ℤ‘0)
10079, 99syl6eleq 2853 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ‘0))
10144adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102 elfz5 12540 . . . . . . . . . . 11 (((2 · 𝑘) ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103100, 101, 102syl2anc 579 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
10498, 103mpbird 248 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105 fznn0sub2 12653 . . . . . . . . 9 ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106104, 105syl 17 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107106ex 401 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
10813nncnd 11291 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109108adantr 472 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110 2cn 11346 . . . . . . . . . . 11 2 ∈ ℂ
111 elfzelz 12548 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112111zcnd 11729 . . . . . . . . . . . 12 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113112ad2antrl 719 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114 mulcl 10272 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115110, 113, 114sylancr 581 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116112ssriv 3764 . . . . . . . . . . . 12 (0...𝑀) ⊆ ℂ
117 simprr 789 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118116, 117sseldi 3758 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119 mulcl 10272 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120110, 118, 119sylancr 581 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121109, 115, 120subcanad 10688 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122 2cnne0 11487 . . . . . . . . . . 11 (2 ∈ ℂ ∧ 2 ≠ 0)
123122a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124 mulcan 10917 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125113, 118, 123, 124syl3anc 1490 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126121, 125bitrd 270 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127126ex 401 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128107, 127dom2lem 8199 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129 f1f1orn 6330 . . . . . 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 6849 . . . . . . . 8 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132131oveq2d 6857 . . . . . . 7 (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133 eqid 2764 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134 ovex 6873 . . . . . . 7 (𝑁 − (2 · 𝑗)) ∈ V
135132, 133, 134fvmpt 6470 . . . . . 6 (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136135adantl 473 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137 f1f 6282 . . . . . . . . . . 11 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138128, 137syl 17 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
139138frnd 6229 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
140139sselda 3760 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
141 bccl2 13313 . . . . . . . . . . 11 (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
142141adantl 473 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
143142nncnd 11291 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
1442rprecred 12080 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
145 fznn0sub 12579 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑁𝑚) ∈ ℕ0)
146 reexpcl 13083 . . . . . . . . . . . 12 (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁𝑚) ∈ ℕ0) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
147144, 145, 146syl2an 589 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
148147recnd 10321 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℂ)
149 elfznn0 12639 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
150149adantl 473 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0)
151 expcl 13084 . . . . . . . . . . 11 ((i ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (i↑𝑚) ∈ ℂ)
1525, 150, 151sylancr 581 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
153148, 152mulcld 10313 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℂ)
154143, 153mulcld 10313 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
155140, 154syldan 585 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
156155imcld 14221 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℝ)
157156recnd 10321 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℂ)
15873, 74, 130, 136, 157fsumf1o 14740 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
159 eldifi 3893 . . . . . . . 8 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
160142nnred 11290 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
161159, 160sylan2 586 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
162159, 147sylan2 586 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
163 eldif 3741 . . . . . . . . 9 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
164 elfzelz 12548 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
165164adantl 473 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
166 zeo 11709 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167165, 166syl 17 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
168 i2 13171 . . . . . . . . . . . . . . . . . 18 (i↑2) = -1
169168oveq1i 6851 . . . . . . . . . . . . . . . . 17 ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
170 simprr 789 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
171149ad2antrl 719 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
172 nn0re 11547 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0𝑚 ∈ ℝ)
173 nn0ge0 11564 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
174 divge0 11145 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
17589, 90, 174mpanr12 696 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
176172, 173, 175syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → 0 ≤ (𝑚 / 2))
177171, 176syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
178 elnn0z 11636 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 / 2) ∈ ℕ0 ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
179170, 177, 178sylanbrc 578 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ0)
180 expmul 13111 . . . . . . . . . . . . . . . . . . . 20 ((i ∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
1815, 75, 180mp3an12 1575 . . . . . . . . . . . . . . . . . . 19 ((𝑚 / 2) ∈ ℕ0 → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
182179, 181syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
183171nn0cnd 11599 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
184 2ne0 11382 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
185 divcan2 10946 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
186110, 184, 185mp3an23 1577 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
187183, 186syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
188187oveq2d 6857 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
189182, 188eqtr3d 2800 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
190169, 189syl5eqr 2812 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
191 neg1rr 11393 . . . . . . . . . . . . . . . . 17 -1 ∈ ℝ
192 reexpcl 13083 . . . . . . . . . . . . . . . . 17 ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ)
193191, 179, 192sylancr 581 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
194190, 193eqeltrrd 2844 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
195194expr 448 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
196145ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℕ0)
197 nn0re 11547 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → (𝑁𝑚) ∈ ℝ)
198 nn0ge0 11564 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ (𝑁𝑚))
199 divge0 11145 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁𝑚) / 2))
20089, 90, 199mpanr12 696 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) → 0 ≤ ((𝑁𝑚) / 2))
201197, 198, 200syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ ((𝑁𝑚) / 2))
202196, 201syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁𝑚) / 2))
203196nn0red 11598 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℝ)
20449adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
205 peano2re 10462 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
207149ad2antrl 719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
208207, 173syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
209207nn0red 11598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
210204, 209subge02d 10872 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁𝑚) ≤ 𝑁))
211208, 210mpbid 223 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ≤ 𝑁)
212204ltp1d 11207 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
213203, 204, 206, 211, 212lelttrd 10448 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (𝑁 + 1))
214 2t1e2 11440 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 · 1) = 2
215 df-2 11334 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 = (1 + 1)
216214, 215eqtr2i 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) = (2 · 1)
217216oveq2i 6852 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
2187oveq1i 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
21911nncnd 11291 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
220219adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
221 1cnd 10287 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
222220, 221, 221addassd 10315 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
223218, 222syl5eq 2810 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
224 2cnd 11349 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
225 nncn 11282 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
226225ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
227224, 226, 221adddid 10317 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
228217, 223, 2273eqtr4a 2824 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
229213, 228breqtrd 4834 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (2 · (𝑀 + 1)))
230 nnz 11645 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
231230ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
232231peano2zd 11731 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
233232zred 11728 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
23491a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
235 ltdivmul 11151 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
236203, 233, 234, 235syl3anc 1490 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
237229, 236mpbird 248 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) < (𝑀 + 1))
238108adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
239207nn0cnd 11599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
240238, 239, 221pnpcan2d 10683 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁𝑚))
241228oveq1d 6856 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
242240, 241eqtr3d 2800 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
243242oveq1d 6856 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
244232zcnd 11729 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
245 mulcl 10272 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
246110, 244, 245sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
247 peano2cn 10461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → (𝑚 + 1) ∈ ℂ)
248239, 247syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈ ℂ)
249122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℂ ∧ 2 ≠ 0))
250 divsubdir 10974 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
251246, 248, 249, 250syl3anc 1490 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
252184a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠ 0)
253244, 224, 252divcan3d 11059 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
254253oveq1d 6856 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
255243, 251, 2543eqtrd 2802 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
256 simprr 789 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
257232, 256zsubcld 11733 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
258255, 257eqeltrd 2843 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ ℤ)
259 zleltp1 11674 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
260258, 231, 259syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
261237, 260mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ≤ 𝑀)
262 0zd 11635 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
263 elfz 12538 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
264258, 262, 231, 263syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
265202, 261, 264mpbir2and 704 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ (0...𝑀))
266 oveq2 6849 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = ((𝑁𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁𝑚) / 2)))
267266oveq2d 6857 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
268 ovex 6873 . . . . . . . . . . . . . . . . . . 19 (𝑁 − (2 · ((𝑁𝑚) / 2))) ∈ V
269267, 133, 268fvmpt 6470 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
270265, 269syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
271196nn0cnd 11599 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℂ)
272271, 224, 252divcan2d 11056 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁𝑚) / 2)) = (𝑁𝑚))
273272oveq2d 6857 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁𝑚) / 2))) = (𝑁 − (𝑁𝑚)))
274238, 239nncand 10650 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁𝑚)) = 𝑚)
275270, 273, 2743eqtrd 2802 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = 𝑚)
276138ffnd 6223 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
277276adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
278 fnfvelrn 6545 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
279277, 265, 278syl2anc 579 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
280275, 279eqeltrrd 2844 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
281280expr 448 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
282195, 281orim12d 987 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
283167, 282mpd 15 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
284283orcomd 897 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
285284ord 890 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
286285impr 446 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
287163, 286sylan2b 587 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
288162, 287remulcld 10323 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℝ)
289161, 288remulcld 10323 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℝ)
290289reim0d 14251 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = 0)
291 fzfid 12979 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
292139, 157, 290, 291fsumss 14742 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
29314adantr 472 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℕ0)
294 elfznn0 12639 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
295294adantl 473 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
296 nn0mulcl 11575 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ0𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
29775, 295, 296sylancr 581 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ0)
298297nn0zd 11726 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
299 bccl 13312 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
300293, 298, 299syl2anc 579 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
301300nn0red 11598 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
302 fznn0sub 12579 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑀𝑗) ∈ ℕ0)
303302adantl 473 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀𝑗) ∈ ℕ0)
304 reexpcl 13083 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ (𝑀𝑗) ∈ ℕ0) → (-1↑(𝑀𝑗)) ∈ ℝ)
305191, 303, 304sylancr 581 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℝ)
306301, 305remulcld 10323 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) ∈ ℝ)
307 2z 11655 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
308 znegcl 11658 . . . . . . . . . . . . . . . 16 (2 ∈ ℤ → -2 ∈ ℤ)
309307, 308ax-mp 5 . . . . . . . . . . . . . . 15 -2 ∈ ℤ
310 rpexpcl 13085 . . . . . . . . . . . . . . 15 (((tan‘𝐴) ∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ+)
3112, 309, 310sylancl 580 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ+)
312311rpred 12069 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
313 reexpcl 13083 . . . . . . . . . . . . 13 ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
314312, 294, 313syl2an 589 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
315306, 314remulcld 10323 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
316315recnd 10321 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
317 mulcl 10272 . . . . . . . . . 10 ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
3185, 316, 317sylancr 581 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
319318addid2d 10490 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
320300nn0cnd 11599 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
321305recnd 10321 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℂ)
322314recnd 10321 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
323320, 321, 322mulassd 10316 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
324323oveq2d 6857 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
3255a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → i ∈ ℂ)
326321, 322mulcld 10313 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
327325, 320, 326mul12d 10498 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
328324, 327eqtrd 2798 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
329 bccmpl 13299 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
330293, 298, 329syl2anc 579 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
331108adantr 472 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
332297nn0cnd 11599 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
333331, 332nncand 10650 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
334333oveq2d 6857 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
3352adantr 472 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ+)
336335rpcnd 12071 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
337 expneg 13074 . . . . . . . . . . . . . 14 (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
338336, 297, 337syl2anc 579 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
339295nn0cnd 11599 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
340 mulneg1 10719 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
341110, 339, 340sylancr 581 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
342341oveq2d 6857 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
343335rpne0d 12074 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
344336, 343, 298exprecd 13222 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
345338, 342, 3443eqtr4d 2808 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
346309a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
347295nn0zd 11726 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
348 expmulz 13112 . . . . . . . . . . . . 13 ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
349336, 343, 346, 347, 348syl22anc 867 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
350334, 345, 3493eqtr2d 2804 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
3517oveq1i 6851 . . . . . . . . . . . . . . 15 (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
35211adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
353352nncnd 11291 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
354 1cnd 10287 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
355353, 354, 332addsubd 10666 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
356 2cnd 11349 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
357225ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
358356, 357, 339subdid 10739 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
359358oveq1d 6856 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
360355, 359eqtr4d 2801 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
361351, 360syl5eq 2810 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
362361oveq2d 6857 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀𝑗)) + 1)))
363 nn0mulcl 11575 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑀𝑗) ∈ ℕ0) → (2 · (𝑀𝑗)) ∈ ℕ0)
36475, 303, 363sylancr 581 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) ∈ ℕ0)
365 expp1 13073 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑀𝑗)) ∈ ℕ0) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
3665, 364, 365sylancr 581 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
36775a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ0)
368325, 303, 367expmuld 13217 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = ((i↑2)↑(𝑀𝑗)))
369168oveq1i 6851 . . . . . . . . . . . . . . 15 ((i↑2)↑(𝑀𝑗)) = (-1↑(𝑀𝑗))
370368, 369syl6eq 2814 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = (-1↑(𝑀𝑗)))
371370oveq1d 6856 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀𝑗))) · i) = ((-1↑(𝑀𝑗)) · i))
372362, 366, 3713eqtrd 2802 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀𝑗)) · i))
373 mulcom 10274 . . . . . . . . . . . . 13 (((-1↑(𝑀𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
374321, 5, 373sylancl 580 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
375372, 374eqtrd 2798 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀𝑗))))
376350, 375oveq12d 6859 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
377 mulcl 10272 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (-1↑(𝑀𝑗)) ∈ ℂ) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
3785, 321, 377sylancr 581 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
379378, 322mulcomd 10314 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
380325, 321, 322mulassd 10316 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
381376, 379, 3803eqtr2rd 2805 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
382330, 381oveq12d 6859 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
383319, 328, 3823eqtrd 2802 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
384383fveq2d 6378 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
385 0re 10294 . . . . . . 7 0 ∈ ℝ
386 crim 14141 . . . . . . 7 ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
387385, 315, 386sylancr 581 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
388384, 387eqtr3d 2800 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389388sumeq2dv 14719 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390158, 292, 3893eqtr3d 2806 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
391291, 154fsumim 14826 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
392311rpcnd 12071 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
393 oveq1 6848 . . . . . . 7 (𝑡 = ((tan‘𝐴)↑-2) → (𝑡𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
394393oveq2d 6857 . . . . . 6 (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
395394sumeq2sdv 14721 . . . . 5 (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
396 basel.p . . . . 5 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
397 sumex 14704 . . . . 5 Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
398395, 396, 397fvmpt 6470 . . . 4 (((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
399392, 398syl 17 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
400390, 391, 3993eqtr4d 2808 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
40151, 58rerpdivcld 12100 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
40253, 58rerpdivcld 12100 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
403401, 402crimd 14258 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
40466, 400, 4033eqtr3d 2806 1 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wcel 2155  wne 2936  cdif 3728   class class class wbr 4808  cmpt 4887  ran crn 5277   Fn wfn 6062  wf 6063  1-1wf1 6064  1-1-ontowf1o 6066  cfv 6067  (class class class)co 6841  cc 10186  cr 10187  0cc0 10188  1c1 10189  ici 10190   + caddc 10191   · cmul 10193   < clt 10327  cle 10328  cmin 10519  -cneg 10520   / cdiv 10937  cn 11273  2c2 11326  0cn0 11537  cz 11623  cuz 11885  +crp 12027  (,)cioo 12376  ...cfz 12532  cexp 13066  Ccbc 13292  cim 14124  Σcsu 14702  sincsin 15077  cosccos 15078  tanctan 15079  πcpi 15080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-fi 8523  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-q 11989  df-rp 12028  df-xneg 12145  df-xadd 12146  df-xmul 12147  df-ioo 12380  df-ioc 12381  df-ico 12382  df-icc 12383  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-fac 13264  df-bc 13293  df-hash 13321  df-shft 14093  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-limsup 14488  df-clim 14505  df-rlim 14506  df-sum 14703  df-ef 15081  df-sin 15083  df-cos 15084  df-tan 15085  df-pi 15086  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-rest 16350  df-topn 16351  df-0g 16369  df-gsum 16370  df-topgen 16371  df-pt 16372  df-prds 16375  df-xrs 16429  df-qtop 16434  df-imas 16435  df-xps 16437  df-mre 16513  df-mrc 16514  df-acs 16516  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-mulg 17809  df-cntz 18014  df-cmn 18460  df-psmet 20010  df-xmet 20011  df-met 20012  df-bl 20013  df-mopn 20014  df-fbas 20015  df-fg 20016  df-cnfld 20019  df-top 20977  df-topon 20994  df-topsp 21016  df-bases 21029  df-cld 21102  df-ntr 21103  df-cls 21104  df-nei 21181  df-lp 21219  df-perf 21220  df-cn 21310  df-cnp 21311  df-haus 21398  df-tx 21644  df-hmeo 21837  df-fil 21928  df-fm 22020  df-flim 22021  df-flf 22022  df-xms 22403  df-ms 22404  df-tms 22405  df-cncf 22959  df-limc 23920  df-dv 23921
This theorem is referenced by:  basellem4  25100
  Copyright terms: Public domain W3C validator