basellem3 - Metamath Proof Explorer

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

Theorem basellem3 27060

Description: Lemma for basel 27067. 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.

Step	Hyp	Ref	Expression
1		tanrpcl 26481	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ⁺)
2	1	adantl 481	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ⁺)
3	2	rpreccld 12987	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ⁺)
4	3	rpcnd 12979	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5		ax-icn 11088	. . . . . 6 ⊢ i ∈ ℂ
6	5	a1i 11	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7		basel.n	. . . . . . 7 ⊢ 𝑁 = ((2 · 𝑀) + 1)
8		2nn 12245	. . . . . . . . 9 ⊢ 2 ∈ ℕ
9		simpl 482	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10		nnmulcl 12189	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
11	8, 9, 10	sylancr 588	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
12	11	peano2nnd 12182	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
13	7, 12	eqeltrid 2841	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
14	13	nnnn0d 12489	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ₀)
15		binom 15786	. . . . 5 ⊢ (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
16	4, 6, 14, 15	syl3anc 1374	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
17		elioore 13319	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
18	17	adantl 481	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
19	18	recoscld 16102	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
20	19	recnd 11164	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
21	18	resincld 16101	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
22	21	recnd 11164	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23		mulcl 11113	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
24	5, 22, 23	sylancr 588	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
25	20, 24	addcld 11155	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26		sincosq1sgn 26475	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
27	26	adantl 481	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
28	27	simpld 494	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
29	28	gt0ne0d 11705	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
30	25, 22, 29, 14	expdivd 14113	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
31	20, 24, 22, 29	divdird 11960	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
32	18	recnd 11164	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
33	27	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
34	33	gt0ne0d 11705	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35		tanval 16086	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	32, 34, 35	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7376	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
38	22, 20, 29, 34	recdivd 11939	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
39	37, 38	eqtr2d 2773	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
40	6, 22, 29	divcan4d 11928	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
41	39, 40	oveq12d 7378	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
42	31, 41	eqtrd 2772	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
43	42	oveq1d 7375	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
44	13	nnzd 12541	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45		demoivre 16158	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
46	32, 44, 45	syl2anc 585	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
47	46	oveq1d 7375	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
48	30, 43, 47	3eqtr3d 2780	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
49	13	nnred 12180	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
50	49, 18	remulcld 11166	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
51	50	recoscld 16102	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
52	51	recnd 11164	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
53	50	resincld 16101	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
54	53	recnd 11164	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55		mulcl 11113	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
56	5, 54, 55	sylancr 588	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
57	21, 28	elrpd 12974	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ⁺)
58	57, 44	rpexpcld 14200	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ⁺)
59	58	rpcnd 12979	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
60	58	rpne0d 12982	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
61	52, 56, 59, 60	divdird 11960	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
62	6, 54, 59, 60	divassd 11957	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
63	62	oveq2d 7376	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
64	48, 61, 63	3eqtrd 2776	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
65	16, 64	eqtr3d 2774	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
66	65	fveq2d 6838	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67		oveq2 7368	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68		oveq2 7368	. . . . . . . . 9 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
69	68	oveq2d 7376	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70		oveq2 7368	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
71	69, 70	oveq12d 7378	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
72	67, 71	oveq12d 7378	. . . . . 6 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
73	72	fveq2d 6838	. . . . 5 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74		fzfid 13926	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75		2nn0 12445	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
76		elfznn0 13565	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ₀)
77	76	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ₀)
78		nn0mulcl 12464	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
79	75, 77, 78	sylancr 588	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ₀)
80	79	nn0red 12490	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
81	11	nnred 12180	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
82	81	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
83	49	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84		elfzle2 13473	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀)
85	84	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀)
86	77	nn0red 12490	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87		nnre 12172	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
88	87	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89		2re 12246	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90		2pos 12275	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
91	89, 90	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ 0 < 2)
92	91	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93		lemul2 11999	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
94	86, 88, 92, 93	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
95	85, 94	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
96	82	lep1d 12078	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
97	96, 7	breqtrrdi 5128	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
98	80, 82, 83, 95, 97	letrd 11294	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99		nn0uz 12817	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
100	79, 99	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ_≥‘0))
101	44	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102		elfz5 13461	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ (ℤ_≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103	100, 101, 102	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
104	98, 103	mpbird 257	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105		fznn0sub2 13580	. . . . . . . . 9 ⊢ ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106	104, 105	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107	106	ex 412	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
108	13	nncnd 12181	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109	108	adantr 480	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110		2cn 12247	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
111		elfzelz 13469	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112	111	zcnd 12625	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113	112	ad2antrl 729	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114		mulcl 11113	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115	110, 113, 114	sylancr 588	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116	112	ssriv 3926	. . . . . . . . . . . 12 ⊢ (0...𝑀) ⊆ ℂ
117		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118	116, 117	sselid 3920	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119		mulcl 11113	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120	110, 118, 119	sylancr 588	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121	109, 115, 120	subcanad 11539	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122		2cnne0 12377	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124		mulcan 11778	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125	113, 118, 123, 124	syl3anc 1374	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126	121, 125	bitrd 279	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127	126	ex 412	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128	107, 127	dom2lem 8932	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129		f1f1orn 6785	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
130	128, 129	syl 17	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
131		oveq2 7368	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132	131	oveq2d 7376	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133		eqid 2737	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134		ovex 7393	. . . . . . 7 ⊢ (𝑁 − (2 · 𝑗)) ∈ V
135	132, 133, 134	fvmpt 6941	. . . . . 6 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136	135	adantl 481	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137	106	fmpttd 7061	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138	137	frnd 6670	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
139	138	sselda 3922	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
140		bccl2 14276	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
141	140	adantl 481	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
142	141	nncnd 12181	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
143	2	rprecred 12988	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
144		fznn0sub 13501	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈ ℕ₀)
145		reexpcl 14031	. . . . . . . . . . . 12 ⊢ (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁 − 𝑚) ∈ ℕ₀) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
146	143, 144, 145	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
147	146	recnd 11164	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ)
148		elfznn0 13565	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
149	148	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ₀)
150		expcl 14032	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ∧ 𝑚 ∈ ℕ₀) → (i↑𝑚) ∈ ℂ)
151	5, 149, 150	sylancr 588	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
152	147, 151	mulcld 11156	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ)
153	142, 152	mulcld 11156	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
154	139, 153	syldan 592	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
155	154	imcld 15148	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ)
156	155	recnd 11164	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ)
157	73, 74, 130, 136, 156	fsumf1o 15676	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
158		eldifi 4072	. . . . . . . 8 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
159	141	nnred 12180	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
160	158, 159	sylan2 594	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
161	158, 146	sylan2 594	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
162		eldif 3900	. . . . . . . . 9 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
163		elfzelz 13469	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
164	163	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
165		zeo 12606	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
166	164, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167		i2 14155	. . . . . . . . . . . . . . . . . 18 ⊢ (i↑2) = -1
168	167	oveq1i 7370	. . . . . . . . . . . . . . . . 17 ⊢ ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
169		simprr 773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
170	148	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
171		nn0re 12437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℝ)
172		nn0ge0 12453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ 𝑚)
173		divge0 12016	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
174	89, 90, 173	mpanr12 706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
175	171, 172, 174	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ (𝑚 / 2))
176	170, 175	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
177		elnn0z 12528	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 / 2) ∈ ℕ₀ ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
178	169, 176, 177	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ₀)
179		expmul 14060	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ (𝑚 / 2) ∈ ℕ₀) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
180	5, 75, 178, 179	mp3an12i 1468	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
181	170	nn0cnd 12491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
182		2ne0 12276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≠ 0
183		divcan2 11808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
184	110, 182, 183	mp3an23 1456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
186	185	oveq2d 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
187	180, 186	eqtr3d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
188	168, 187	eqtr3id 2786	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
189		neg1rr 12136	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℝ
190		reexpcl 14031	. . . . . . . . . . . . . . . . 17 ⊢ ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ₀) → (-1↑(𝑚 / 2)) ∈ ℝ)
191	189, 178, 190	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
192	188, 191	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
193	192	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
194		0zd 12527	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
195		nnz 12536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
196	195	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
197	108	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
198	148	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
199	198	nn0cnd 12491	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
200		1cnd 11130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
201	197, 199, 200	pnpcan2d 11534	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚))
202		2t1e2 12330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 · 1) = 2
203		df-2 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 = (1 + 1)
204	202, 203	eqtr2i 2761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 + 1) = (2 · 1)
205	204	oveq2i 7371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
206	7	oveq1i 7370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
207	11	nncnd 12181	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
208	207	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
209	208, 200, 200	addassd 11158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
210	206, 209	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
211		2cnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
212		nncn 12173	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
213	212	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
214	211, 213, 200	adddid 11160	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
215	205, 210, 214	3eqtr4a 2798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
216	215	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
217	201, 216	eqtr3d 2774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
218	217	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
219	196	peano2zd 12627	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
220	219	zcnd 12625	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
221		mulcl 11113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
222	110, 220, 221	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
223		peano2cn 11309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℂ → (𝑚 + 1) ∈ ℂ)
224	199, 223	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈ ℂ)
225	122	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℂ ∧ 2 ≠ 0))
226		divsubdir 11839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
227	222, 224, 225, 226	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
228	182	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ≠ 0)
229	220, 211, 228	divcan3d 11927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
230	229	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
231	218, 227, 230	3eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
232		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
233	219, 232	zsubcld 12629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
234	231, 233	eqeltrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ)
235	144	ad2antrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℕ₀)
236		nn0re 12437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → (𝑁 − 𝑚) ∈ ℝ)
237		nn0ge0 12453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ (𝑁 − 𝑚))
238		divge0 12016	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 𝑚) / 2))
239	89, 90, 238	mpanr12 706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2))
240	236, 237, 239	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ ((𝑁 − 𝑚) / 2))
241	235, 240	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁 − 𝑚) / 2))
242	235	nn0red 12490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ)
243	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
244		peano2re 11310	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
245	243, 244	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
246	198, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
247	198	nn0red 12490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
248	243, 247	subge02d 11733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁))
249	246, 248	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁)
250	243	ltp1d 12077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
251	242, 243, 245, 249, 250	lelttrd 11295	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1))
252	251, 215	breqtrd 5112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1)))
253	219	zred 12624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
254	91	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
255		ltdivmul 12022	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
256	242, 253, 254, 255	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
257	252, 256	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1))
258		zleltp1 12569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
259	234, 196, 258	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
260	257, 259	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀)
261	194, 196, 234, 241, 260	elfzd 13460	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀))
262		oveq2 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2)))
263	262	oveq2d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
264		ovex 7393	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V
265	263, 133, 264	fvmpt 6941	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
266	261, 265	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
267	235	nn0cnd 12491	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ)
268	267, 211, 228	divcan2d 11924	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚))
269	268	oveq2d 7376	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚)))
270	197, 199	nncand 11501	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚)
271	266, 269, 270	3eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚)
272	137	ffnd 6663	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
273		fnfvelrn 7026	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
274	272, 261, 273	syl2an2r 686	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
275	271, 274	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
276	275	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
277	193, 276	orim12d 967	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
278	166, 277	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
279	278	orcomd 872	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
280	279	ord 865	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
281	280	impr 454	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
282	162, 281	sylan2b 595	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
283	161, 282	remulcld 11166	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ)
284	160, 283	remulcld 11166	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ)
285	284	reim0d 15178	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0)
286		fzfid 13926	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
287	138, 156, 285, 286	fsumss 15678	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
288		elfznn0 13565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
289	288	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
290		nn0mulcl 12464	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ₀ ∧ 𝑗 ∈ ℕ₀) → (2 · 𝑗) ∈ ℕ₀)
291	75, 289, 290	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ₀)
292	291	nn0zd 12540	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
293		bccl 14275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
294	14, 292, 293	syl2an2r 686	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
295	294	nn0red 12490	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
296		fznn0sub 13501	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈ ℕ₀)
297	296	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈ ℕ₀)
298		reexpcl 14031	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
299	189, 297, 298	sylancr 588	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
300	295, 299	remulcld 11166	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ)
301		2z 12550	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
302		znegcl 12553	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
303	301, 302	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ -2 ∈ ℤ
304		rpexpcl 14033	. . . . . . . . . . . . . . 15 ⊢ (((tan‘𝐴) ∈ ℝ⁺ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
305	2, 303, 304	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
306	305	rpred 12977	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
307		reexpcl 14031	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
308	306, 288, 307	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
309	300, 308	remulcld 11166	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
310	309	recnd 11164	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
311		mulcl 11113	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
312	5, 310, 311	sylancr 588	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
313	312	addlidd 11338	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
314	294	nn0cnd 12491	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
315	299	recnd 11164	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ)
316	308	recnd 11164	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
317	314, 315, 316	mulassd 11159	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
318	317	oveq2d 7376	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
319	5	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → i ∈ ℂ)
320	315, 316	mulcld 11156	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
321	319, 314, 320	mul12d 11346	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
322	318, 321	eqtrd 2772	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
323		bccmpl 14262	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
324	14, 292, 323	syl2an2r 686	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
325	108	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
326	291	nn0cnd 12491	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
327	325, 326	nncand 11501	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
328	327	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
329	2	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ⁺)
330	329	rpcnd 12979	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
331		expneg 14022	. . . . . . . . . . . . . 14 ⊢ (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ₀) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
332	330, 291, 331	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
333	289	nn0cnd 12491	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
334		mulneg1 11577	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
335	110, 333, 334	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
336	335	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
337	329	rpne0d 12982	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
338	330, 337, 292	exprecd 14107	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
339	332, 336, 338	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
340	303	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
341	289	nn0zd 12540	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
342		expmulz 14061	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
343	330, 337, 340, 341, 342	syl22anc 839	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
344	328, 339, 343	3eqtr2d 2778	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
345	7	oveq1i 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
346	11	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
347	346	nncnd 12181	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
348		1cnd 11130	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
349	347, 348, 326	addsubd 11517	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
350		2cnd 12250	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
351	212	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
352	350, 351, 333	subdid 11597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
353	352	oveq1d 7375	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
354	349, 353	eqtr4d 2775	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
355	345, 354	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
356	355	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀 − 𝑗)) + 1)))
357		nn0mulcl 12464	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ₀ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
358	75, 297, 357	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
359		expp1 14021	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ₀) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
360	5, 358, 359	sylancr 588	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
361	75	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ₀)
362	319, 297, 361	expmuld 14102	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗)))
363	167	oveq1i 7370	. . . . . . . . . . . . . . 15 ⊢ ((i↑2)↑(𝑀 − 𝑗)) = (-1↑(𝑀 − 𝑗))
364	362, 363	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗)))
365	364	oveq1d 7375	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀 − 𝑗))) · i) = ((-1↑(𝑀 − 𝑗)) · i))
366	356, 360, 365	3eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i))
367		mulcom 11115	. . . . . . . . . . . . 13 ⊢ (((-1↑(𝑀 − 𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
368	315, 5, 367	sylancl 587	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
369	366, 368	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀 − 𝑗))))
370	344, 369	oveq12d 7378	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
371		mulcl 11113	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
372	5, 315, 371	sylancr 588	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
373	372, 316	mulcomd 11157	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
374	319, 315, 316	mulassd 11159	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
375	370, 373, 374	3eqtr2rd 2779	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
376	324, 375	oveq12d 7378	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
377	313, 322, 376	3eqtrd 2776	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
378	377	fveq2d 6838	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
379		0re 11137	. . . . . . 7 ⊢ 0 ∈ ℝ
380		crim 15068	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
381	379, 309, 380	sylancr 588	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
382	378, 381	eqtr3d 2774	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
383	382	sumeq2dv 15655	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
384	157, 287, 383	3eqtr3d 2780	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
385	286, 153	fsumim 15763	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
386	305	rpcnd 12979	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
387		oveq1 7367	. . . . . . 7 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
388	387	oveq2d 7376	. . . . . 6 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389	388	sumeq2sdv 15656	. . . . 5 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390		basel.p	. . . . 5 ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))
391		sumex 15641	. . . . 5 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
392	389, 390, 391	fvmpt 6941	. . . 4 ⊢ (((tan‘𝐴)↑-2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
393	386, 392	syl 17	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
394	384, 385, 393	3eqtr4d 2782	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
395	51, 58	rerpdivcld 13008	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
396	53, 58	rerpdivcld 13008	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
397	395, 396	crimd 15185	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
398	66, 394, 397	3eqtr3d 2780	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∖ cdif 3887 class class class wbr 5086 ↦ cmpt 5167 ran crn 5625 Fn wfn 6487 –1-1→wf1 6489 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7360 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 ici 11031 + caddc 11032 · cmul 11034 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 / cdiv 11798 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 (,)cioo 13289 ...cfz 13452 ↑cexp 14014 Ccbc 14255 ℑcim 15051 Σcsu 15639 sincsin 16019 cosccos 16020 tanctan 16021 πcpi 16022

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-supp 8104 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-2o 8399 df-er 8636 df-map 8768 df-pm 8769 df-ixp 8839 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-fsupp 9268 df-fi 9317 df-sup 9348 df-inf 9349 df-oi 9418 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-fac 14227 df-bc 14256 df-hash 14284 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15424 df-clim 15441 df-rlim 15442 df-sum 15640 df-ef 16023 df-sin 16025 df-cos 16026 df-tan 16027 df-pi 16028 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-mulg 19035 df-cntz 19283 df-cmn 19748 df-psmet 21336 df-xmet 21337 df-met 21338 df-bl 21339 df-mopn 21340 df-fbas 21341 df-fg 21342 df-cnfld 21345 df-top 22869 df-topon 22886 df-topsp 22908 df-bases 22921 df-cld 22994 df-ntr 22995 df-cls 22996 df-nei 23073 df-lp 23111 df-perf 23112 df-cn 23202 df-cnp 23203 df-haus 23290 df-tx 23537 df-hmeo 23730 df-fil 23821 df-fm 23913 df-flim 23914 df-flf 23915 df-xms 24295 df-ms 24296 df-tms 24297 df-cncf 24855 df-limc 25843 df-dv 25844

This theorem is referenced by: basellem4 27061

W3C validator