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 26432

Description: Lemma for basel 26439. 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 25861	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ⁺)
2	1	adantl 482	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ⁺)
3	2	rpreccld 12967	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ⁺)
4	3	rpcnd 12959	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5		ax-icn 11110	. . . . . 6 ⊢ i ∈ ℂ
6	5	a1i 11	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7		basel.n	. . . . . . 7 ⊢ 𝑁 = ((2 · 𝑀) + 1)
8		2nn 12226	. . . . . . . . 9 ⊢ 2 ∈ ℕ
9		simpl 483	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10		nnmulcl 12177	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
11	8, 9, 10	sylancr 587	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
12	11	peano2nnd 12170	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
13	7, 12	eqeltrid 2842	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
14	13	nnnn0d 12473	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ₀)
15		binom 15715	. . . . 5 ⊢ (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
16	4, 6, 14, 15	syl3anc 1371	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
17		elioore 13294	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
18	17	adantl 482	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
19	18	recoscld 16026	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
20	19	recnd 11183	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
21	18	resincld 16025	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
22	21	recnd 11183	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23		mulcl 11135	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
24	5, 22, 23	sylancr 587	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
25	20, 24	addcld 11174	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26		sincosq1sgn 25855	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
27	26	adantl 482	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
28	27	simpld 495	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
29	28	gt0ne0d 11719	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
30	25, 22, 29, 14	expdivd 14065	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
31	20, 24, 22, 29	divdird 11969	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
32	18	recnd 11183	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
33	27	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
34	33	gt0ne0d 11719	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35		tanval 16010	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	32, 34, 35	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7373	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
38	22, 20, 29, 34	recdivd 11948	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
39	37, 38	eqtr2d 2777	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
40	6, 22, 29	divcan4d 11937	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
41	39, 40	oveq12d 7375	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
42	31, 41	eqtrd 2776	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
43	42	oveq1d 7372	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
44	13	nnzd 12526	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45		demoivre 16082	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
46	32, 44, 45	syl2anc 584	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
47	46	oveq1d 7372	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
48	30, 43, 47	3eqtr3d 2784	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
49	13	nnred 12168	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
50	49, 18	remulcld 11185	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
51	50	recoscld 16026	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
52	51	recnd 11183	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
53	50	resincld 16025	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
54	53	recnd 11183	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55		mulcl 11135	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
56	5, 54, 55	sylancr 587	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
57	21, 28	elrpd 12954	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ⁺)
58	57, 44	rpexpcld 14150	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ⁺)
59	58	rpcnd 12959	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
60	58	rpne0d 12962	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
61	52, 56, 59, 60	divdird 11969	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
62	6, 54, 59, 60	divassd 11966	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
63	62	oveq2d 7373	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
64	48, 61, 63	3eqtrd 2780	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
65	16, 64	eqtr3d 2778	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
66	65	fveq2d 6846	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67		oveq2 7365	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68		oveq2 7365	. . . . . . . . 9 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
69	68	oveq2d 7373	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70		oveq2 7365	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
71	69, 70	oveq12d 7375	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
72	67, 71	oveq12d 7375	. . . . . 6 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
73	72	fveq2d 6846	. . . . 5 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74		fzfid 13878	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75		2nn0 12430	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
76		elfznn0 13534	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ₀)
77	76	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ₀)
78		nn0mulcl 12449	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
79	75, 77, 78	sylancr 587	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ₀)
80	79	nn0red 12474	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
81	11	nnred 12168	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
82	81	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
83	49	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀)
85	84	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀)
86	77	nn0red 12474	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87		nnre 12160	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
88	87	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89		2re 12227	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90		2pos 12256	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
91	89, 90	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ 0 < 2)
92	91	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93		lemul2 12008	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
94	86, 88, 92, 93	syl3anc 1371	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
95	85, 94	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
96	82	lep1d 12086	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
97	96, 7	breqtrrdi 5147	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
98	80, 82, 83, 95, 97	letrd 11312	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99		nn0uz 12805	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
100	79, 99	eleqtrdi 2848	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ_≥‘0))
101	44	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102		elfz5 13433	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ (ℤ_≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103	100, 101, 102	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
104	98, 103	mpbird 256	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105		fznn0sub2 13548	. . . . . . . . 9 ⊢ ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106	104, 105	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107	106	ex 413	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
108	13	nncnd 12169	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109	108	adantr 481	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110		2cn 12228	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
111		elfzelz 13441	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112	111	zcnd 12608	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113	112	ad2antrl 726	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114		mulcl 11135	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115	110, 113, 114	sylancr 587	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116	112	ssriv 3948	. . . . . . . . . . . 12 ⊢ (0...𝑀) ⊆ ℂ
117		simprr 771	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118	116, 117	sselid 3942	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119		mulcl 11135	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120	110, 118, 119	sylancr 587	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121	109, 115, 120	subcanad 11555	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122		2cnne0 12363	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124		mulcan 11792	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125	113, 118, 123, 124	syl3anc 1371	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126	121, 125	bitrd 278	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127	126	ex 413	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128	107, 127	dom2lem 8932	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129		f1f1orn 6795	. . . . . 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 7365	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132	131	oveq2d 7373	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133		eqid 2736	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134		ovex 7390	. . . . . . 7 ⊢ (𝑁 − (2 · 𝑗)) ∈ V
135	132, 133, 134	fvmpt 6948	. . . . . 6 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136	135	adantl 482	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137	106	fmpttd 7063	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138	137	frnd 6676	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
139	138	sselda 3944	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
140		bccl2 14223	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
141	140	adantl 482	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
142	141	nncnd 12169	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
143	2	rprecred 12968	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
144		fznn0sub 13473	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈ ℕ₀)
145		reexpcl 13984	. . . . . . . . . . . 12 ⊢ (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁 − 𝑚) ∈ ℕ₀) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
146	143, 144, 145	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
147	146	recnd 11183	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ)
148		elfznn0 13534	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
149	148	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ₀)
150		expcl 13985	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ∧ 𝑚 ∈ ℕ₀) → (i↑𝑚) ∈ ℂ)
151	5, 149, 150	sylancr 587	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
152	147, 151	mulcld 11175	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ)
153	142, 152	mulcld 11175	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
154	139, 153	syldan 591	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
155	154	imcld 15080	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ)
156	155	recnd 11183	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ)
157	73, 74, 130, 136, 156	fsumf1o 15608	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
158		eldifi 4086	. . . . . . . 8 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
159	141	nnred 12168	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
160	158, 159	sylan2 593	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
161	158, 146	sylan2 593	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
162		eldif 3920	. . . . . . . . 9 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
163		elfzelz 13441	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
164	163	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
165		zeo 12589	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
166	164, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167		i2 14106	. . . . . . . . . . . . . . . . . 18 ⊢ (i↑2) = -1
168	167	oveq1i 7367	. . . . . . . . . . . . . . . . 17 ⊢ ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
169		simprr 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
170	148	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
171		nn0re 12422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℝ)
172		nn0ge0 12438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ 𝑚)
173		divge0 12024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
174	89, 90, 173	mpanr12 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
175	171, 172, 174	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ (𝑚 / 2))
176	170, 175	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
177		elnn0z 12512	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 / 2) ∈ ℕ₀ ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
178	169, 176, 177	sylanbrc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ₀)
179		expmul 14013	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ (𝑚 / 2) ∈ ℕ₀) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
180	5, 75, 178, 179	mp3an12i 1465	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
181	170	nn0cnd 12475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
182		2ne0 12257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≠ 0
183		divcan2 11821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
184	110, 182, 183	mp3an23 1453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
186	185	oveq2d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
187	180, 186	eqtr3d 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
188	168, 187	eqtr3id 2790	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
189		neg1rr 12268	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℝ
190		reexpcl 13984	. . . . . . . . . . . . . . . . 17 ⊢ ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ₀) → (-1↑(𝑚 / 2)) ∈ ℝ)
191	189, 178, 190	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
192	188, 191	eqeltrrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
193	192	expr 457	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
194		0zd 12511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
195		nnz 12520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
196	195	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
197	108	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
198	148	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
199	198	nn0cnd 12475	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
200		1cnd 11150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
201	197, 199, 200	pnpcan2d 11550	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚))
202		2t1e2 12316	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 · 1) = 2
203		df-2 12216	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 = (1 + 1)
204	202, 203	eqtr2i 2765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 + 1) = (2 · 1)
205	204	oveq2i 7368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
206	7	oveq1i 7367	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
207	11	nncnd 12169	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
208	207	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
209	208, 200, 200	addassd 11177	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
210	206, 209	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
211		2cnd 12231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
212		nncn 12161	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
213	212	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
214	211, 213, 200	adddid 11179	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
215	205, 210, 214	3eqtr4a 2802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
216	215	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
217	201, 216	eqtr3d 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
218	217	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
219	196	peano2zd 12610	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
220	219	zcnd 12608	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
221		mulcl 11135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
222	110, 220, 221	sylancr 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
223		peano2cn 11327	. . . . . . . . . . . . . . . . . . . . . . 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 11849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
227	222, 224, 225, 226	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 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 11936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
230	229	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
231	218, 227, 230	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
232		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
233	219, 232	zsubcld 12612	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
234	231, 233	eqeltrd 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ)
235	144	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℕ₀)
236		nn0re 12422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → (𝑁 − 𝑚) ∈ ℝ)
237		nn0ge0 12438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ (𝑁 − 𝑚))
238		divge0 12024	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 𝑚) / 2))
239	89, 90, 238	mpanr12 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2))
240	236, 237, 239	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ ((𝑁 − 𝑚) / 2))
241	235, 240	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁 − 𝑚) / 2))
242	235	nn0red 12474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ)
243	49	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
244		peano2re 11328	. . . . . . . . . . . . . . . . . . . . . . . 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 12474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
248	243, 247	subge02d 11747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁))
249	246, 248	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁)
250	243	ltp1d 12085	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
251	242, 243, 245, 249, 250	lelttrd 11313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1))
252	251, 215	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1)))
253	219	zred 12607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
254	91	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
255		ltdivmul 12030	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
256	242, 253, 254, 255	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
257	252, 256	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) < (𝑀 + 1))
258		zleltp1 12554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
259	234, 196, 258	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
260	257, 259	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ≤ 𝑀)
261	194, 196, 234, 241, 260	elfzd 13432	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀))
262		oveq2 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2)))
263	262	oveq2d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
264		ovex 7390	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V
265	263, 133, 264	fvmpt 6948	. . . . . . . . . . . . . . . . . 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 12475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ)
268	267, 211, 228	divcan2d 11933	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚))
269	268	oveq2d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚)))
270	197, 199	nncand 11517	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚)
271	266, 269, 270	3eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚)
272	137	ffnd 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
273		fnfvelrn 7031	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
274	272, 261, 273	syl2an2r 683	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
275	271, 274	eqeltrrd 2839	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
276	275	expr 457	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
277	193, 276	orim12d 963	. . . . . . . . . . . . 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 869	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
280	279	ord 862	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
281	280	impr 455	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
282	162, 281	sylan2b 594	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
283	161, 282	remulcld 11185	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ)
284	160, 283	remulcld 11185	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ)
285	284	reim0d 15110	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0)
286		fzfid 13878	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
287	138, 156, 285, 286	fsumss 15610	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
288		elfznn0 13534	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
289	288	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
290		nn0mulcl 12449	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ₀ ∧ 𝑗 ∈ ℕ₀) → (2 · 𝑗) ∈ ℕ₀)
291	75, 289, 290	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ₀)
292	291	nn0zd 12525	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
293		bccl 14222	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
294	14, 292, 293	syl2an2r 683	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
295	294	nn0red 12474	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
296		fznn0sub 13473	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈ ℕ₀)
297	296	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈ ℕ₀)
298		reexpcl 13984	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
299	189, 297, 298	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
300	295, 299	remulcld 11185	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ)
301		2z 12535	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
302		znegcl 12538	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
303	301, 302	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ -2 ∈ ℤ
304		rpexpcl 13986	. . . . . . . . . . . . . . 15 ⊢ (((tan‘𝐴) ∈ ℝ⁺ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
305	2, 303, 304	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
306	305	rpred 12957	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
307		reexpcl 13984	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
308	306, 288, 307	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
309	300, 308	remulcld 11185	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
310	309	recnd 11183	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
311		mulcl 11135	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
312	5, 310, 311	sylancr 587	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
313	312	addid2d 11356	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
314	294	nn0cnd 12475	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
315	299	recnd 11183	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ)
316	308	recnd 11183	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
317	314, 315, 316	mulassd 11178	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
318	317	oveq2d 7373	. . . . . . . . 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 11175	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
321	319, 314, 320	mul12d 11364	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
322	318, 321	eqtrd 2776	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
323		bccmpl 14209	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
324	14, 292, 323	syl2an2r 683	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
325	108	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
326	291	nn0cnd 12475	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
327	325, 326	nncand 11517	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
328	327	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
329	2	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ⁺)
330	329	rpcnd 12959	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
331		expneg 13975	. . . . . . . . . . . . . 14 ⊢ (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ₀) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
332	330, 291, 331	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
333	289	nn0cnd 12475	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
334		mulneg1 11591	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
335	110, 333, 334	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
336	335	oveq2d 7373	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
337	329	rpne0d 12962	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
338	330, 337, 292	exprecd 14059	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
339	332, 336, 338	3eqtr4d 2786	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
340	303	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
341	289	nn0zd 12525	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
342		expmulz 14014	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
343	330, 337, 340, 341, 342	syl22anc 837	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
344	328, 339, 343	3eqtr2d 2782	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
345	7	oveq1i 7367	. . . . . . . . . . . . . . 15 ⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
346	11	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
347	346	nncnd 12169	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
348		1cnd 11150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
349	347, 348, 326	addsubd 11533	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
350		2cnd 12231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
351	212	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
352	350, 351, 333	subdid 11611	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
353	352	oveq1d 7372	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
354	349, 353	eqtr4d 2779	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
355	345, 354	eqtrid 2788	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
356	355	oveq2d 7373	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀 − 𝑗)) + 1)))
357		nn0mulcl 12449	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ₀ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
358	75, 297, 357	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
359		expp1 13974	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ₀) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
360	5, 358, 359	sylancr 587	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
361	75	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ₀)
362	319, 297, 361	expmuld 14054	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗)))
363	167	oveq1i 7367	. . . . . . . . . . . . . . 15 ⊢ ((i↑2)↑(𝑀 − 𝑗)) = (-1↑(𝑀 − 𝑗))
364	362, 363	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗)))
365	364	oveq1d 7372	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀 − 𝑗))) · i) = ((-1↑(𝑀 − 𝑗)) · i))
366	356, 360, 365	3eqtrd 2780	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i))
367		mulcom 11137	. . . . . . . . . . . . 13 ⊢ (((-1↑(𝑀 − 𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
368	315, 5, 367	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
369	366, 368	eqtrd 2776	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀 − 𝑗))))
370	344, 369	oveq12d 7375	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
371		mulcl 11135	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
372	5, 315, 371	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
373	372, 316	mulcomd 11176	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
374	319, 315, 316	mulassd 11178	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
375	370, 373, 374	3eqtr2rd 2783	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
376	324, 375	oveq12d 7375	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
377	313, 322, 376	3eqtrd 2780	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
378	377	fveq2d 6846	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
379		0re 11157	. . . . . . 7 ⊢ 0 ∈ ℝ
380		crim 15000	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
381	379, 309, 380	sylancr 587	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
382	378, 381	eqtr3d 2778	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
383	382	sumeq2dv 15588	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
384	157, 287, 383	3eqtr3d 2784	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
385	286, 153	fsumim 15694	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
386	305	rpcnd 12959	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
387		oveq1 7364	. . . . . . 7 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
388	387	oveq2d 7373	. . . . . 6 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389	388	sumeq2sdv 15589	. . . . 5 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390		basel.p	. . . . 5 ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))
391		sumex 15572	. . . . 5 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
392	389, 390, 391	fvmpt 6948	. . . 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 2786	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
395	51, 58	rerpdivcld 12988	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
396	53, 58	rerpdivcld 12988	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
397	395, 396	crimd 15117	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
398	66, 394, 397	3eqtr3d 2784	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∖ cdif 3907 class class class wbr 5105 ↦ cmpt 5188 ran crn 5634 Fn wfn 6491 –1-1→wf1 6493 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 ici 11053 + caddc 11054 · cmul 11056 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 / cdiv 11812 ℕcn 12153 2c2 12208 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 (,)cioo 13264 ...cfz 13424 ↑cexp 13967 Ccbc 14202 ℑcim 14983 Σcsu 15570 sincsin 15946 cosccos 15947 tanctan 15948 πcpi 15949

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-addf 11130 ax-mulf 11131

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-supp 8093 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9306 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-5 12219 df-6 12220 df-7 12221 df-8 12222 df-9 12223 df-n0 12414 df-z 12500 df-dec 12619 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ioc 13269 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-seq 13907 df-exp 13968 df-fac 14174 df-bc 14203 df-hash 14231 df-shft 14952 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-limsup 15353 df-clim 15370 df-rlim 15371 df-sum 15571 df-ef 15950 df-sin 15952 df-cos 15953 df-tan 15954 df-pi 15955 df-struct 17019 df-sets 17036 df-slot 17054 df-ndx 17066 df-base 17084 df-ress 17113 df-plusg 17146 df-mulr 17147 df-starv 17148 df-sca 17149 df-vsca 17150 df-ip 17151 df-tset 17152 df-ple 17153 df-ds 17155 df-unif 17156 df-hom 17157 df-cco 17158 df-rest 17304 df-topn 17305 df-0g 17323 df-gsum 17324 df-topgen 17325 df-pt 17326 df-prds 17329 df-xrs 17384 df-qtop 17389 df-imas 17390 df-xps 17392 df-mre 17466 df-mrc 17467 df-acs 17469 df-mgm 18497 df-sgrp 18546 df-mnd 18557 df-submnd 18602 df-mulg 18873 df-cntz 19097 df-cmn 19564 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-fbas 20793 df-fg 20794 df-cnfld 20797 df-top 22243 df-topon 22260 df-topsp 22282 df-bases 22296 df-cld 22370 df-ntr 22371 df-cls 22372 df-nei 22449 df-lp 22487 df-perf 22488 df-cn 22578 df-cnp 22579 df-haus 22666 df-tx 22913 df-hmeo 23106 df-fil 23197 df-fm 23289 df-flim 23290 df-flf 23291 df-xms 23673 df-ms 23674 df-tms 23675 df-cncf 24241 df-limc 25230 df-dv 25231

This theorem is referenced by: basellem4 26433

W3C validator