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

Theorem basellem3 24722
Description: Lemma for basel 24729. 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 24173 . . . . . . . 8 (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
21adantl 482 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ+)
32rpreccld 11833 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ+)
43rpcnd 11825 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5 ax-icn 9946 . . . . . 6 i ∈ ℂ
65a1i 11 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7 basel.n . . . . . . 7 𝑁 = ((2 · 𝑀) + 1)
8 2nn 11136 . . . . . . . . 9 2 ∈ ℕ
9 simpl 473 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10 nnmulcl 10994 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
118, 9, 10sylancr 694 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
1211peano2nnd 10988 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
137, 12syl5eqel 2702 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
1413nnnn0d 11302 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ0)
15 binom 14494 . . . . 5 (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
164, 6, 14, 15syl3anc 1323 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
17 elioore 12154 . . . . . . . . . . 11 (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
1817adantl 482 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
1918recoscld 14806 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
2019recnd 10019 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
2118resincld 14805 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
2221recnd 10019 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23 mulcl 9971 . . . . . . . . 9 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
245, 22, 23sylancr 694 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
2520, 24addcld 10010 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26 sincosq1sgn 24167 . . . . . . . . . 10 (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2726adantl 482 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2827simpld 475 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
2928gt0ne0d 10543 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
3025, 22, 29, 14expdivd 12969 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
3120, 24, 22, 29divdird 10790 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
3218recnd 10019 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
3327simprd 479 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
3433gt0ne0d 10543 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35 tanval 14790 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3632, 34, 35syl2anc 692 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3736oveq2d 6626 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
3822, 20, 29, 34recdivd 10769 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
3937, 38eqtr2d 2656 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
406, 22, 29divcan4d 10758 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
4139, 40oveq12d 6628 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
4231, 41eqtrd 2655 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
4342oveq1d 6625 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
4413nnzd 11432 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45 demoivre 14862 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4632, 44, 45syl2anc 692 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4746oveq1d 6625 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4830, 43, 473eqtr3d 2663 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4913nnred 10986 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
5049, 18remulcld 10021 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
5150recoscld 14806 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
5251recnd 10019 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
5350resincld 14805 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
5453recnd 10019 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55 mulcl 9971 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
565, 54, 55sylancr 694 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
5721, 28elrpd 11820 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ+)
5857, 44rpexpcld 12979 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ+)
5958rpcnd 11825 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
6058rpne0d 11828 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
6152, 56, 59, 60divdird 10790 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
626, 54, 59, 60divassd 10787 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
6362oveq2d 6626 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6448, 61, 633eqtrd 2659 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6516, 64eqtr3d 2657 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6665fveq2d 6157 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67 oveq2 6618 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68 oveq2 6618 . . . . . . . . 9 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
6968oveq2d 6626 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70 oveq2 6618 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
7169, 70oveq12d 6628 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
7267, 71oveq12d 6628 . . . . . 6 (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
7372fveq2d 6157 . . . . 5 (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74 fzfid 12719 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75 2nn0 11260 . . . . . . . . . . . . 13 2 ∈ ℕ0
76 elfznn0 12381 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0)
7776adantl 482 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0)
78 nn0mulcl 11280 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
7975, 77, 78sylancr 694 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ0)
8079nn0red 11303 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
8111nnred 10986 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
8281adantr 481 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
8349adantr 481 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84 elfzle2 12294 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘𝑀)
8584adantl 482 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘𝑀)
8677nn0red 11303 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87 nnre 10978 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8887ad2antrr 761 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89 2re 11041 . . . . . . . . . . . . . . 15 2 ∈ ℝ
90 2pos 11063 . . . . . . . . . . . . . . 15 0 < 2
9189, 90pm3.2i 471 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
9291a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93 lemul2 10827 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9486, 88, 92, 93syl3anc 1323 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9585, 94mpbid 222 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
9682lep1d 10906 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
9796, 7syl6breqr 4660 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
9880, 82, 83, 95, 97letrd 10145 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99 nn0uz 11673 . . . . . . . . . . . 12 0 = (ℤ‘0)
10079, 99syl6eleq 2708 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ‘0))
10144adantr 481 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102 elfz5 12283 . . . . . . . . . . 11 (((2 · 𝑘) ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103100, 101, 102syl2anc 692 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
10498, 103mpbird 247 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105 fznn0sub2 12394 . . . . . . . . 9 ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106104, 105syl 17 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107106ex 450 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
10813nncnd 10987 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109108adantr 481 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110 2cn 11042 . . . . . . . . . . 11 2 ∈ ℂ
111 elfzelz 12291 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112111zcnd 11434 . . . . . . . . . . . 12 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113112ad2antrl 763 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114 mulcl 9971 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115110, 113, 114sylancr 694 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116112ssriv 3591 . . . . . . . . . . . 12 (0...𝑀) ⊆ ℂ
117 simprr 795 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118116, 117sseldi 3585 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119 mulcl 9971 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120110, 118, 119sylancr 694 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121109, 115, 120subcanad 10386 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122 2cnne0 11193 . . . . . . . . . . 11 (2 ∈ ℂ ∧ 2 ≠ 0)
123122a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124 mulcan 10615 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125113, 118, 123, 124syl3anc 1323 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126121, 125bitrd 268 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127126ex 450 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128107, 127dom2lem 7946 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129 f1f1orn 6110 . . . . . 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 6618 . . . . . . . 8 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132131oveq2d 6626 . . . . . . 7 (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133 eqid 2621 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134 ovex 6638 . . . . . . 7 (𝑁 − (2 · 𝑗)) ∈ V
135132, 133, 134fvmpt 6244 . . . . . 6 (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136135adantl 482 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137 f1f 6063 . . . . . . . . . . 11 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138128, 137syl 17 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
139 frn 6015 . . . . . . . . . 10 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
140138, 139syl 17 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
141140sselda 3587 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
142 bccl2 13057 . . . . . . . . . . 11 (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
143142adantl 482 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
144143nncnd 10987 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
1452rprecred 11834 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
146 fznn0sub 12322 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑁𝑚) ∈ ℕ0)
147 reexpcl 12824 . . . . . . . . . . . 12 (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁𝑚) ∈ ℕ0) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
148145, 146, 147syl2an 494 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
149148recnd 10019 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℂ)
150 elfznn0 12381 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
151150adantl 482 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0)
152 expcl 12825 . . . . . . . . . . 11 ((i ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (i↑𝑚) ∈ ℂ)
1535, 151, 152sylancr 694 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
154149, 153mulcld 10011 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℂ)
155144, 154mulcld 10011 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
156141, 155syldan 487 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
157156imcld 13876 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℝ)
158157recnd 10019 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℂ)
15973, 74, 130, 136, 158fsumf1o 14394 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
160 eldifi 3715 . . . . . . . 8 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
161143nnred 10986 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
162160, 161sylan2 491 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
163160, 148sylan2 491 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
164 eldif 3569 . . . . . . . . 9 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
165 elfzelz 12291 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
166165adantl 482 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
167 zeo 11414 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
168166, 167syl 17 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
169 i2 12912 . . . . . . . . . . . . . . . . . 18 (i↑2) = -1
170169oveq1i 6620 . . . . . . . . . . . . . . . . 17 ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
171 simprr 795 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
172150ad2antrl 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
173 nn0re 11252 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0𝑚 ∈ ℝ)
174 nn0ge0 11269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
175 divge0 10843 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
17689, 90, 175mpanr12 720 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
177173, 174, 176syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → 0 ≤ (𝑚 / 2))
178172, 177syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
179 elnn0z 11341 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 / 2) ∈ ℕ0 ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
180171, 178, 179sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ0)
181 expmul 12852 . . . . . . . . . . . . . . . . . . . 20 ((i ∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
1825, 75, 181mp3an12 1411 . . . . . . . . . . . . . . . . . . 19 ((𝑚 / 2) ∈ ℕ0 → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
183180, 182syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
184172nn0cnd 11304 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
185 2ne0 11064 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
186 divcan2 10644 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
187110, 185, 186mp3an23 1413 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
188184, 187syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
189188oveq2d 6626 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
190183, 189eqtr3d 2657 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
191170, 190syl5eqr 2669 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
192 neg1rr 11076 . . . . . . . . . . . . . . . . 17 -1 ∈ ℝ
193 reexpcl 12824 . . . . . . . . . . . . . . . . 17 ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ)
194192, 180, 193sylancr 694 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
195191, 194eqeltrrd 2699 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
196195expr 642 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
197146ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℕ0)
198 nn0re 11252 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → (𝑁𝑚) ∈ ℝ)
199 nn0ge0 11269 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ (𝑁𝑚))
200 divge0 10843 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁𝑚) / 2))
20189, 90, 200mpanr12 720 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) → 0 ≤ ((𝑁𝑚) / 2))
202198, 199, 201syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ ((𝑁𝑚) / 2))
203197, 202syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁𝑚) / 2))
204197nn0red 11303 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℝ)
20549adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
206 peano2re 10160 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
207205, 206syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
208150ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
209208, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
210208nn0red 11303 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
211205, 210subge02d 10570 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁𝑚) ≤ 𝑁))
212209, 211mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ≤ 𝑁)
213205ltp1d 10905 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
214204, 205, 207, 212, 213lelttrd 10146 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (𝑁 + 1))
215 2t1e2 11127 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 · 1) = 2
216 df-2 11030 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 = (1 + 1)
217215, 216eqtr2i 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) = (2 · 1)
218217oveq2i 6621 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
2197oveq1i 6620 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
22011nncnd 10987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
221220adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
222 1cnd 10007 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
223221, 222, 222addassd 10013 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
224219, 223syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
225 2cnd 11044 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
226 nncn 10979 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
227226ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
228225, 227, 222adddid 10015 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
229218, 224, 2283eqtr4a 2681 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
230214, 229breqtrd 4644 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (2 · (𝑀 + 1)))
231 nnz 11350 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
232231ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
233232peano2zd 11436 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
234233zred 11433 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
23591a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
236 ltdivmul 10849 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
237204, 234, 235, 236syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
238230, 237mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) < (𝑀 + 1))
239108adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
240208nn0cnd 11304 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
241239, 240, 222pnpcan2d 10381 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁𝑚))
242229oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
243241, 242eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
244243oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
245233zcnd 11434 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
246 mulcl 9971 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
247110, 245, 246sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
248 peano2cn 10159 . . . . . . . . . . . . . . . . . . . . . . . . 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 10672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
252247, 249, 250, 251syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . 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 10757 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
255254oveq1d 6625 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
256244, 252, 2553eqtrd 2659 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
257 simprr 795 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
258233, 257zsubcld 11438 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
259256, 258eqeltrd 2698 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ ℤ)
260 zleltp1 11379 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
261259, 232, 260syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
262238, 261mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ≤ 𝑀)
263 0zd 11340 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
264 elfz 12281 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
265259, 263, 232, 264syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
266203, 262, 265mpbir2and 956 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ (0...𝑀))
267 oveq2 6618 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = ((𝑁𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁𝑚) / 2)))
268267oveq2d 6626 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
269 ovex 6638 . . . . . . . . . . . . . . . . . . 19 (𝑁 − (2 · ((𝑁𝑚) / 2))) ∈ V
270268, 133, 269fvmpt 6244 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
271266, 270syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
272197nn0cnd 11304 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℂ)
273272, 225, 253divcan2d 10754 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁𝑚) / 2)) = (𝑁𝑚))
274273oveq2d 6626 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁𝑚) / 2))) = (𝑁 − (𝑁𝑚)))
275239, 240nncand 10348 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁𝑚)) = 𝑚)
276271, 274, 2753eqtrd 2659 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = 𝑚)
277 ffn 6007 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
278138, 277syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
279278adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
280 fnfvelrn 6317 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
281279, 266, 280syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
282276, 281eqeltrrd 2699 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
283282expr 642 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
284196, 283orim12d 882 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
285168, 284mpd 15 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
286285orcomd 403 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
287286ord 392 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
288287impr 648 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
289164, 288sylan2b 492 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
290163, 289remulcld 10021 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℝ)
291162, 290remulcld 10021 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℝ)
292291reim0d 13906 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = 0)
293 fzfid 12719 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
294140, 158, 292, 293fsumss 14396 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
29514adantr 481 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℕ0)
296 elfznn0 12381 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
297296adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
298 nn0mulcl 11280 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ0𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
29975, 297, 298sylancr 694 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ0)
300299nn0zd 11431 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
301 bccl 13056 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
302295, 300, 301syl2anc 692 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
303302nn0red 11303 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
304 fznn0sub 12322 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑀𝑗) ∈ ℕ0)
305304adantl 482 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀𝑗) ∈ ℕ0)
306 reexpcl 12824 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ (𝑀𝑗) ∈ ℕ0) → (-1↑(𝑀𝑗)) ∈ ℝ)
307192, 305, 306sylancr 694 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℝ)
308303, 307remulcld 10021 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) ∈ ℝ)
309 2z 11360 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
310 znegcl 11363 . . . . . . . . . . . . . . . 16 (2 ∈ ℤ → -2 ∈ ℤ)
311309, 310ax-mp 5 . . . . . . . . . . . . . . 15 -2 ∈ ℤ
312 rpexpcl 12826 . . . . . . . . . . . . . . 15 (((tan‘𝐴) ∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ+)
3132, 311, 312sylancl 693 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ+)
314313rpred 11823 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
315 reexpcl 12824 . . . . . . . . . . . . 13 ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
316314, 296, 315syl2an 494 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
317308, 316remulcld 10021 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
318317recnd 10019 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
319 mulcl 9971 . . . . . . . . . 10 ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
3205, 318, 319sylancr 694 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
321320addid2d 10188 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
322302nn0cnd 11304 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
323307recnd 10019 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℂ)
324316recnd 10019 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
325322, 323, 324mulassd 10014 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
326325oveq2d 6626 . . . . . . . . 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 10011 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
329327, 322, 328mul12d 10196 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
330326, 329eqtrd 2655 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
331 bccmpl 13043 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
332295, 300, 331syl2anc 692 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
333108adantr 481 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
334299nn0cnd 11304 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
335333, 334nncand 10348 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
336335oveq2d 6626 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
3372adantr 481 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ+)
338337rpcnd 11825 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
339 expneg 12815 . . . . . . . . . . . . . 14 (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
340338, 299, 339syl2anc 692 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
341297nn0cnd 11304 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
342 mulneg1 10417 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
343110, 341, 342sylancr 694 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
344343oveq2d 6626 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
345337rpne0d 11828 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
346338, 345, 300exprecd 12963 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
347340, 344, 3463eqtr4d 2665 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
348311a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
349297nn0zd 11431 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
350 expmulz 12853 . . . . . . . . . . . . 13 ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
351338, 345, 348, 349, 350syl22anc 1324 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
352336, 347, 3513eqtr2d 2661 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
3537oveq1i 6620 . . . . . . . . . . . . . . 15 (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
35411adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
355354nncnd 10987 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
356 1cnd 10007 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
357355, 356, 334addsubd 10364 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
358 2cnd 11044 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
359226ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
360358, 359, 341subdid 10437 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
361360oveq1d 6625 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
362357, 361eqtr4d 2658 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
363353, 362syl5eq 2667 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
364363oveq2d 6626 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀𝑗)) + 1)))
365 nn0mulcl 11280 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑀𝑗) ∈ ℕ0) → (2 · (𝑀𝑗)) ∈ ℕ0)
36675, 305, 365sylancr 694 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) ∈ ℕ0)
367 expp1 12814 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑀𝑗)) ∈ ℕ0) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
3685, 366, 367sylancr 694 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
36975a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ0)
370327, 305, 369expmuld 12958 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = ((i↑2)↑(𝑀𝑗)))
371169oveq1i 6620 . . . . . . . . . . . . . . 15 ((i↑2)↑(𝑀𝑗)) = (-1↑(𝑀𝑗))
372370, 371syl6eq 2671 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = (-1↑(𝑀𝑗)))
373372oveq1d 6625 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀𝑗))) · i) = ((-1↑(𝑀𝑗)) · i))
374364, 368, 3733eqtrd 2659 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀𝑗)) · i))
375 mulcom 9973 . . . . . . . . . . . . 13 (((-1↑(𝑀𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
376323, 5, 375sylancl 693 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
377374, 376eqtrd 2655 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀𝑗))))
378352, 377oveq12d 6628 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
379 mulcl 9971 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (-1↑(𝑀𝑗)) ∈ ℂ) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
3805, 323, 379sylancr 694 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
381380, 324mulcomd 10012 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
382327, 323, 324mulassd 10014 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
383378, 381, 3823eqtr2rd 2662 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
384332, 383oveq12d 6628 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
385321, 330, 3843eqtrd 2659 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
386385fveq2d 6157 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
387 0re 9991 . . . . . . 7 0 ∈ ℝ
388 crim 13796 . . . . . . 7 ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389387, 317, 388sylancr 694 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390386, 389eqtr3d 2657 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
391390sumeq2dv 14374 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
392159, 294, 3913eqtr3d 2663 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
393293, 155fsumim 14475 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
394313rpcnd 11825 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
395 oveq1 6617 . . . . . . 7 (𝑡 = ((tan‘𝐴)↑-2) → (𝑡𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
396395oveq2d 6626 . . . . . 6 (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
397396sumeq2sdv 14375 . . . . 5 (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
398 basel.p . . . . 5 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
399 sumex 14359 . . . . 5 Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
400397, 398, 399fvmpt 6244 . . . 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 2665 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
40351, 58rerpdivcld 11854 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
40453, 58rerpdivcld 11854 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
405403, 404crimd 13913 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
40666, 402, 4053eqtr3d 2663 1 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  cdif 3556  wss 3559   class class class wbr 4618  cmpt 4678  ran crn 5080   Fn wfn 5847  wf 5848  1-1wf1 5849  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  cc 9885  cr 9886  0cc0 9887  1c1 9888  ici 9889   + caddc 9890   · cmul 9892   < clt 10025  cle 10026  cmin 10217  -cneg 10218   / cdiv 10635  cn 10971  2c2 11021  0cn0 11243  cz 11328  cuz 11638  +crp 11783  (,)cioo 12124  ...cfz 12275  cexp 12807  Ccbc 13036  cim 13779  Σcsu 14357  sincsin 14726  cosccos 14727  tanctan 14728  πcpi 14729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-seq 12749  df-exp 12808  df-fac 13008  df-bc 13037  df-hash 13065  df-shft 13748  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-limsup 14143  df-clim 14160  df-rlim 14161  df-sum 14358  df-ef 14730  df-sin 14732  df-cos 14733  df-tan 14734  df-pi 14735  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-hom 15894  df-cco 15895  df-rest 16011  df-topn 16012  df-0g 16030  df-gsum 16031  df-topgen 16032  df-pt 16033  df-prds 16036  df-xrs 16090  df-qtop 16095  df-imas 16096  df-xps 16098  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-mulg 17469  df-cntz 17678  df-cmn 18123  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-perf 20860  df-cn 20950  df-cnp 20951  df-haus 21038  df-tx 21284  df-hmeo 21477  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-xms 22044  df-ms 22045  df-tms 22046  df-cncf 22600  df-limc 23549  df-dv 23550
This theorem is referenced by:  basellem4  24723
  Copyright terms: Public domain W3C validator