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

Theorem basellem3 25356
Description: Lemma for basel 25363. 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 24787 . . . . . . . 8 (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ+)
21adantl 474 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ+)
32rpreccld 12252 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ+)
43rpcnd 12244 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5 ax-icn 10388 . . . . . 6 i ∈ ℂ
65a1i 11 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7 basel.n . . . . . . 7 𝑁 = ((2 · 𝑀) + 1)
8 2nn 11507 . . . . . . . . 9 2 ∈ ℕ
9 simpl 475 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10 nnmulcl 11458 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
118, 9, 10sylancr 578 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
1211peano2nnd 11452 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
137, 12syl5eqel 2864 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
1413nnnn0d 11761 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ0)
15 binom 15039 . . . . 5 (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
164, 6, 14, 15syl3anc 1351 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))))
17 elioore 12578 . . . . . . . . . . 11 (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
1817adantl 474 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
1918recoscld 15351 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
2019recnd 10462 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
2118resincld 15350 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
2221recnd 10462 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23 mulcl 10413 . . . . . . . . 9 ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
245, 22, 23sylancr 578 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
2520, 24addcld 10453 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26 sincosq1sgn 24781 . . . . . . . . . 10 (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2726adantl 474 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
2827simpld 487 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
2928gt0ne0d 10999 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
3025, 22, 29, 14expdivd 13333 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
3120, 24, 22, 29divdird 11249 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
3218recnd 10462 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
3327simprd 488 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
3433gt0ne0d 10999 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35 tanval 15335 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3632, 34, 35syl2anc 576 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
3736oveq2d 6986 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
3822, 20, 29, 34recdivd 11228 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
3937, 38eqtr2d 2809 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
406, 22, 29divcan4d 11217 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
4139, 40oveq12d 6988 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
4231, 41eqtrd 2808 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
4342oveq1d 6985 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
4413nnzd 11893 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45 demoivre 15407 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4632, 44, 45syl2anc 576 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
4746oveq1d 6985 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4830, 43, 473eqtr3d 2816 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
4913nnred 11450 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
5049, 18remulcld 10464 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
5150recoscld 15351 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
5251recnd 10462 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
5350resincld 15350 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
5453recnd 10462 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55 mulcl 10413 . . . . . . 7 ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
565, 54, 55sylancr 578 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
5721, 28elrpd 12239 . . . . . . . 8 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ+)
5857, 44rpexpcld 13417 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ+)
5958rpcnd 12244 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
6058rpne0d 12247 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
6152, 56, 59, 60divdird 11249 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
626, 54, 59, 60divassd 11246 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
6362oveq2d 6986 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6448, 61, 633eqtrd 2812 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6516, 64eqtr3d 2810 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
6665fveq2d 6497 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67 oveq2 6978 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68 oveq2 6978 . . . . . . . . 9 (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
6968oveq2d 6986 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70 oveq2 6978 . . . . . . . 8 (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
7169, 70oveq12d 6988 . . . . . . 7 (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
7267, 71oveq12d 6988 . . . . . 6 (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
7372fveq2d 6497 . . . . 5 (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74 fzfid 13150 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75 2nn0 11720 . . . . . . . . . . . . 13 2 ∈ ℕ0
76 elfznn0 12810 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0)
7776adantl 474 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0)
78 nn0mulcl 11739 . . . . . . . . . . . . 13 ((2 ∈ ℕ0𝑘 ∈ ℕ0) → (2 · 𝑘) ∈ ℕ0)
7975, 77, 78sylancr 578 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ0)
8079nn0red 11762 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
8111nnred 11450 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
8281adantr 473 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
8349adantr 473 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84 elfzle2 12721 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘𝑀)
8584adantl 474 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘𝑀)
8677nn0red 11762 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87 nnre 11441 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
8887ad2antrr 713 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89 2re 11508 . . . . . . . . . . . . . . 15 2 ∈ ℝ
90 2pos 11544 . . . . . . . . . . . . . . 15 0 < 2
9189, 90pm3.2i 463 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
9291a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93 lemul2 11288 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9486, 88, 92, 93syl3anc 1351 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
9585, 94mpbid 224 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
9682lep1d 11366 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
9796, 7syl6breqr 4965 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
9880, 82, 83, 95, 97letrd 10591 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99 nn0uz 12088 . . . . . . . . . . . 12 0 = (ℤ‘0)
10079, 99syl6eleq 2870 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ‘0))
10144adantr 473 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102 elfz5 12710 . . . . . . . . . . 11 (((2 · 𝑘) ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103100, 101, 102syl2anc 576 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
10498, 103mpbird 249 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105 fznn0sub2 12824 . . . . . . . . 9 ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106104, 105syl 17 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107106ex 405 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
10813nncnd 11451 . . . . . . . . . . 11 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109108adantr 473 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110 2cn 11509 . . . . . . . . . . 11 2 ∈ ℂ
111 elfzelz 12718 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112111zcnd 11895 . . . . . . . . . . . 12 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113112ad2antrl 715 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114 mulcl 10413 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115110, 113, 114sylancr 578 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116112ssriv 3856 . . . . . . . . . . . 12 (0...𝑀) ⊆ ℂ
117 simprr 760 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118116, 117sseldi 3850 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119 mulcl 10413 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120110, 118, 119sylancr 578 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121109, 115, 120subcanad 10835 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122 2cnne0 11651 . . . . . . . . . . 11 (2 ∈ ℂ ∧ 2 ≠ 0)
123122a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124 mulcan 11072 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125113, 118, 123, 124syl3anc 1351 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126121, 125bitrd 271 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127126ex 405 . . . . . . 7 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128107, 127dom2lem 8340 . . . . . 6 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129 f1f1orn 6449 . . . . . 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 6978 . . . . . . . 8 (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132131oveq2d 6986 . . . . . . 7 (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133 eqid 2772 . . . . . . 7 (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134 ovex 7002 . . . . . . 7 (𝑁 − (2 · 𝑗)) ∈ V
135132, 133, 134fvmpt 6589 . . . . . 6 (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136135adantl 474 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137106fmpttd 6696 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138137frnd 6345 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
139138sselda 3852 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
140 bccl2 13492 . . . . . . . . . . 11 (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
141140adantl 474 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
142141nncnd 11451 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
1432rprecred 12253 . . . . . . . . . . . 12 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
144 fznn0sub 12749 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → (𝑁𝑚) ∈ ℕ0)
145 reexpcl 13255 . . . . . . . . . . . 12 (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁𝑚) ∈ ℕ0) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
146143, 144, 145syl2an 586 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
147146recnd 10462 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℂ)
148 elfznn0 12810 . . . . . . . . . . . 12 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
149148adantl 474 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ0)
150 expcl 13256 . . . . . . . . . . 11 ((i ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (i↑𝑚) ∈ ℂ)
1515, 149, 150sylancr 578 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
152147, 151mulcld 10454 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℂ)
153142, 152mulcld 10454 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
154139, 153syldan 582 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℂ)
155154imcld 14409 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℝ)
156155recnd 10462 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) ∈ ℂ)
15773, 74, 130, 136, 156fsumf1o 14934 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
158 eldifi 3987 . . . . . . . 8 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
159141nnred 11450 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
160158, 159sylan2 583 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
161158, 146sylan2 583 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁𝑚)) ∈ ℝ)
162 eldif 3833 . . . . . . . . 9 (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
163 elfzelz 12718 . . . . . . . . . . . . . . 15 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
164163adantl 474 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
165 zeo 11875 . . . . . . . . . . . . . 14 (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
166164, 165syl 17 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167 i2 13374 . . . . . . . . . . . . . . . . . 18 (i↑2) = -1
168167oveq1i 6980 . . . . . . . . . . . . . . . . 17 ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
169 simprr 760 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
170148ad2antrl 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
171 nn0re 11711 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0𝑚 ∈ ℝ)
172 nn0ge0 11728 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
173 divge0 11304 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
17489, 90, 173mpanr12 692 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
175171, 172, 174syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ0 → 0 ≤ (𝑚 / 2))
176170, 175syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
177 elnn0z 11800 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 / 2) ∈ ℕ0 ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
178169, 176, 177sylanbrc 575 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ0)
179 expmul 13283 . . . . . . . . . . . . . . . . . . 19 ((i ∈ ℂ ∧ 2 ∈ ℕ0 ∧ (𝑚 / 2) ∈ ℕ0) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
1805, 75, 178, 179mp3an12i 1444 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
181170nn0cnd 11763 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
182 2ne0 11545 . . . . . . . . . . . . . . . . . . . . 21 2 ≠ 0
183 divcan2 11101 . . . . . . . . . . . . . . . . . . . . 21 ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
184110, 182, 183mp3an23 1432 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
185181, 184syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
186185oveq2d 6986 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
187180, 186eqtr3d 2810 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
188168, 187syl5eqr 2822 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
189 neg1rr 11556 . . . . . . . . . . . . . . . . 17 -1 ∈ ℝ
190 reexpcl 13255 . . . . . . . . . . . . . . . . 17 ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ0) → (-1↑(𝑚 / 2)) ∈ ℝ)
191189, 178, 190sylancr 578 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
192188, 191eqeltrrd 2861 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
193192expr 449 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
194144ad2antrl 715 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℕ0)
195 nn0re 11711 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → (𝑁𝑚) ∈ ℝ)
196 nn0ge0 11728 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ (𝑁𝑚))
197 divge0 11304 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁𝑚) / 2))
19889, 90, 197mpanr12 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁𝑚) ∈ ℝ ∧ 0 ≤ (𝑁𝑚)) → 0 ≤ ((𝑁𝑚) / 2))
199195, 196, 198syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑚) ∈ ℕ0 → 0 ≤ ((𝑁𝑚) / 2))
200194, 199syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁𝑚) / 2))
201194nn0red 11762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℝ)
20249adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
203 peano2re 10607 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
204202, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
205148ad2antrl 715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ0)
206205, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
207205nn0red 11762 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
208202, 207subge02d 11027 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁𝑚) ≤ 𝑁))
209206, 208mpbid 224 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ≤ 𝑁)
210202ltp1d 11365 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
211201, 202, 204, 209, 210lelttrd 10592 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (𝑁 + 1))
212 2t1e2 11604 . . . . . . . . . . . . . . . . . . . . . . . . 25 (2 · 1) = 2
213 df-2 11497 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 = (1 + 1)
214212, 213eqtr2i 2797 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 + 1) = (2 · 1)
215214oveq2i 6981 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
2167oveq1i 6980 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
21711nncnd 11451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
218217adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
219 1cnd 10428 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
220218, 219, 219addassd 10456 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
221216, 220syl5eq 2820 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
222 2cnd 11512 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
223 nncn 11442 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
224223ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
225222, 224, 219adddid 10458 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
226215, 221, 2253eqtr4a 2834 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
227211, 226breqtrd 4949 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) < (2 · (𝑀 + 1)))
228 nnz 11811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
229228ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
230229peano2zd 11897 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
231230zred 11894 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
23291a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
233 ltdivmul 11310 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
234201, 231, 232, 233syl3anc 1351 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) < (𝑀 + 1) ↔ (𝑁𝑚) < (2 · (𝑀 + 1))))
235227, 234mpbird 249 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) < (𝑀 + 1))
236108adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
237205nn0cnd 11763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
238236, 237, 219pnpcan2d 10830 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁𝑚))
239226oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
240238, 239eqtr3d 2810 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
241240oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
242230zcnd 11895 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
243 mulcl 10413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
244110, 242, 243sylancr 578 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
245 peano2cn 10606 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → (𝑚 + 1) ∈ ℂ)
246237, 245syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈ ℂ)
247122a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℂ ∧ 2 ≠ 0))
248 divsubdir 11129 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
249244, 246, 247, 248syl3anc 1351 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
250182a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠ 0)
251242, 222, 250divcan3d 11216 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
252251oveq1d 6985 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
253241, 249, 2523eqtrd 2812 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
254 simprr 760 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
255230, 254zsubcld 11899 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
256253, 255eqeltrd 2860 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ ℤ)
257 zleltp1 11840 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
258256, 229, 257syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ≤ 𝑀 ↔ ((𝑁𝑚) / 2) < (𝑀 + 1)))
259235, 258mpbird 249 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ≤ 𝑀)
260 0zd 11799 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
261 elfz 12708 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁𝑚) / 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
262256, 260, 229, 261syl3anc 1351 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁𝑚) / 2) ∈ (0...𝑀) ↔ (0 ≤ ((𝑁𝑚) / 2) ∧ ((𝑁𝑚) / 2) ≤ 𝑀)))
263200, 259, 262mpbir2and 700 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁𝑚) / 2) ∈ (0...𝑀))
264 oveq2 6978 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = ((𝑁𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁𝑚) / 2)))
265264oveq2d 6986 . . . . . . . . . . . . . . . . . . 19 (𝑘 = ((𝑁𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
266 ovex 7002 . . . . . . . . . . . . . . . . . . 19 (𝑁 − (2 · ((𝑁𝑚) / 2))) ∈ V
267265, 133, 266fvmpt 6589 . . . . . . . . . . . . . . . . . 18 (((𝑁𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
268263, 267syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = (𝑁 − (2 · ((𝑁𝑚) / 2))))
269194nn0cnd 11763 . . . . . . . . . . . . . . . . . . 19 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁𝑚) ∈ ℂ)
270269, 222, 250divcan2d 11213 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁𝑚) / 2)) = (𝑁𝑚))
271270oveq2d 6986 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁𝑚) / 2))) = (𝑁 − (𝑁𝑚)))
272236, 237nncand 10797 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁𝑚)) = 𝑚)
273268, 271, 2723eqtrd 2812 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) = 𝑚)
274137ffnd 6339 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
275 fnfvelrn 6667 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
276274, 263, 275syl2an2r 672 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
277273, 276eqeltrrd 2861 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
278277expr 449 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
279193, 278orim12d 947 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
280166, 279mpd 15 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
281280orcomd 857 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
282281ord 850 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
283282impr 447 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
284162, 283sylan2b 584 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
285161, 284remulcld 10464 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)) ∈ ℝ)
286160, 285remulcld 10464 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚))) ∈ ℝ)
287286reim0d 14439 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = 0)
288 fzfid 13150 . . . . 5 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
289138, 156, 287, 288fsumss 14936 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
290 elfznn0 12810 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
291290adantl 474 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
292 nn0mulcl 11739 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ0𝑗 ∈ ℕ0) → (2 · 𝑗) ∈ ℕ0)
29375, 291, 292sylancr 578 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ0)
294293nn0zd 11892 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
295 bccl 13491 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
29614, 294, 295syl2an2r 672 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ0)
297296nn0red 11762 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
298 fznn0sub 12749 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → (𝑀𝑗) ∈ ℕ0)
299298adantl 474 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀𝑗) ∈ ℕ0)
300 reexpcl 13255 . . . . . . . . . . . . . 14 ((-1 ∈ ℝ ∧ (𝑀𝑗) ∈ ℕ0) → (-1↑(𝑀𝑗)) ∈ ℝ)
301189, 299, 300sylancr 578 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℝ)
302297, 301remulcld 10464 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) ∈ ℝ)
303 2z 11821 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
304 znegcl 11824 . . . . . . . . . . . . . . . 16 (2 ∈ ℤ → -2 ∈ ℤ)
305303, 304ax-mp 5 . . . . . . . . . . . . . . 15 -2 ∈ ℤ
306 rpexpcl 13257 . . . . . . . . . . . . . . 15 (((tan‘𝐴) ∈ ℝ+ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ+)
3072, 305, 306sylancl 577 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ+)
308307rpred 12242 . . . . . . . . . . . . 13 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
309 reexpcl 13255 . . . . . . . . . . . . 13 ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ0) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
310308, 290, 309syl2an 586 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
311302, 310remulcld 10464 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
312311recnd 10462 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
313 mulcl 10413 . . . . . . . . . 10 ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
3145, 312, 313sylancr 578 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
315314addid2d 10635 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
316296nn0cnd 11763 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
317301recnd 10462 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀𝑗)) ∈ ℂ)
318310recnd 10462 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
319316, 317, 318mulassd 10457 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
320319oveq2d 6986 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
3215a1i 11 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → i ∈ ℂ)
322317, 318mulcld 10454 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
323321, 316, 322mul12d 10643 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
324320, 323eqtrd 2808 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
325 bccmpl 13478 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
32614, 294, 325syl2an2r 672 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
327108adantr 473 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
328293nn0cnd 11763 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
329327, 328nncand 10797 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
330329oveq2d 6986 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
3312adantr 473 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ+)
332331rpcnd 12244 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
333 expneg 13246 . . . . . . . . . . . . . 14 (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ0) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
334332, 293, 333syl2anc 576 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
335291nn0cnd 11763 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
336 mulneg1 10871 . . . . . . . . . . . . . . 15 ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
337110, 335, 336sylancr 578 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
338337oveq2d 6986 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
339331rpne0d 12247 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
340332, 339, 294exprecd 13327 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
341334, 338, 3403eqtr4d 2818 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
342305a1i 11 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
343291nn0zd 11892 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
344 expmulz 13284 . . . . . . . . . . . . 13 ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
345332, 339, 342, 343, 344syl22anc 826 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
346330, 341, 3453eqtr2d 2814 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
3477oveq1i 6980 . . . . . . . . . . . . . . 15 (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
34811adantr 473 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
349348nncnd 11451 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
350 1cnd 10428 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
351349, 350, 328addsubd 10813 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
352 2cnd 11512 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
353223ad2antrr 713 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
354352, 353, 335subdid 10891 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
355354oveq1d 6985 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
356351, 355eqtr4d 2811 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
357347, 356syl5eq 2820 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀𝑗)) + 1))
358357oveq2d 6986 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀𝑗)) + 1)))
359 nn0mulcl 11739 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ0 ∧ (𝑀𝑗) ∈ ℕ0) → (2 · (𝑀𝑗)) ∈ ℕ0)
36075, 299, 359sylancr 578 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀𝑗)) ∈ ℕ0)
361 expp1 13245 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (2 · (𝑀𝑗)) ∈ ℕ0) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
3625, 360, 361sylancr 578 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀𝑗)) + 1)) = ((i↑(2 · (𝑀𝑗))) · i))
36375a1i 11 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ0)
364321, 299, 363expmuld 13322 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = ((i↑2)↑(𝑀𝑗)))
365167oveq1i 6980 . . . . . . . . . . . . . . 15 ((i↑2)↑(𝑀𝑗)) = (-1↑(𝑀𝑗))
366364, 365syl6eq 2824 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀𝑗))) = (-1↑(𝑀𝑗)))
367366oveq1d 6985 . . . . . . . . . . . . 13 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀𝑗))) · i) = ((-1↑(𝑀𝑗)) · i))
368358, 362, 3673eqtrd 2812 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀𝑗)) · i))
369 mulcom 10415 . . . . . . . . . . . . 13 (((-1↑(𝑀𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
370317, 5, 369sylancl 577 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀𝑗)) · i) = (i · (-1↑(𝑀𝑗))))
371368, 370eqtrd 2808 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀𝑗))))
372346, 371oveq12d 6988 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
373 mulcl 10413 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ (-1↑(𝑀𝑗)) ∈ ℂ) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
3745, 317, 373sylancr 578 . . . . . . . . . . 11 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀𝑗))) ∈ ℂ)
375374, 318mulcomd 10455 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀𝑗)))))
376321, 317, 318mulassd 10457 . . . . . . . . . 10 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
377372, 375, 3763eqtr2rd 2815 . . . . . . . . 9 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
378326, 377oveq12d 6988 . . . . . . . 8 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
379315, 324, 3783eqtrd 2812 . . . . . . 7 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
380379fveq2d 6497 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
381 0re 10435 . . . . . . 7 0 ∈ ℝ
382 crim 14329 . . . . . . 7 ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
383381, 311, 382sylancr 578 . . . . . 6 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
384380, 383eqtr3d 2810 . . . . 5 (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
385384sumeq2dv 14914 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
386157, 289, 3853eqtr3d 2816 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
387288, 153fsumim 15018 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))))
388307rpcnd 12244 . . . 4 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
389 oveq1 6977 . . . . . . 7 (𝑡 = ((tan‘𝐴)↑-2) → (𝑡𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
390389oveq2d 6986 . . . . . 6 (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
391390sumeq2sdv 14915 . . . . 5 (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
392 basel.p . . . . 5 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
393 sumex 14899 . . . . 5 Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
394391, 392, 393fvmpt 6589 . . . 4 (((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
395388, 394syl 17 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
396386, 387, 3953eqtr4d 2818 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
39751, 58rerpdivcld 12273 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
39853, 58rerpdivcld 12273 . . 3 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
399397, 398crimd 14446 . 2 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
40066, 396, 3993eqtr3d 2816 1 ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 833   = wceq 1507  wcel 2050  wne 2961  cdif 3820   class class class wbr 4923  cmpt 5002  ran crn 5402   Fn wfn 6177  1-1wf1 6179  1-1-ontowf1o 6181  cfv 6182  (class class class)co 6970  cc 10327  cr 10328  0cc0 10329  1c1 10330  ici 10331   + caddc 10332   · cmul 10334   < clt 10468  cle 10469  cmin 10664  -cneg 10665   / cdiv 11092  cn 11433  2c2 11489  0cn0 11701  cz 11787  cuz 12052  +crp 12198  (,)cioo 12548  ...cfz 12702  cexp 13238  Ccbc 13471  cim 14312  Σcsu 14897  sincsin 15271  cosccos 15272  tanctan 15273  πcpi 15274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8892  ax-cnex 10385  ax-resscn 10386  ax-1cn 10387  ax-icn 10388  ax-addcl 10389  ax-addrcl 10390  ax-mulcl 10391  ax-mulrcl 10392  ax-mulcom 10393  ax-addass 10394  ax-mulass 10395  ax-distr 10396  ax-i2m1 10397  ax-1ne0 10398  ax-1rid 10399  ax-rnegex 10400  ax-rrecex 10401  ax-cnre 10402  ax-pre-lttri 10403  ax-pre-lttrn 10404  ax-pre-ltadd 10405  ax-pre-mulgt0 10406  ax-pre-sup 10407  ax-addf 10408  ax-mulf 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5306  df-eprel 5311  df-po 5320  df-so 5321  df-fr 5360  df-se 5361  df-we 5362  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-om 7391  df-1st 7495  df-2nd 7496  df-supp 7628  df-wrecs 7744  df-recs 7806  df-rdg 7844  df-1o 7899  df-2o 7900  df-oadd 7903  df-er 8083  df-map 8202  df-pm 8203  df-ixp 8254  df-en 8301  df-dom 8302  df-sdom 8303  df-fin 8304  df-fsupp 8623  df-fi 8664  df-sup 8695  df-inf 8696  df-oi 8763  df-card 9156  df-cda 9382  df-pnf 10470  df-mnf 10471  df-xr 10472  df-ltxr 10473  df-le 10474  df-sub 10666  df-neg 10667  df-div 11093  df-nn 11434  df-2 11497  df-3 11498  df-4 11499  df-5 11500  df-6 11501  df-7 11502  df-8 11503  df-9 11504  df-n0 11702  df-z 11788  df-dec 11906  df-uz 12053  df-q 12157  df-rp 12199  df-xneg 12318  df-xadd 12319  df-xmul 12320  df-ioo 12552  df-ioc 12553  df-ico 12554  df-icc 12555  df-fz 12703  df-fzo 12844  df-fl 12971  df-seq 13179  df-exp 13239  df-fac 13443  df-bc 13472  df-hash 13500  df-shft 14281  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-limsup 14683  df-clim 14700  df-rlim 14701  df-sum 14898  df-ef 15275  df-sin 15277  df-cos 15278  df-tan 15279  df-pi 15280  df-struct 16335  df-ndx 16336  df-slot 16337  df-base 16339  df-sets 16340  df-ress 16341  df-plusg 16428  df-mulr 16429  df-starv 16430  df-sca 16431  df-vsca 16432  df-ip 16433  df-tset 16434  df-ple 16435  df-ds 16437  df-unif 16438  df-hom 16439  df-cco 16440  df-rest 16546  df-topn 16547  df-0g 16565  df-gsum 16566  df-topgen 16567  df-pt 16568  df-prds 16571  df-xrs 16625  df-qtop 16630  df-imas 16631  df-xps 16633  df-mre 16709  df-mrc 16710  df-acs 16712  df-mgm 17704  df-sgrp 17746  df-mnd 17757  df-submnd 17798  df-mulg 18006  df-cntz 18212  df-cmn 18662  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-fbas 20238  df-fg 20239  df-cnfld 20242  df-top 21200  df-topon 21217  df-topsp 21239  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-perf 21443  df-cn 21533  df-cnp 21534  df-haus 21621  df-tx 21868  df-hmeo 22061  df-fil 22152  df-fm 22244  df-flim 22245  df-flf 22246  df-xms 22627  df-ms 22628  df-tms 22629  df-cncf 23183  df-limc 24161  df-dv 24162
This theorem is referenced by:  basellem4  25357
  Copyright terms: Public domain W3C validator