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 26137

Description: Lemma for basel 26144. 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 25566	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (tan‘𝐴) ∈ ℝ⁺)
2	1	adantl 481	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) ∈ ℝ⁺)
3	2	rpreccld 12711	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ⁺)
4	3	rpcnd 12703	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℂ)
5		ax-icn 10861	. . . . . 6 ⊢ i ∈ ℂ
6	5	a1i 11	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → i ∈ ℂ)
7		basel.n	. . . . . . 7 ⊢ 𝑁 = ((2 · 𝑀) + 1)
8		2nn 11976	. . . . . . . . 9 ⊢ 2 ∈ ℕ
9		simpl 482	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑀 ∈ ℕ)
10		nnmulcl 11927	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
11	8, 9, 10	sylancr 586	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℕ)
12	11	peano2nnd 11920	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((2 · 𝑀) + 1) ∈ ℕ)
13	7, 12	eqeltrid 2843	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ)
14	13	nnnn0d 12223	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℕ₀)
15		binom 15470	. . . . 5 ⊢ (((1 / (tan‘𝐴)) ∈ ℂ ∧ i ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
16	4, 6, 14, 15	syl3anc 1369	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))))
17		elioore 13038	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (0(,)(π / 2)) → 𝐴 ∈ ℝ)
18	17	adantl 481	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℝ)
19	18	recoscld 15781	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℝ)
20	19	recnd 10934	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ∈ ℂ)
21	18	resincld 15780	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ)
22	21	recnd 10934	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℂ)
23		mulcl 10886	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ (sin‘𝐴) ∈ ℂ) → (i · (sin‘𝐴)) ∈ ℂ)
24	5, 22, 23	sylancr 586	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘𝐴)) ∈ ℂ)
25	20, 24	addcld 10925	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) + (i · (sin‘𝐴))) ∈ ℂ)
26		sincosq1sgn 25560	. . . . . . . . . 10 ⊢ (𝐴 ∈ (0(,)(π / 2)) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
27	26	adantl 481	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0 < (sin‘𝐴) ∧ 0 < (cos‘𝐴)))
28	27	simpld 494	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (sin‘𝐴))
29	28	gt0ne0d 11469	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ≠ 0)
30	25, 22, 29, 14	expdivd 13806	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)))
31	20, 24, 22, 29	divdird 11719	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))))
32	18	recnd 10934	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝐴 ∈ ℂ)
33	27	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 0 < (cos‘𝐴))
34	33	gt0ne0d 11469	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘𝐴) ≠ 0)
35		tanval 15765	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
36	32, 34, 35	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (tan‘𝐴) = ((sin‘𝐴) / (cos‘𝐴)))
37	36	oveq2d 7271	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) = (1 / ((sin‘𝐴) / (cos‘𝐴))))
38	22, 20, 29, 34	recdivd 11698	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / ((sin‘𝐴) / (cos‘𝐴))) = ((cos‘𝐴) / (sin‘𝐴)))
39	37, 38	eqtr2d 2779	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘𝐴) / (sin‘𝐴)) = (1 / (tan‘𝐴)))
40	6, 22, 29	divcan4d 11687	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘𝐴)) / (sin‘𝐴)) = i)
41	39, 40	oveq12d 7273	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) / (sin‘𝐴)) + ((i · (sin‘𝐴)) / (sin‘𝐴))) = ((1 / (tan‘𝐴)) + i))
42	31, 41	eqtrd 2778	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴)) = ((1 / (tan‘𝐴)) + i))
43	42	oveq1d 7270	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴))) / (sin‘𝐴))↑𝑁) = (((1 / (tan‘𝐴)) + i)↑𝑁))
44	13	nnzd 12354	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℤ)
45		demoivre 15837	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
46	32, 44, 45	syl2anc 583	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
47	46	oveq1d 7270	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
48	30, 43, 47	3eqtr3d 2786	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)))
49	13	nnred 11918	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℝ)
50	49, 18	remulcld 10936	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑁 · 𝐴) ∈ ℝ)
51	50	recoscld 15781	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℝ)
52	51	recnd 10934	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (cos‘(𝑁 · 𝐴)) ∈ ℂ)
53	50	resincld 15780	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℝ)
54	53	recnd 10934	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘(𝑁 · 𝐴)) ∈ ℂ)
55		mulcl 10886	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (sin‘(𝑁 · 𝐴)) ∈ ℂ) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
56	5, 54, 55	sylancr 586	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (i · (sin‘(𝑁 · 𝐴))) ∈ ℂ)
57	21, 28	elrpd 12698	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (sin‘𝐴) ∈ ℝ⁺)
58	57, 44	rpexpcld 13890	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℝ⁺)
59	58	rpcnd 12703	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ∈ ℂ)
60	58	rpne0d 12706	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘𝐴)↑𝑁) ≠ 0)
61	52, 56, 59, 60	divdird 11719	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))) / ((sin‘𝐴)↑𝑁)) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))))
62	6, 54, 59, 60	divassd 11716	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁)) = (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))
63	62	oveq2d 7271	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + ((i · (sin‘(𝑁 · 𝐴))) / ((sin‘𝐴)↑𝑁))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
64	48, 61, 63	3eqtrd 2782	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (((1 / (tan‘𝐴)) + i)↑𝑁) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
65	16, 64	eqtr3d 2780	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = (((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))))
66	65	fveq2d 6760	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))))
67		oveq2 7263	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁C𝑚) = (𝑁C(𝑁 − (2 · 𝑗))))
68		oveq2 7263	. . . . . . . . 9 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (𝑁 − 𝑚) = (𝑁 − (𝑁 − (2 · 𝑗))))
69	68	oveq2d 7271	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) = ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))))
70		oveq2 7263	. . . . . . . 8 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (i↑𝑚) = (i↑(𝑁 − (2 · 𝑗))))
71	69, 70	oveq12d 7273	. . . . . . 7 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
72	67, 71	oveq12d 7273	. . . . . 6 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
73	72	fveq2d 6760	. . . . 5 ⊢ (𝑚 = (𝑁 − (2 · 𝑗)) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
74		fzfid 13621	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑀) ∈ Fin)
75		2nn0 12180	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
76		elfznn0 13278	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ₀)
77	76	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ₀)
78		nn0mulcl 12199	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ₀ ∧ 𝑘 ∈ ℕ₀) → (2 · 𝑘) ∈ ℕ₀)
79	75, 77, 78	sylancr 586	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℕ₀)
80	79	nn0red 12224	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ ℝ)
81	11	nnred 11918	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℝ)
82	81	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℝ)
83	49	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℝ)
84		elfzle2 13189	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ≤ 𝑀)
85	84	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ≤ 𝑀)
86	77	nn0red 12224	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℝ)
87		nnre 11910	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℝ)
88	87	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
89		2re 11977	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
90		2pos 12006	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
91	89, 90	pm3.2i 470	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ 0 < 2)
92	91	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 ∈ ℝ ∧ 0 < 2))
93		lemul2 11758	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
94	86, 88, 92, 93	syl3anc 1369	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑘 ≤ 𝑀 ↔ (2 · 𝑘) ≤ (2 · 𝑀)))
95	85, 94	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ (2 · 𝑀))
96	82	lep1d 11836	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
97	96, 7	breqtrrdi 5112	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑀) ≤ 𝑁)
98	80, 82, 83, 95, 97	letrd 11062	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ≤ 𝑁)
99		nn0uz 12549	. . . . . . . . . . . 12 ⊢ ℕ₀ = (ℤ_≥‘0)
100	79, 99	eleqtrdi 2849	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (ℤ_≥‘0))
101	44	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
102		elfz5 13177	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ (ℤ_≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
103	100, 101, 102	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → ((2 · 𝑘) ∈ (0...𝑁) ↔ (2 · 𝑘) ≤ 𝑁))
104	98, 103	mpbird 256	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (2 · 𝑘) ∈ (0...𝑁))
105		fznn0sub2 13292	. . . . . . . . 9 ⊢ ((2 · 𝑘) ∈ (0...𝑁) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
106	104, 105	syl 17	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑘 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁))
107	106	ex 412	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) → (𝑁 − (2 · 𝑘)) ∈ (0...𝑁)))
108	13	nncnd 11919	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → 𝑁 ∈ ℂ)
109	108	adantr 480	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑁 ∈ ℂ)
110		2cn 11978	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
111		elfzelz 13185	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
112	111	zcnd 12356	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
113	112	ad2antrl 724	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑘 ∈ ℂ)
114		mulcl 10886	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
115	110, 113, 114	sylancr 586	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑘) ∈ ℂ)
116	112	ssriv 3921	. . . . . . . . . . . 12 ⊢ (0...𝑀) ⊆ ℂ
117		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ (0...𝑀))
118	116, 117	sselid 3915	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → 𝑚 ∈ ℂ)
119		mulcl 10886	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (2 · 𝑚) ∈ ℂ)
120	110, 118, 119	sylancr 586	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 · 𝑚) ∈ ℂ)
121	109, 115, 120	subcanad 11305	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ (2 · 𝑘) = (2 · 𝑚)))
122		2cnne0 12113	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → (2 ∈ ℂ ∧ 2 ≠ 0))
124		mulcan 11542	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
125	113, 118, 123, 124	syl3anc 1369	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((2 · 𝑘) = (2 · 𝑚) ↔ 𝑘 = 𝑚))
126	121, 125	bitrd 278	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀))) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚))
127	126	ex 412	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((𝑘 ∈ (0...𝑀) ∧ 𝑚 ∈ (0...𝑀)) → ((𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑚)) ↔ 𝑘 = 𝑚)))
128	107, 127	dom2lem 8735	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)–1-1→(0...𝑁))
129		f1f1orn 6711	. . . . . 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 7263	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (2 · 𝑘) = (2 · 𝑗))
132	131	oveq2d 7271	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · 𝑗)))
133		eqid 2738	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) = (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))
134		ovex 7288	. . . . . . 7 ⊢ (𝑁 − (2 · 𝑗)) ∈ V
135	132, 133, 134	fvmpt 6857	. . . . . 6 ⊢ (𝑗 ∈ (0...𝑀) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
136	135	adantl 481	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘𝑗) = (𝑁 − (2 · 𝑗)))
137	106	fmpttd 6971	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))):(0...𝑀)⟶(0...𝑁))
138	137	frnd 6592	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ⊆ (0...𝑁))
139	138	sselda 3917	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
140		bccl2 13965	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ)
141	140	adantl 481	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ)
142	141	nncnd 11919	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ)
143	2	rprecred 12712	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (1 / (tan‘𝐴)) ∈ ℝ)
144		fznn0sub 13217	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → (𝑁 − 𝑚) ∈ ℕ₀)
145		reexpcl 13727	. . . . . . . . . . . 12 ⊢ (((1 / (tan‘𝐴)) ∈ ℝ ∧ (𝑁 − 𝑚) ∈ ℕ₀) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
146	143, 144, 145	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
147	146	recnd 10934	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℂ)
148		elfznn0 13278	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
149	148	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℕ₀)
150		expcl 13728	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ∧ 𝑚 ∈ ℕ₀) → (i↑𝑚) ∈ ℂ)
151	5, 149, 150	sylancr 586	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (i↑𝑚) ∈ ℂ)
152	147, 151	mulcld 10926	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℂ)
153	142, 152	mulcld 10926	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
154	139, 153	syldan 590	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℂ)
155	154	imcld 14834	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℝ)
156	155	recnd 10934	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) ∈ ℂ)
157	73, 74, 130, 136, 156	fsumf1o 15363	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
158		eldifi 4057	. . . . . . . 8 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) → 𝑚 ∈ (0...𝑁))
159	141	nnred 11918	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℝ)
160	158, 159	sylan2 592	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (𝑁C𝑚) ∈ ℝ)
161	158, 146	sylan2 592	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) ∈ ℝ)
162		eldif 3893	. . . . . . . . 9 ⊢ (𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))) ↔ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
163		elfzelz 13185	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
164	163	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → 𝑚 ∈ ℤ)
165		zeo 12336	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℤ → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
166	164, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ ∨ ((𝑚 + 1) / 2) ∈ ℤ))
167		i2 13847	. . . . . . . . . . . . . . . . . 18 ⊢ (i↑2) = -1
168	167	oveq1i 7265	. . . . . . . . . . . . . . . . 17 ⊢ ((i↑2)↑(𝑚 / 2)) = (-1↑(𝑚 / 2))
169		simprr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℤ)
170	148	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
171		nn0re 12172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℝ)
172		nn0ge0 12188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ 𝑚)
173		divge0 11774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (𝑚 / 2))
174	89, 90, 173	mpanr12 701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) → 0 ≤ (𝑚 / 2))
175	171, 172, 174	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → 0 ≤ (𝑚 / 2))
176	170, 175	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 0 ≤ (𝑚 / 2))
177		elnn0z 12262	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 / 2) ∈ ℕ₀ ↔ ((𝑚 / 2) ∈ ℤ ∧ 0 ≤ (𝑚 / 2)))
178	169, 176, 177	sylanbrc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (𝑚 / 2) ∈ ℕ₀)
179		expmul 13756	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ (𝑚 / 2) ∈ ℕ₀) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
180	5, 75, 178, 179	mp3an12i 1463	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = ((i↑2)↑(𝑚 / 2)))
181	170	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
182		2ne0 12007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ≠ 0
183		divcan2 11571	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · (𝑚 / 2)) = 𝑚)
184	110, 182, 183	mp3an23 1451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 ∈ ℂ → (2 · (𝑚 / 2)) = 𝑚)
185	181, 184	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (2 · (𝑚 / 2)) = 𝑚)
186	185	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑(2 · (𝑚 / 2))) = (i↑𝑚))
187	180, 186	eqtr3d 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → ((i↑2)↑(𝑚 / 2)) = (i↑𝑚))
188	168, 187	eqtr3id 2793	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) = (i↑𝑚))
189		neg1rr 12018	. . . . . . . . . . . . . . . . 17 ⊢ -1 ∈ ℝ
190		reexpcl 13727	. . . . . . . . . . . . . . . . 17 ⊢ ((-1 ∈ ℝ ∧ (𝑚 / 2) ∈ ℕ₀) → (-1↑(𝑚 / 2)) ∈ ℝ)
191	189, 178, 190	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (-1↑(𝑚 / 2)) ∈ ℝ)
192	188, 191	eqeltrrd 2840	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ (𝑚 / 2) ∈ ℤ)) → (i↑𝑚) ∈ ℝ)
193	192	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 / 2) ∈ ℤ → (i↑𝑚) ∈ ℝ))
194		0zd 12261	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ∈ ℤ)
195		nnz 12272	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
196	195	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℤ)
197	108	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℂ)
198	148	ad2antrl 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℕ₀)
199	198	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℂ)
200		1cnd 10901	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 1 ∈ ℂ)
201	197, 199, 200	pnpcan2d 11300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = (𝑁 − 𝑚))
202		2t1e2 12066	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 · 1) = 2
203		df-2 11966	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 = (1 + 1)
204	202, 203	eqtr2i 2767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1 + 1) = (2 · 1)
205	204	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 · 𝑀) + (1 + 1)) = ((2 · 𝑀) + (2 · 1))
206	7	oveq1i 7265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
207	11	nncnd 11919	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (2 · 𝑀) ∈ ℂ)
208	207	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · 𝑀) ∈ ℂ)
209	208, 200, 200	addassd 10928	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
210	206, 209	syl5eq 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = ((2 · 𝑀) + (1 + 1)))
211		2cnd 11981	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 2 ∈ ℂ)
212		nncn 11911	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
213	212	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑀 ∈ ℂ)
214	211, 213, 200	adddid 10930	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) = ((2 · 𝑀) + (2 · 1)))
215	205, 210, 214	3eqtr4a 2805	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 + 1) = (2 · (𝑀 + 1)))
216	215	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 + 1) − (𝑚 + 1)) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
217	201, 216	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) = ((2 · (𝑀 + 1)) − (𝑚 + 1)))
218	217	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2))
219	196	peano2zd 12358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℤ)
220	219	zcnd 12356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℂ)
221		mulcl 10886	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∈ ℂ ∧ (𝑀 + 1) ∈ ℂ) → (2 · (𝑀 + 1)) ∈ ℂ)
222	110, 220, 221	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · (𝑀 + 1)) ∈ ℂ)
223		peano2cn 11077	. . . . . . . . . . . . . . . . . . . . . . 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 11599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · (𝑀 + 1)) ∈ ℂ ∧ (𝑚 + 1) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · (𝑀 + 1)) − (𝑚 + 1)) / 2) = (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)))
227	222, 224, 225, 226	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . 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 11686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((2 · (𝑀 + 1)) / 2) = (𝑀 + 1))
230	229	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (((2 · (𝑀 + 1)) / 2) − ((𝑚 + 1) / 2)) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
231	218, 227, 230	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) = ((𝑀 + 1) − ((𝑚 + 1) / 2)))
232		simprr 769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑚 + 1) / 2) ∈ ℤ)
233	219, 232	zsubcld 12360	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑀 + 1) − ((𝑚 + 1) / 2)) ∈ ℤ)
234	231, 233	eqeltrd 2839	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ ℤ)
235	144	ad2antrl 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℕ₀)
236		nn0re 12172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → (𝑁 − 𝑚) ∈ ℝ)
237		nn0ge0 12188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ (𝑁 − 𝑚))
238		divge0 11774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ ((𝑁 − 𝑚) / 2))
239	89, 90, 238	mpanr12 701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ 0 ≤ (𝑁 − 𝑚)) → 0 ≤ ((𝑁 − 𝑚) / 2))
240	236, 237, 239	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 − 𝑚) ∈ ℕ₀ → 0 ≤ ((𝑁 − 𝑚) / 2))
241	235, 240	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 0 ≤ ((𝑁 − 𝑚) / 2))
242	235	nn0red 12224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℝ)
243	49	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 ∈ ℝ)
244		peano2re 11078	. . . . . . . . . . . . . . . . . . . . . . . 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 12224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ℝ)
248	243, 247	subge02d 11497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (0 ≤ 𝑚 ↔ (𝑁 − 𝑚) ≤ 𝑁))
249	246, 248	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ≤ 𝑁)
250	243	ltp1d 11835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑁 < (𝑁 + 1))
251	242, 243, 245, 249, 250	lelttrd 11063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (𝑁 + 1))
252	251, 215	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) < (2 · (𝑀 + 1)))
253	219	zred 12355	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑀 + 1) ∈ ℝ)
254	91	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 ∈ ℝ ∧ 0 < 2))
255		ltdivmul 11780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 − 𝑚) ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((𝑁 − 𝑚) / 2) < (𝑀 + 1) ↔ (𝑁 − 𝑚) < (2 · (𝑀 + 1))))
256	242, 253, 254, 255	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . 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 12301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 − 𝑚) / 2) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝑁 − 𝑚) / 2) ≤ 𝑀 ↔ ((𝑁 − 𝑚) / 2) < (𝑀 + 1)))
259	234, 196, 258	syl2anc 583	. . . . . . . . . . . . . . . . . . . 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 13176	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑁 − 𝑚) / 2) ∈ (0...𝑀))
262		oveq2 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (2 · 𝑘) = (2 · ((𝑁 − 𝑚) / 2)))
263	262	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = ((𝑁 − 𝑚) / 2) → (𝑁 − (2 · 𝑘)) = (𝑁 − (2 · ((𝑁 − 𝑚) / 2))))
264		ovex 7288	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) ∈ V
265	263, 133, 264	fvmpt 6857	. . . . . . . . . . . . . . . . . 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 12225	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − 𝑚) ∈ ℂ)
268	267, 211, 228	divcan2d 11683	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (2 · ((𝑁 − 𝑚) / 2)) = (𝑁 − 𝑚))
269	268	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (2 · ((𝑁 − 𝑚) / 2))) = (𝑁 − (𝑁 − 𝑚)))
270	197, 199	nncand 11267	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → (𝑁 − (𝑁 − 𝑚)) = 𝑚)
271	266, 269, 270	3eqtrd 2782	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) = 𝑚)
272	137	ffnd 6585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀))
273		fnfvelrn 6940	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) Fn (0...𝑀) ∧ ((𝑁 − 𝑚) / 2) ∈ (0...𝑀)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
274	272, 261, 273	syl2an2r 681	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → ((𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))‘((𝑁 − 𝑚) / 2)) ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
275	271, 274	eqeltrrd 2840	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ((𝑚 + 1) / 2) ∈ ℤ)) → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))
276	275	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (((𝑚 + 1) / 2) ∈ ℤ → 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))))
277	193, 276	orim12d 961	. . . . . . . . . . . . 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 867	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) ∨ (i↑𝑚) ∈ ℝ))
280	279	ord 860	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))) → (i↑𝑚) ∈ ℝ))
281	280	impr 454	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ (𝑚 ∈ (0...𝑁) ∧ ¬ 𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
282	162, 281	sylan2b 593	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (i↑𝑚) ∈ ℝ)
283	161, 282	remulcld 10936	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)) ∈ ℝ)
284	160, 283	remulcld 10936	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → ((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚))) ∈ ℝ)
285	284	reim0d 14864	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑚 ∈ ((0...𝑁) ∖ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘))))) → (ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = 0)
286		fzfid 13621	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (0...𝑁) ∈ Fin)
287	138, 156, 285, 286	fsumss 15365	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ ran (𝑘 ∈ (0...𝑀) ↦ (𝑁 − (2 · 𝑘)))(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
288		elfznn0 13278	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
289	288	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
290		nn0mulcl 12199	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ₀ ∧ 𝑗 ∈ ℕ₀) → (2 · 𝑗) ∈ ℕ₀)
291	75, 289, 290	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℕ₀)
292	291	nn0zd 12353	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℤ)
293		bccl 13964	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
294	14, 292, 293	syl2an2r 681	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℕ₀)
295	294	nn0red 12224	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℝ)
296		fznn0sub 13217	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → (𝑀 − 𝑗) ∈ ℕ₀)
297	296	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 − 𝑗) ∈ ℕ₀)
298		reexpcl 13727	. . . . . . . . . . . . . 14 ⊢ ((-1 ∈ ℝ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
299	189, 297, 298	sylancr 586	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℝ)
300	295, 299	remulcld 10936	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) ∈ ℝ)
301		2z 12282	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
302		znegcl 12285	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
303	301, 302	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ -2 ∈ ℤ
304		rpexpcl 13729	. . . . . . . . . . . . . . 15 ⊢ (((tan‘𝐴) ∈ ℝ⁺ ∧ -2 ∈ ℤ) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
305	2, 303, 304	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ⁺)
306	305	rpred 12701	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℝ)
307		reexpcl 13727	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴)↑-2) ∈ ℝ ∧ 𝑗 ∈ ℕ₀) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
308	306, 288, 307	syl2an 595	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℝ)
309	300, 308	remulcld 10936	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ)
310	309	recnd 10934	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
311		mulcl 10886	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
312	5, 310, 311	sylancr 586	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) ∈ ℂ)
313	312	addid2d 11106	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))
314	294	nn0cnd 12225	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) ∈ ℂ)
315	299	recnd 10934	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-1↑(𝑀 − 𝑗)) ∈ ℂ)
316	308	recnd 10934	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((tan‘𝐴)↑-2)↑𝑗) ∈ ℂ)
317	314, 315, 316	mulassd 10929	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
318	317	oveq2d 7271	. . . . . . . . 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 10926	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℂ)
321	319, 314, 320	mul12d 11114	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((𝑁C(2 · 𝑗)) · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
322	318, 321	eqtrd 2778	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))) = ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))))
323		bccmpl 13951	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · 𝑗) ∈ ℤ) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
324	14, 292, 323	syl2an2r 681	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁C(2 · 𝑗)) = (𝑁C(𝑁 − (2 · 𝑗))))
325	108	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
326	291	nn0cnd 12225	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑗) ∈ ℂ)
327	325, 326	nncand 11267	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (𝑁 − (2 · 𝑗))) = (2 · 𝑗))
328	327	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
329	2	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℝ⁺)
330	329	rpcnd 12703	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ∈ ℂ)
331		expneg 13718	. . . . . . . . . . . . . 14 ⊢ (((tan‘𝐴) ∈ ℂ ∧ (2 · 𝑗) ∈ ℕ₀) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
332	330, 291, 331	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑-(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
333	289	nn0cnd 12225	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
334		mulneg1 11341	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (-2 · 𝑗) = -(2 · 𝑗))
335	110, 333, 334	sylancr 586	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (-2 · 𝑗) = -(2 · 𝑗))
336	335	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((tan‘𝐴)↑-(2 · 𝑗)))
337	329	rpne0d 12706	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (tan‘𝐴) ≠ 0)
338	330, 337, 292	exprecd 13800	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(2 · 𝑗)) = (1 / ((tan‘𝐴)↑(2 · 𝑗))))
339	332, 336, 338	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = ((1 / (tan‘𝐴))↑(2 · 𝑗)))
340	303	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → -2 ∈ ℤ)
341	289	nn0zd 12353	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℤ)
342		expmulz 13757	. . . . . . . . . . . . 13 ⊢ ((((tan‘𝐴) ∈ ℂ ∧ (tan‘𝐴) ≠ 0) ∧ (-2 ∈ ℤ ∧ 𝑗 ∈ ℤ)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
343	330, 337, 340, 341, 342	syl22anc 835	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((tan‘𝐴)↑(-2 · 𝑗)) = (((tan‘𝐴)↑-2)↑𝑗))
344	328, 339, 343	3eqtr2d 2784	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) = (((tan‘𝐴)↑-2)↑𝑗))
345	7	oveq1i 7265	. . . . . . . . . . . . . . 15 ⊢ (𝑁 − (2 · 𝑗)) = (((2 · 𝑀) + 1) − (2 · 𝑗))
346	11	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℕ)
347	346	nncnd 11919	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · 𝑀) ∈ ℂ)
348		1cnd 10901	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 1 ∈ ℂ)
349	347, 348, 326	addsubd 11283	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
350		2cnd 11981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℂ)
351	212	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
352	350, 351, 333	subdid 11361	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) = ((2 · 𝑀) − (2 · 𝑗)))
353	352	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((2 · (𝑀 − 𝑗)) + 1) = (((2 · 𝑀) − (2 · 𝑗)) + 1))
354	349, 353	eqtr4d 2781	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((2 · 𝑀) + 1) − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
355	345, 354	syl5eq 2791	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (𝑁 − (2 · 𝑗)) = ((2 · (𝑀 − 𝑗)) + 1))
356	355	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i↑((2 · (𝑀 − 𝑗)) + 1)))
357		nn0mulcl 12199	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℕ₀ ∧ (𝑀 − 𝑗) ∈ ℕ₀) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
358	75, 297, 357	sylancr 586	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (2 · (𝑀 − 𝑗)) ∈ ℕ₀)
359		expp1 13717	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ (2 · (𝑀 − 𝑗)) ∈ ℕ₀) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
360	5, 358, 359	sylancr 586	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑((2 · (𝑀 − 𝑗)) + 1)) = ((i↑(2 · (𝑀 − 𝑗))) · i))
361	75	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → 2 ∈ ℕ₀)
362	319, 297, 361	expmuld 13795	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = ((i↑2)↑(𝑀 − 𝑗)))
363	167	oveq1i 7265	. . . . . . . . . . . . . . 15 ⊢ ((i↑2)↑(𝑀 − 𝑗)) = (-1↑(𝑀 − 𝑗))
364	362, 363	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(2 · (𝑀 − 𝑗))) = (-1↑(𝑀 − 𝑗)))
365	364	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i↑(2 · (𝑀 − 𝑗))) · i) = ((-1↑(𝑀 − 𝑗)) · i))
366	356, 360, 365	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = ((-1↑(𝑀 − 𝑗)) · i))
367		mulcom 10888	. . . . . . . . . . . . 13 ⊢ (((-1↑(𝑀 − 𝑗)) ∈ ℂ ∧ i ∈ ℂ) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
368	315, 5, 367	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((-1↑(𝑀 − 𝑗)) · i) = (i · (-1↑(𝑀 − 𝑗))))
369	366, 368	eqtrd 2778	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i↑(𝑁 − (2 · 𝑗))) = (i · (-1↑(𝑀 − 𝑗))))
370	344, 369	oveq12d 7273	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
371		mulcl 10886	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (-1↑(𝑀 − 𝑗)) ∈ ℂ) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
372	5, 315, 371	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · (-1↑(𝑀 − 𝑗))) ∈ ℂ)
373	372, 316	mulcomd 10927	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = ((((tan‘𝐴)↑-2)↑𝑗) · (i · (-1↑(𝑀 − 𝑗)))))
374	319, 315, 316	mulassd 10929	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((i · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) = (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))))
375	370, 373, 374	3eqtr2rd 2785	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗))) = (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))
376	324, 375	oveq12d 7273	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑁C(2 · 𝑗)) · (i · ((-1↑(𝑀 − 𝑗)) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
377	313, 322, 376	3eqtrd 2782	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))) = ((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗))))))
378	377	fveq2d 6760	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))))
379		0re 10908	. . . . . . 7 ⊢ 0 ∈ ℝ
380		crim 14754	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ ℝ) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
381	379, 309, 380	sylancr 586	. . . . . 6 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘(0 + (i · (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
382	378, 381	eqtr3d 2780	. . . . 5 ⊢ (((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) ∧ 𝑗 ∈ (0...𝑀)) → (ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
383	382	sumeq2dv 15343	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑗 ∈ (0...𝑀)(ℑ‘((𝑁C(𝑁 − (2 · 𝑗))) · (((1 / (tan‘𝐴))↑(𝑁 − (𝑁 − (2 · 𝑗)))) · (i↑(𝑁 − (2 · 𝑗)))))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
384	157, 287, 383	3eqtr3d 2786	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
385	286, 153	fsumim 15449	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = Σ𝑚 ∈ (0...𝑁)(ℑ‘((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))))
386	305	rpcnd 12703	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((tan‘𝐴)↑-2) ∈ ℂ)
387		oveq1 7262	. . . . . . 7 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (𝑡↑𝑗) = (((tan‘𝐴)↑-2)↑𝑗))
388	387	oveq2d 7271	. . . . . 6 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = (((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
389	388	sumeq2sdv 15344	. . . . 5 ⊢ (𝑡 = ((tan‘𝐴)↑-2) → Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)) = Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)))
390		basel.p	. . . . 5 ⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗)))
391		sumex 15327	. . . . 5 ⊢ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (((tan‘𝐴)↑-2)↑𝑗)) ∈ V
392	389, 390, 391	fvmpt 6857	. . . 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 2788	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (((1 / (tan‘𝐴))↑(𝑁 − 𝑚)) · (i↑𝑚)))) = (𝑃‘((tan‘𝐴)↑-2)))
395	51, 58	rerpdivcld 12732	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
396	53, 58	rerpdivcld 12732	. . 3 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) ∈ ℝ)
397	395, 396	crimd 14871	. 2 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (ℑ‘(((cos‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)) + (i · ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁))))) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))
398	66, 394, 397	3eqtr3d 2786	1 ⊢ ((𝑀 ∈ ℕ ∧ 𝐴 ∈ (0(,)(π / 2))) → (𝑃‘((tan‘𝐴)↑-2)) = ((sin‘(𝑁 · 𝐴)) / ((sin‘𝐴)↑𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∖ cdif 3880 class class class wbr 5070 ↦ cmpt 5153 ran crn 5581 Fn wfn 6413 –1-1→wf1 6415 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 ici 10804 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 (,)cioo 13008 ...cfz 13168 ↑cexp 13710 Ccbc 13944 ℑcim 14737 Σcsu 15325 sincsin 15701 cosccos 15702 tanctan 15703 πcpi 15704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-fac 13916 df-bc 13945 df-hash 13973 df-shft 14706 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-limsup 15108 df-clim 15125 df-rlim 15126 df-sum 15326 df-ef 15705 df-sin 15707 df-cos 15708 df-tan 15709 df-pi 15710 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-pt 17072 df-prds 17075 df-xrs 17130 df-qtop 17135 df-imas 17136 df-xps 17138 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-submnd 18346 df-mulg 18616 df-cntz 18838 df-cmn 19303 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-fbas 20507 df-fg 20508 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-perf 22196 df-cn 22286 df-cnp 22287 df-haus 22374 df-tx 22621 df-hmeo 22814 df-fil 22905 df-fm 22997 df-flim 22998 df-flf 22999 df-xms 23381 df-ms 23382 df-tms 23383 df-cncf 23947 df-limc 24935 df-dv 24936

This theorem is referenced by: basellem4 26138

W3C validator