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 27415

Description: Lemma for basel 27422. 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 26838	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ⁺)
2	1	adantl 487	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ⁺)
3	2	rpreccld 13177	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ⁺)
4	3	rpcnd 13169	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5		ax-icn 11262	. . . . . 6 ⊢ i ∈ ℂ
6	5	a1i 11	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7		basel.n	. . . . . . 7 ⊢ 𝑁 = ((2 · 𝑀) + 1)
8		2nn 12419	. . . . . . . . 9 ⊢ 2 ∈ ℕ
9		simpl 488	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10		nnmulcl 12362	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
11	8, 9, 10	sylancr 599	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
12	11	peano2nnd 12355	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
13	7, 12	eqeltrid 2864	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
14	13	nnnn0d 12670	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ₀)
15		binom 16004	. . . . 5 ⊢ (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
16	4, 6, 14, 15	syl3anc 1398	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
17		elioore 13509	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
18	17	adantl 487	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
19	18	recoscld 16317	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
20	19	recnd 11340	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
21	18	resincld 16316	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
22	21	recnd 11340	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23		mulcl 11287	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
24	5, 22, 23	sylancr 599	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
25	20, 24	addcld 11331	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26		sincosq1sgn 26832	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
27	26	adantl 487	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
28	27	simpld 500	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
29	28	gt0ne0d 11883	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
30	25, 22, 29, 14	expdivd 14306	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
31	20, 24, 22, 29	divdird 12134	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
32	18	recnd 11340	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
33	27	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
34	33	gt0ne0d 11883	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35		tanval 16301	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	32, 34, 35	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
38	22, 20, 29, 34	recdivd 12113	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
39	37, 38	eqtr2d 2796	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
40	6, 22, 29	divcan4d 12102	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
41	39, 40	oveq12d 7438	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
42	31, 41	eqtrd 2795	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
43	42	oveq1d 7435	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
44	13	nnzd 12722	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45		demoivre 16373	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
46	32, 44, 45	syl2anc 596	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
47	46	oveq1d 7435	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
48	30, 43, 47	3eqtr3d 2803	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
49	13	nnred 12353	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
50	49, 18	remulcld 11342	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
51	50	recoscld 16317	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
52	51	recnd 11340	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
53	50	resincld 16316	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
54	53	recnd 11340	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55		mulcl 11287	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
56	5, 54, 55	sylancr 599	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
57	21, 28	elrpd 13164	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ⁺)
58	57, 44	rpexpcld 14394	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ⁺)
59	58	rpcnd 13169	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
60	58	rpne0d 13172	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
61	52, 56, 59, 60	divdird 12134	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
62	6, 54, 59, 60	divassd 12131	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
63	62	oveq2d 7436	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
64	48, 61, 63	3eqtrd 2799	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
65	16, 64	eqtr3d 2797	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
66	65	fveq2d 6889	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67		oveq2 7428	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68		oveq2 7428	. . . . . . . . 9 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
69	68	oveq2d 7436	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70		oveq2 7428	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
71	69, 70	oveq12d 7438	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
72	67, 71	oveq12d 7438	. . . . . 6 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
73	72	fveq2d 6889	. . . . 5 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74		fzfid 14119	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75		2nn0 12626	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
76		elfznn0 13757	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ₀)
77	76	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ₀)
78		nn0mulcl 12645	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
79	75, 77, 78	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ₀)
80	79	nn0red 12671	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
81	11	nnred 12353	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
82	81	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
83	49	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84		elfzle2 13664	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀)
85	84	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀)
86	77	nn0red 12671	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87		nnre 12345	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
88	87	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89		2re 12420	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90		2pos 12450	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
91	89, 90	pm3.2i 476	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ 0 < 2)
92	91	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93		lemul2 12173	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
94	86, 88, 92, 93	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
95	85, 94	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
96	82	lep1d 12251	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
97	96, 7	breqtrrdi 5146	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
98	80, 82, 83, 95, 97	letrd 11470	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99		nn0uz 13006	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
100	79, 99	eleqtrdi 2870	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ_≥‘0))
101	44	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102		elfz5 13651	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ (ℤ_≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103	100, 101, 102	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
104	98, 103	mpbird 260	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105		fznn0sub2 13772	. . . . . . . . 9 ⊢ ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106	104, 105	syl 18	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107	106	ex 418	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
108	13	nncnd 12354	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109	108	adantr 486	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110		2cn 12421	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
111		elfzelz 13659	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112	111	zcnd 12807	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113	112	ad2antrl 741	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114		mulcl 11287	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115	110, 113, 114	sylancr 599	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116	112	ssriv 3912	. . . . . . . . . . . 12 ⊢ (0...𝑀) ⊆ ℂ
117		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118	116, 117	sselid 3906	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119		mulcl 11287	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120	110, 118, 119	sylancr 599	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121	109, 115, 120	subcanad 11715	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122		2cnne0 12558	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124		mulcan 11956	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125	113, 118, 123, 124	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126	121, 125	bitrd 282	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127	126	ex 418	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128	107, 127	dom2lem 9022	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129		f1f1orn 6836	. . . . . 6 ⊢ ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
130	128, 129	syl 18	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1-onto→ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
131		oveq2 7428	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132	131	oveq2d 7436	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133		eqid 2760	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134		ovex 7453	. . . . . . 7 ⊢ (𝑁 − (2 · 𝑗)) ∈ V
135	132, 133, 134	fvmpt 6993	. . . . . 6 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136	135	adantl 487	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137	106	fmpttd 7115	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138	137	frnd 6718	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
139	138	sselda 3908	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
140		bccl2 14470	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
141	140	adantl 487	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
142	141	nncnd 12354	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
143	2	rprecred 13178	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
144		fznn0sub 13693	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈ ℕ₀)
145		reexpcl 14224	. . . . . . . . . . . 12 ⊢ (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁 − 𝑚) ∈ ℕ₀) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
146	143, 144, 145	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
147	146	recnd 11340	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ)
148		elfznn0 13757	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
149	148	adantl 487	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ₀)
150		expcl 14225	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ∧ 𝑚 ∈ ℕ₀) → (i↑𝑚) ∈ ℂ)
151	5, 149, 150	sylancr 599	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
152	147, 151	mulcld 11332	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ)
153	142, 152	mulcld 11332	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
154	139, 153	syldan 603	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
155	154	imcld 15367	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ)
156	155	recnd 11340	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ)
157	73, 74, 130, 136, 156	fsumf1o 15894	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
158		eldifi 4067	. . . . . . . 8 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
159	141	nnred 12353	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
160	158, 159	sylan2 605	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
161	158, 146	sylan2 605	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
162		eldif 4049	. . . . . . . . 9 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
163		elfzelz 13659	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
164	163	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
165		zeo 12788	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
166	164, 165	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167		i2 14349	. . . . . . . . . . . . . . . . . 18 ⊢ (i↑2) = -1
168	167	oveq1i 7430	. . . . . . . . . . . . . . . . 17 ⊢ ((i↑2)↑(𝑚 / 2)) = ( -1↑(𝑚 / 2))
169		simprr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
170	148	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
171		nn0re 12618	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℝ)
172		nn0ge0 12634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ 𝑚)
173		divge0 12189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
174	89, 90, 173	mpanr12 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
175	171, 172, 174	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ (𝑚 / 2))
176	170, 175	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
177		elnn0z 12709	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 / 2) ∈ ℕ₀ ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
178	169, 176, 177	sylanbrc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ₀)
179		expmul 14253	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ (𝑚 / 2) ∈ ℕ₀) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
180	5, 75, 178, 179	mp3an12i 1494	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
181	170	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
182		2ne0 12452	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≠ 0
183		divcan2 11985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
184	110, 182, 183	mp3an23 1482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
185	181, 184	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
186	185	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
187	180, 186	eqtr3d 2797	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
188	168, 187	eqtr3id 2809	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ( -1↑(𝑚 / 2)) = (i↑𝑚))
189		neg1rr 12309	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℝ
190		reexpcl 14224	. . . . . . . . . . . . . . . . 17 ⊢ (( -1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ₀) → ( -1↑(𝑚 / 2)) ∈ ℝ)
191	189, 178, 190	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ( -1↑(𝑚 / 2)) ∈ ℝ)
192	188, 191	eqeltrrd 2861	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
193	192	expr 462	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
194		0zd 12708	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
195		nnz 12717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
196	195	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
197	108	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
198	148	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
199	198	nn0cnd 12672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
200		1cnd 11305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
201	197, 199, 200	pnpcan2d 11710	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚))
202		2t1e2 12508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 · 1) = 2
203		df-2 12408	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 = (1 + 1)
204	202, 203	eqtr2i 2784	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 + 1) = (2 · 1)
205	204	oveq2i 7431	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
206	7	oveq1i 7430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
207	11	nncnd 12354	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
208	207	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
209	208, 200, 200	addassd 11334	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
210	206, 209	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
211		2cnd 12424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
212		nncn 12346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
213	212	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
214	211, 213, 200	adddid 11336	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
215	205, 210, 214	3eqtr4a 2821	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
216	215	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
217	201, 216	eqtr3d 2797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
218	217	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
219	196	peano2zd 12809	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
220	219	zcnd 12807	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
221		mulcl 11287	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
222	110, 220, 221	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
223		peano2cn 11485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℂ → (𝑚 + 1) ∈ ℂ)
224	199, 223	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑚 + 1) ∈ ℂ)
225	122	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℂ ∧ 2 ≠ 0))
226		divsubdir 12013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
227	222, 224, 225, 226	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 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 12101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
230	229	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
231	218, 227, 230	3eqtrd 2799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
232		simprr 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
233	219, 232	zsubcld 12811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
234	231, 233	eqeltrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ)
235	144	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℕ₀)
236		nn0re 12618	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → (𝑁 − 𝑚) ∈ ℝ)
237		nn0ge0 12634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ (𝑁 − 𝑚))
238		divge0 12189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 𝑚) / 2))
239	89, 90, 238	mpanr12 718	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2))
240	236, 237, 239	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ ((𝑁 − 𝑚) / 2))
241	235, 240	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁 − 𝑚) / 2))
242	235	nn0red 12671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ)
243	49	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
244		peano2re 11486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
245	243, 244	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) ∈ ℝ)
246	198, 172	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ 𝑚)
247	198	nn0red 12671	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
248	243, 247	subge02d 11911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁))
249	246, 248	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁)
250	243	ltp1d 12250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
251	242, 243, 245, 249, 250	lelttrd 11471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1))
252	251, 215	breqtrd 5130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1)))
253	219	zred 12806	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
254	91	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
255		ltdivmul 12195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
256	242, 253, 254, 255	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
257	252, 256	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1))
258		zleltp1 12750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
259	234, 196, 258	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
260	257, 259	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀)
261	194, 196, 234, 241, 260	elfzd 13650	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀))
262		oveq2 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2)))
263	262	oveq2d 7436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
264		ovex 7453	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V
265	263, 133, 264	fvmpt 6993	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 − 𝑚) / 2) ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
266	261, 265	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
267	235	nn0cnd 12672	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ)
268	267, 211, 228	divcan2d 12098	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚))
269	268	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚)))
270	197, 199	nncand 11677	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚)
271	266, 269, 270	3eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚)
272	137	ffnd 6710	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
273		fnfvelrn 7080	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
274	272, 261, 273	syl2an2r 698	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
275	271, 274	eqeltrrd 2861	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
276	275	expr 462	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
277	193, 276	orim12d 979	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))))
278	166, 277	mpd 16	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((i↑𝑚) ∈ ℝ ∨ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
279	278	orcomd 885	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
280	279	ord 878	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
281	280	impr 460	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
282	162, 281	sylan2b 606	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
283	161, 282	remulcld 11342	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ)
284	160, 283	remulcld 11342	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ)
285	284	reim0d 15397	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0)
286		fzfid 14119	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
287	138, 156, 285, 286	fsumss 15896	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
288		elfznn0 13757	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
289	288	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
290		nn0mulcl 12645	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ₀ ∧ 𝑗 ∈ ℕ₀) → (2 · 𝑗) ∈ ℕ₀)
291	75, 289, 290	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ₀)
292	291	nn0zd 12721	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
293		bccl 14469	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
294	14, 292, 293	syl2an2r 698	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
295	294	nn0red 12671	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
296		fznn0sub 13693	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈ ℕ₀)
297	296	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈ ℕ₀)
298		reexpcl 14224	. . . . . . . . . . . . . 14 ⊢ (( -1 ∈ ℝ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → ( -1↑(𝑀 − 𝑗)) ∈ ℝ)
299	189, 297, 298	sylancr 599	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ( -1↑(𝑀 − 𝑗)) ∈ ℝ)
300	295, 299	remulcld 11342	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) ∈ ℝ)
301		2z 12731	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
302		znegcl 12734	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
303	301, 302	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ -2 ∈ ℤ
304		rpexpcl 14226	. . . . . . . . . . . . . . 15 ⊢ (((tan‘𝐴) ∈ ℝ⁺ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑ -2) ∈ ℝ⁺)
305	2, 303, 304	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑ -2) ∈ ℝ⁺)
306	305	rpred 13167	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑ -2) ∈ ℝ)
307		reexpcl 14224	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴)↑ -2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → (((tan‘𝐴)↑ -2)↑𝑗) ∈ ℝ)
308	306, 288, 307	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑ -2)↑𝑗) ∈ ℝ)
309	300, 308	remulcld 11342	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ ℝ)
310	309	recnd 11340	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ ℂ)
311		mulcl 11287	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))) ∈ ℂ)
312	5, 310, 311	sylancr 599	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))) ∈ ℂ)
313	312	addlidd 11514	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))))
314	294	nn0cnd 12672	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
315	299	recnd 11340	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ( -1↑(𝑀 − 𝑗)) ∈ ℂ)
316	308	recnd 11340	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑ -2)↑𝑗) ∈ ℂ)
317	314, 315, 316	mulassd 11335	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗))))
318	317	oveq2d 7436	. . . . . . . . 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 11332	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ ℂ)
321	319, 314, 320	mul12d 11522	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗)))))
322	318, 321	eqtrd 2795	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗)))))
323		bccmpl 14456	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
324	14, 292, 323	syl2an2r 698	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
325	108	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
326	291	nn0cnd 12672	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
327	325, 326	nncand 11677	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
328	327	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
329	2	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ⁺)
330	329	rpcnd 13169	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
331		expneg 14215	. . . . . . . . . . . . . 14 ⊢ (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ₀) → ((tan‘𝐴)↑ -(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
332	330, 291, 331	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑ -(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
333	289	nn0cnd 12672	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
334		mulneg1 11755	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → ( -2 · 𝑗) = -(2 · 𝑗))
335	110, 333, 334	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ( -2 · 𝑗) = -(2 · 𝑗))
336	335	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑( -2 · 𝑗)) = ((tan‘𝐴)↑ -(2 · 𝑗)))
337	329	rpne0d 13172	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
338	330, 337, 292	exprecd 14300	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
339	332, 336, 338	3eqtr4d 2805	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑( -2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
340	303	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
341	289	nn0zd 12721	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
342		expmulz 14254	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ ( -2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑( -2 · 𝑗)) = (((tan‘𝐴)↑ -2)↑𝑗))
343	330, 337, 340, 341, 342	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑( -2 · 𝑗)) = (((tan‘𝐴)↑ -2)↑𝑗))
344	328, 339, 343	3eqtr2d 2801	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑ -2)↑𝑗))
345	7	oveq1i 7430	. . . . . . . . . . . . . . 15 ⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
346	11	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
347	346	nncnd 12354	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
348		1cnd 11305	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
349	347, 348, 326	addsubd 11693	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
350		2cnd 12424	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
351	212	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
352	350, 351, 333	subdid 11775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
353	352	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
354	349, 353	eqtr4d 2798	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
355	345, 354	eqtrid 2807	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
356	355	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀 − 𝑗)) + 1)))
357		nn0mulcl 12645	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ₀ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
358	75, 297, 357	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
359		expp1 14214	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ₀) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
360	5, 358, 359	sylancr 599	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
361	75	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ₀)
362	319, 297, 361	expmuld 14295	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗)))
363	167	oveq1i 7430	. . . . . . . . . . . . . . 15 ⊢ ((i↑2)↑(𝑀 − 𝑗)) = ( -1↑(𝑀 − 𝑗))
364	362, 363	eqtrdi 2811	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = ( -1↑(𝑀 − 𝑗)))
365	364	oveq1d 7435	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀 − 𝑗))) · i) = (( -1↑(𝑀 − 𝑗)) · i))
366	356, 360, 365	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (( -1↑(𝑀 − 𝑗)) · i))
367		mulcom 11289	. . . . . . . . . . . . 13 ⊢ ((( -1↑(𝑀 − 𝑗)) ∈ ℂ ∧ i ∈ ℂ) → (( -1↑(𝑀 − 𝑗)) · i) = (i · ( -1↑(𝑀 − 𝑗))))
368	315, 5, 367	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (( -1↑(𝑀 − 𝑗)) · i) = (i · ( -1↑(𝑀 − 𝑗))))
369	366, 368	eqtrd 2795	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · ( -1↑(𝑀 − 𝑗))))
370	344, 369	oveq12d 7438	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑ -2)↑𝑗) · (i · ( -1↑(𝑀 − 𝑗)))))
371		mulcl 11287	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ ( -1↑(𝑀 − 𝑗)) ∈ ℂ) → (i · ( -1↑(𝑀 − 𝑗))) ∈ ℂ)
372	5, 315, 371	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ( -1↑(𝑀 − 𝑗))) ∈ ℂ)
373	372, 316	mulcomd 11333	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) = ((((tan‘𝐴)↑ -2)↑𝑗) · (i · ( -1↑(𝑀 − 𝑗)))))
374	319, 315, 316	mulassd 11335	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) = (i · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗))))
375	370, 373, 374	3eqtr2rd 2802	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
376	324, 375	oveq12d 7438	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · (( -1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑ -2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
377	313, 322, 376	3eqtrd 2799	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
378	377	fveq2d 6889	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
379		0re 11313	. . . . . . 7 ⊢ 0 ∈ ℝ
380		crim 15287	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
381	379, 309, 380	sylancr 599	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
382	378, 381	eqtr3d 2797	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
383	382	sumeq2dv 15874	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
384	157, 287, 383	3eqtr3d 2803	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
385	286, 153	fsumim 15981	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
386	305	rpcnd 13169	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑ -2) ∈ ℂ)
387		oveq1 7427	. . . . . . 7 ⊢ (𝑡 = ((tan‘𝐴)↑ -2) → (𝑡↑𝑗) = (((tan‘𝐴)↑ -2)↑𝑗))
388	387	oveq2d 7436	. . . . . 6 ⊢ (𝑡 = ((tan‘𝐴)↑ -2) → (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
389	388	sumeq2sdv 15875	. . . . 5 ⊢ (𝑡 = ((tan‘𝐴)↑ -2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
390		basel.p	. . . . 5 ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))
391		sumex 15860	. . . . 5 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)) ∈ V
392	389, 390, 391	fvmpt 6993	. . . 4 ⊢ (((tan‘𝐴)↑ -2) ∈ ℂ → (𝑃‘((tan‘𝐴)↑ -2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
393	386, 392	syl 18	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑ -2)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑ -2)↑𝑗)))
394	384, 385, 393	3eqtr4d 2805	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑ -2)))
395	51, 58	rerpdivcld 13198	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
396	53, 58	rerpdivcld 13198	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
397	395, 396	crimd 15404	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
398	66, 394, 397	3eqtr3d 2803	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑ -2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∖ cdif 4045 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 Fn wfn 6533 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 ici 11205 + caddc 11206 · cmul 11208 < clt 11346 ≤ cle 11347 − cmin 11544 -cneg 11545 / cdiv 11976 ℕcn 12338 2c2 12400 ℕ₀cn0 12609 ℤcz 12696 ℤ_≥cuz 12968 ℝ⁺crp 13123 (,)cioo 13479 ...cfz 13642 ↑cexp 14207 Ccbc 14449 ℑcim 15270 Σcsu 15858 sincsin 16234 cosccos 16235 tanctan 16236 πcpi 16237

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281 ax-addf 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-map 8852 df-pm 8853 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9507 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-9 12415 df-n0 12610 df-z 12697 df-dec 12818 df-uz 12969 df-q 13079 df-rp 13124 df-xneg 13244 df-xadd 13245 df-xmul 13246 df-ioo 13483 df-ioc 13484 df-ico 13485 df-icc 13486 df-fz 13643 df-fzo 13792 df-fl 13935 df-seq 14148 df-exp 14208 df-fac 14421 df-bc 14450 df-hash 14478 df-shft 15225 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-limsup 15643 df-clim 15660 df-rlim 15661 df-sum 15859 df-ef 16238 df-sin 16240 df-cos 16241 df-tan 16242 df-pi 16243 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-starv 17448 df-sca 17449 df-vsca 17450 df-ip 17451 df-tset 17452 df-ple 17453 df-ds 17455 df-unif 17456 df-hom 17457 df-cco 17458 df-rest 17598 df-topn 17599 df-0g 17617 df-gsum 17618 df-topgen 17619 df-pt 17620 df-prds 17623 df-xrs 17679 df-qtop 17684 df-imas 17685 df-xps 17687 df-mre 17761 df-mrc 17762 df-acs 17764 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-submnd 18984 df-mulg 19283 df-cntz 19536 df-cmn 20001 df-psmet 21675 df-xmet 21676 df-met 21677 df-bl 21678 df-mopn 21679 df-fbas 21680 df-fg 21681 df-cnfld 21684 df-top 23217 df-topon 23234 df-topsp 23256 df-bases 23269 df-cld 23342 df-ntr 23343 df-cls 23344 df-nei 23421 df-lp 23459 df-perf 23460 df-cn 23550 df-cnp 23551 df-haus 23638 df-tx 23886 df-hmeo 24079 df-fil 24170 df-fm 24262 df-flim 24263 df-flf 24264 df-xms 24644 df-ms 24645 df-tms 24646 df-cncf 25204 df-limc 26191 df-dv 26192

This theorem is used by: basellem4 27416

W3C validator