basellem3

Description: Lemma for basel . Using the binomial theorem and de Moivre's formula, we have the identity _e ^i N x / ( sin x ) ^ n = sum m e. ( 0 ... N ) ( NC m ) ( i ^ m ) ( cot x ) ^ ( N - m ) , so taking imaginary parts yields sin ( N x ) / ( sin x ) ^ N = sum_ j e. ( 0 ... M ) ( N _C 2 j ) ( -u 1 ) ^ ( M - j ) ( cot x ) ^ ( -u 2 j ) = P ( ( cot x ) ^ 2 ) , where N = 2 M + 1 . (Contributed by Mario Carneiro, 30-Jul-2014)

	Ref	Expression
Hypotheses	basel.n	$⊢ N = 2 \cdot M + 1$
	basel.p	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
Assertion	basellem3	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to P ({\tan A}^{- 2}) = \frac{\sin N A}{{\sin A}^{N}}$

Proof

Step	Hyp	Ref	Expression
1		basel.n	$⊢ N = 2 \cdot M + 1$
2		basel.p	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
3		tanrpcl	$⊢ A \in (0, \frac{π}{2}) \to \tan A \in ℝ^{+}$
4	3	adantl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \tan A \in ℝ^{+}$
5	4	rpreccld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{1}{\tan A} \in ℝ^{+}$
6	5	rpcnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{1}{\tan A} \in ℂ$
7		ax-icn	$⊢ i \in ℂ$
8	7	a1i	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to i \in ℂ$
9		2nn	$⊢ 2 \in ℕ$
10		simpl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to M \in ℕ$
11		nnmulcl	$⊢ (2 \in ℕ \land M \in ℕ) \to 2 \cdot M \in ℕ$
12	9 10 11	sylancr	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 2 \cdot M \in ℕ$
13	12	peano2nnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 2 \cdot M + 1 \in ℕ$
14	1 13	eqeltrid	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N \in ℕ$
15	14	nnnn0d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N \in ℕ_{0}$
16		binom	$⊢ (\frac{1}{\tan A} \in ℂ \land i \in ℂ \land N \in ℕ_{0}) \to {((\frac{1}{\tan A}) + i)}^{N} = \sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}$
17	6 8 15 16	syl3anc	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {((\frac{1}{\tan A}) + i)}^{N} = \sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}$
18		elioore	$⊢ A \in (0, \frac{π}{2}) \to A \in ℝ$
19	18	adantl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to A \in ℝ$
20	19	recoscld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos A \in ℝ$
21	20	recnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos A \in ℂ$
22	19	resincld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin A \in ℝ$
23	22	recnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin A \in ℂ$
24		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
25	7 23 24	sylancr	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to i \sin A \in ℂ$
26	21 25	addcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos A + i \sin A \in ℂ$
27		sincosq1sgn	$⊢ A \in (0, \frac{π}{2}) \to (0 < \sin A \land 0 < \cos A)$
28	27	adantl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (0 < \sin A \land 0 < \cos A)$
29	28	simpld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 0 < \sin A$
30	29	gt0ne0d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin A \neq 0$
31	26 23 30 15	expdivd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {(\frac{\cos A + i \sin A}{\sin A})}^{N} = \frac{{(\cos A + i \sin A)}^{N}}{{\sin A}^{N}}$
32	21 25 23 30	divdird	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos A + i \sin A}{\sin A} = (\frac{\cos A}{\sin A}) + (\frac{i \sin A}{\sin A})$
33	19	recnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to A \in ℂ$
34	28	simprd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 0 < \cos A$
35	34	gt0ne0d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos A \neq 0$
36		tanval	$⊢ (A \in ℂ \land \cos A \neq 0) \to \tan A = \frac{\sin A}{\cos A}$
37	33 35 36	syl2anc	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \tan A = \frac{\sin A}{\cos A}$
38	37	oveq2d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{1}{\tan A} = \frac{1}{\frac{\sin A}{\cos A}}$
39	23 21 30 35	recdivd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{1}{\frac{\sin A}{\cos A}} = \frac{\cos A}{\sin A}$
40	38 39	eqtr2d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos A}{\sin A} = \frac{1}{\tan A}$
41	8 23 30	divcan4d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{i \sin A}{\sin A} = i$
42	40 41	oveq12d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (\frac{\cos A}{\sin A}) + (\frac{i \sin A}{\sin A}) = (\frac{1}{\tan A}) + i$
43	32 42	eqtrd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos A + i \sin A}{\sin A} = (\frac{1}{\tan A}) + i$
44	43	oveq1d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {(\frac{\cos A + i \sin A}{\sin A})}^{N} = {((\frac{1}{\tan A}) + i)}^{N}$
45	14	nnzd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N \in ℤ$
46		demoivre	$⊢ (A \in ℂ \land N \in ℤ) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$
47	33 45 46	syl2anc	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {(\cos A + i \sin A)}^{N} = \cos N A + i \sin N A$
48	47	oveq1d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{{(\cos A + i \sin A)}^{N}}{{\sin A}^{N}} = \frac{\cos N A + i \sin N A}{{\sin A}^{N}}$
49	31 44 48	3eqtr3d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {((\frac{1}{\tan A}) + i)}^{N} = \frac{\cos N A + i \sin N A}{{\sin A}^{N}}$
50	14	nnred	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N \in ℝ$
51	50 19	remulcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N A \in ℝ$
52	51	recoscld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos N A \in ℝ$
53	52	recnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \cos N A \in ℂ$
54	51	resincld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin N A \in ℝ$
55	54	recnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin N A \in ℂ$
56		mulcl	$⊢ (i \in ℂ \land \sin N A \in ℂ) \to i \sin N A \in ℂ$
57	7 55 56	sylancr	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to i \sin N A \in ℂ$
58	22 29	elrpd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sin A \in ℝ^{+}$
59	58 45	rpexpcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\sin A}^{N} \in ℝ^{+}$
60	59	rpcnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\sin A}^{N} \in ℂ$
61	59	rpne0d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\sin A}^{N} \neq 0$
62	53 57 60 61	divdird	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos N A + i \sin N A}{{\sin A}^{N}} = (\frac{\cos N A}{{\sin A}^{N}}) + (\frac{i \sin N A}{{\sin A}^{N}})$
63	8 55 60 61	divassd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{i \sin N A}{{\sin A}^{N}} = i (\frac{\sin N A}{{\sin A}^{N}})$
64	63	oveq2d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (\frac{\cos N A}{{\sin A}^{N}}) + (\frac{i \sin N A}{{\sin A}^{N}}) = (\frac{\cos N A}{{\sin A}^{N}}) + i (\frac{\sin N A}{{\sin A}^{N}})$
65	49 62 64	3eqtrd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {((\frac{1}{\tan A}) + i)}^{N} = (\frac{\cos N A}{{\sin A}^{N}}) + i (\frac{\sin N A}{{\sin A}^{N}})$
66	17 65	eqtr3d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m} = (\frac{\cos N A}{{\sin A}^{N}}) + i (\frac{\sin N A}{{\sin A}^{N}})$
67	66	fveq2d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ℑ (\sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = ℑ ((\frac{\cos N A}{{\sin A}^{N}}) + i (\frac{\sin N A}{{\sin A}^{N}}))$
68		oveq2	$⊢ m = N - 2 j \to (\binom{N}{m}) = (\binom{N}{N - 2 j})$
69		oveq2	$⊢ m = N - 2 j \to N - m = N - (N - 2 j)$
70	69	oveq2d	$⊢ m = N - 2 j \to {(\frac{1}{\tan A})}^{N - m} = {(\frac{1}{\tan A})}^{N - (N - 2 j)}$
71		oveq2	$⊢ m = N - 2 j \to i^{m} = i^{N - 2 j}$
72	70 71	oveq12d	$⊢ m = N - 2 j \to {(\frac{1}{\tan A})}^{N - m} i^{m} = {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}$
73	68 72	oveq12d	$⊢ m = N - 2 j \to (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m} = (\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}$
74	73	fveq2d	$⊢ m = N - 2 j \to ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = ℑ ((\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j})$
75		fzfid	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (0 \dots M) \in Fin$
76		2nn0	$⊢ 2 \in ℕ_{0}$
77		elfznn0	$⊢ k \in (0 \dots M) \to k \in ℕ_{0}$
78	77	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to k \in ℕ_{0}$
79		nn0mulcl	$⊢ (2 \in ℕ_{0} \land k \in ℕ_{0}) \to 2 k \in ℕ_{0}$
80	76 78 79	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \in ℕ_{0}$
81	80	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \in ℝ$
82	12	nnred	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 2 \cdot M \in ℝ$
83	82	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 \cdot M \in ℝ$
84	50	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to N \in ℝ$
85		elfzle2	$⊢ k \in (0 \dots M) \to k \leq M$
86	85	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to k \leq M$
87	78	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to k \in ℝ$
88		nnre	$⊢ M \in ℕ \to M \in ℝ$
89	88	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to M \in ℝ$
90		2re	$⊢ 2 \in ℝ$
91		2pos	$⊢ 0 < 2$
92	90 91	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
93	92	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to (2 \in ℝ \land 0 < 2)$
94		lemul2	$⊢ (k \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (k \leq M \leftrightarrow 2 k \leq 2 \cdot M)$
95	87 89 93 94	syl3anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to (k \leq M \leftrightarrow 2 k \leq 2 \cdot M)$
96	86 95	mpbid	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \leq 2 \cdot M$
97	83	lep1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 \cdot M \leq 2 \cdot M + 1$
98	97 1	breqtrrdi	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 \cdot M \leq N$
99	81 83 84 96 98	letrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \leq N$
100		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
101	80 100	eleqtrdi	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \in ℤ_{\geq 0}$
102	45	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to N \in ℤ$
103		elfz5	$⊢ (2 k \in ℤ_{\geq 0} \land N \in ℤ) \to (2 k \in (0 \dots N) \leftrightarrow 2 k \leq N)$
104	101 102 103	syl2anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to (2 k \in (0 \dots N) \leftrightarrow 2 k \leq N)$
105	99 104	mpbird	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to 2 k \in (0 \dots N)$
106		fznn0sub2	$⊢ 2 k \in (0 \dots N) \to N - 2 k \in (0 \dots N)$
107	105 106	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land k \in (0 \dots M)) \to N - 2 k \in (0 \dots N)$
108	107	ex	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) \to N - 2 k \in (0 \dots N))$
109	14	nncnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to N \in ℂ$
110	109	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to N \in ℂ$
111		2cn	$⊢ 2 \in ℂ$
112		elfzelz	$⊢ k \in (0 \dots M) \to k \in ℤ$
113	112	zcnd	$⊢ k \in (0 \dots M) \to k \in ℂ$
114	113	ad2antrl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to k \in ℂ$
115		mulcl	$⊢ (2 \in ℂ \land k \in ℂ) \to 2 k \in ℂ$
116	111 114 115	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to 2 k \in ℂ$
117	113	ssriv	$⊢ (0 \dots M) \subseteq ℂ$
118		simprr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to m \in (0 \dots M)$
119	117 118	sseldi	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to m \in ℂ$
120		mulcl	$⊢ (2 \in ℂ \land m \in ℂ) \to 2 m \in ℂ$
121	111 119 120	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to 2 m \in ℂ$
122	110 116 121	subcanad	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to (N - 2 k = N - 2 m \leftrightarrow 2 k = 2 m)$
123		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
124	123	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to (2 \in ℂ \land 2 \neq 0)$
125		mulcan	$⊢ (k \in ℂ \land m \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (2 k = 2 m \leftrightarrow k = m)$
126	114 119 124 125	syl3anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to (2 k = 2 m \leftrightarrow k = m)$
127	122 126	bitrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (k \in (0 \dots M) \land m \in (0 \dots M))) \to (N - 2 k = N - 2 m \leftrightarrow k = m)$
128	127	ex	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ((k \in (0 \dots M) \land m \in (0 \dots M)) \to (N - 2 k = N - 2 m \leftrightarrow k = m))$
129	108 128	dom2lem	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) ⟼ N - 2 k) : (0 \dots M) \underset{1-1}{⟶} (0 \dots N)$
130		f1f1orn	$⊢ (k \in (0 \dots M) ⟼ N - 2 k) : (0 \dots M) \underset{1-1}{⟶} (0 \dots N) \to (k \in (0 \dots M) ⟼ N - 2 k) : (0 \dots M) \underset{1-1 onto}{⟶} ran (k \in (0 \dots M) ⟼ N - 2 k)$
131	129 130	syl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) ⟼ N - 2 k) : (0 \dots M) \underset{1-1 onto}{⟶} ran (k \in (0 \dots M) ⟼ N - 2 k)$
132		oveq2	$⊢ k = j \to 2 k = 2 j$
133	132	oveq2d	$⊢ k = j \to N - 2 k = N - 2 j$
134		eqid	$⊢ (k \in (0 \dots M) ⟼ N - 2 k) = (k \in (0 \dots M) ⟼ N - 2 k)$
135		ovex	$⊢ N - 2 j \in V$
136	133 134 135	fvmpt	$⊢ j \in (0 \dots M) \to (k \in (0 \dots M) ⟼ N - 2 k) (j) = N - 2 j$
137	136	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (k \in (0 \dots M) ⟼ N - 2 k) (j) = N - 2 j$
138	107	fmpttd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) ⟼ N - 2 k) : (0 \dots M) ⟶ (0 \dots N)$
139	138	frnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ran (k \in (0 \dots M) ⟼ N - 2 k) \subseteq (0 \dots N)$
140	139	sselda	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ran (k \in (0 \dots M) ⟼ N - 2 k)) \to m \in (0 \dots N)$
141		bccl2	$⊢ m \in (0 \dots N) \to (\binom{N}{m}) \in ℕ$
142	141	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\binom{N}{m}) \in ℕ$
143	142	nncnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\binom{N}{m}) \in ℂ$
144	4	rprecred	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{1}{\tan A} \in ℝ$
145		fznn0sub	$⊢ m \in (0 \dots N) \to N - m \in ℕ_{0}$
146		reexpcl	$⊢ (\frac{1}{\tan A} \in ℝ \land N - m \in ℕ_{0}) \to {(\frac{1}{\tan A})}^{N - m} \in ℝ$
147	144 145 146	syl2an	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to {(\frac{1}{\tan A})}^{N - m} \in ℝ$
148	147	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to {(\frac{1}{\tan A})}^{N - m} \in ℂ$
149		elfznn0	$⊢ m \in (0 \dots N) \to m \in ℕ_{0}$
150	149	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to m \in ℕ_{0}$
151		expcl	$⊢ (i \in ℂ \land m \in ℕ_{0}) \to i^{m} \in ℂ$
152	7 150 151	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to i^{m} \in ℂ$
153	148 152	mulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to {(\frac{1}{\tan A})}^{N - m} i^{m} \in ℂ$
154	143 153	mulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m} \in ℂ$
155	140 154	syldan	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ran (k \in (0 \dots M) ⟼ N - 2 k)) \to (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m} \in ℂ$
156	155	imcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ran (k \in (0 \dots M) ⟼ N - 2 k)) \to ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) \in ℝ$
157	156	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ran (k \in (0 \dots M) ⟼ N - 2 k)) \to ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) \in ℂ$
158	74 75 131 137 157	fsumf1o	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sum_{m \in ran (k \in (0 \dots M) ⟼ N - 2 k)} ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = \sum_{j = 0}^{M} ℑ ((\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j})$
159		eldifi	$⊢ m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k)) \to m \in (0 \dots N)$
160	142	nnred	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\binom{N}{m}) \in ℝ$
161	159 160	sylan2	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to (\binom{N}{m}) \in ℝ$
162	159 147	sylan2	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to {(\frac{1}{\tan A})}^{N - m} \in ℝ$
163		eldif	$⊢ m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k)) \leftrightarrow (m \in (0 \dots N) \land \neg m \in ran (k \in (0 \dots M) ⟼ N - 2 k))$
164		elfzelz	$⊢ m \in (0 \dots N) \to m \in ℤ$
165	164	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to m \in ℤ$
166		zeo	$⊢ m \in ℤ \to (\frac{m}{2} \in ℤ \lor \frac{m + 1}{2} \in ℤ)$
167	165 166	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\frac{m}{2} \in ℤ \lor \frac{m + 1}{2} \in ℤ)$
168		i2	$⊢ i^{2} = - 1$
169	168	oveq1i	$⊢ {(i^{2})}^{\frac{m}{2}} = {(- 1)}^{\frac{m}{2}}$
170		simprr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to \frac{m}{2} \in ℤ$
171	149	ad2antrl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to m \in ℕ_{0}$
172		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
173		nn0ge0	$⊢ m \in ℕ_{0} \to 0 \leq m$
174		divge0	$⊢ ((m \in ℝ \land 0 \leq m) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{m}{2}$
175	90 91 174	mpanr12	$⊢ (m \in ℝ \land 0 \leq m) \to 0 \leq \frac{m}{2}$
176	172 173 175	syl2anc	$⊢ m \in ℕ_{0} \to 0 \leq \frac{m}{2}$
177	171 176	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to 0 \leq \frac{m}{2}$
178		elnn0z	$⊢ \frac{m}{2} \in ℕ_{0} \leftrightarrow (\frac{m}{2} \in ℤ \land 0 \leq \frac{m}{2})$
179	170 177 178	sylanbrc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to \frac{m}{2} \in ℕ_{0}$
180		expmul	$⊢ (i \in ℂ \land 2 \in ℕ_{0} \land \frac{m}{2} \in ℕ_{0}) \to i^{2 (\frac{m}{2})} = {(i^{2})}^{\frac{m}{2}}$
181	7 76 179 180	mp3an12i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to i^{2 (\frac{m}{2})} = {(i^{2})}^{\frac{m}{2}}$
182	171	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to m \in ℂ$
183		2ne0	$⊢ 2 \neq 0$
184		divcan2	$⊢ (m \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{m}{2}) = m$
185	111 183 184	mp3an23	$⊢ m \in ℂ \to 2 (\frac{m}{2}) = m$
186	182 185	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to 2 (\frac{m}{2}) = m$
187	186	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to i^{2 (\frac{m}{2})} = i^{m}$
188	181 187	eqtr3d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to {(i^{2})}^{\frac{m}{2}} = i^{m}$
189	169 188	syl5eqr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to {(- 1)}^{\frac{m}{2}} = i^{m}$
190		neg1rr	$⊢ - 1 \in ℝ$
191		reexpcl	$⊢ (- 1 \in ℝ \land \frac{m}{2} \in ℕ_{0}) \to {(- 1)}^{\frac{m}{2}} \in ℝ$
192	190 179 191	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to {(- 1)}^{\frac{m}{2}} \in ℝ$
193	189 192	eqeltrrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m}{2} \in ℤ)) \to i^{m} \in ℝ$
194	193	expr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\frac{m}{2} \in ℤ \to i^{m} \in ℝ)$
195	145	ad2antrl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m \in ℕ_{0}$
196		nn0re	$⊢ N - m \in ℕ_{0} \to N - m \in ℝ$
197		nn0ge0	$⊢ N - m \in ℕ_{0} \to 0 \leq N - m$
198		divge0	$⊢ ((N - m \in ℝ \land 0 \leq N - m) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{N - m}{2}$
199	90 91 198	mpanr12	$⊢ (N - m \in ℝ \land 0 \leq N - m) \to 0 \leq \frac{N - m}{2}$
200	196 197 199	syl2anc	$⊢ N - m \in ℕ_{0} \to 0 \leq \frac{N - m}{2}$
201	195 200	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 0 \leq \frac{N - m}{2}$
202	195	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m \in ℝ$
203	50	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N \in ℝ$
204		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
205	203 204	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N + 1 \in ℝ$
206	149	ad2antrl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ℕ_{0}$
207	206 173	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 0 \leq m$
208	206	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ℝ$
209	203 208	subge02d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (0 \leq m \leftrightarrow N - m \leq N)$
210	207 209	mpbid	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m \leq N$
211	203	ltp1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N < N + 1$
212	202 203 205 210 211	lelttrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m < N + 1$
213		2t1e2	$⊢ 2 \cdot 1 = 2$
214		df-2	$⊢ 2 = 1 + 1$
215	213 214	eqtr2i	$⊢ 1 + 1 = 2 \cdot 1$
216	215	oveq2i	$⊢ 2 \cdot M + 1 + 1 = 2 \cdot M + 2 \cdot 1$
217	1	oveq1i	$⊢ N + 1 = 2 \cdot M + 1 + 1$
218	12	nncnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 2 \cdot M \in ℂ$
219	218	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 \cdot M \in ℂ$
220		1cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 1 \in ℂ$
221	219 220 220	addassd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 \cdot M + 1 + 1 = 2 \cdot M + 1 + 1$
222	217 221	syl5eq	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N + 1 = 2 \cdot M + 1 + 1$
223		2cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 \in ℂ$
224		nncn	$⊢ M \in ℕ \to M \in ℂ$
225	224	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M \in ℂ$
226	223 225 220	adddid	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 (M + 1) = 2 \cdot M + 2 \cdot 1$
227	216 222 226	3eqtr4a	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N + 1 = 2 (M + 1)$
228	212 227	breqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m < 2 (M + 1)$
229		nnz	$⊢ M \in ℕ \to M \in ℤ$
230	229	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M \in ℤ$
231	230	peano2zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M + 1 \in ℤ$
232	231	zred	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M + 1 \in ℝ$
233	92	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (2 \in ℝ \land 0 < 2)$
234		ltdivmul	$⊢ (N - m \in ℝ \land M + 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{N - m}{2} < M + 1 \leftrightarrow N - m < 2 (M + 1))$
235	202 232 233 234	syl3anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (\frac{N - m}{2} < M + 1 \leftrightarrow N - m < 2 (M + 1))$
236	228 235	mpbird	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} < M + 1$
237	109	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N \in ℂ$
238	206	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ℂ$
239	237 238 220	pnpcan2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N + 1 - (m + 1) = N - m$
240	227	oveq1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N + 1 - (m + 1) = 2 (M + 1) - (m + 1)$
241	239 240	eqtr3d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m = 2 (M + 1) - (m + 1)$
242	241	oveq1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} = \frac{2 (M + 1) - (m + 1)}{2}$
243	231	zcnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M + 1 \in ℂ$
244		mulcl	$⊢ (2 \in ℂ \land M + 1 \in ℂ) \to 2 (M + 1) \in ℂ$
245	111 243 244	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 (M + 1) \in ℂ$
246		peano2cn	$⊢ m \in ℂ \to m + 1 \in ℂ$
247	238 246	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m + 1 \in ℂ$
248	123	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (2 \in ℂ \land 2 \neq 0)$
249		divsubdir	$⊢ (2 (M + 1) \in ℂ \land m + 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 (M + 1) - (m + 1)}{2} = (\frac{2 (M + 1)}{2}) - (\frac{m + 1}{2})$
250	245 247 248 249	syl3anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{2 (M + 1) - (m + 1)}{2} = (\frac{2 (M + 1)}{2}) - (\frac{m + 1}{2})$
251	183	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 \neq 0$
252	243 223 251	divcan3d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{2 (M + 1)}{2} = M + 1$
253	252	oveq1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (\frac{2 (M + 1)}{2}) - (\frac{m + 1}{2}) = M + 1 - (\frac{m + 1}{2})$
254	242 250 253	3eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} = M + 1 - (\frac{m + 1}{2})$
255		simprr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{m + 1}{2} \in ℤ$
256	231 255	zsubcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M + 1 - (\frac{m + 1}{2}) \in ℤ$
257	254 256	eqeltrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} \in ℤ$
258		zleltp1	$⊢ (\frac{N - m}{2} \in ℤ \land M \in ℤ) \to (\frac{N - m}{2} \leq M \leftrightarrow \frac{N - m}{2} < M + 1)$
259	257 230 258	syl2anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (\frac{N - m}{2} \leq M \leftrightarrow \frac{N - m}{2} < M + 1)$
260	236 259	mpbird	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} \leq M$
261		0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 0 \in ℤ$
262		elfz	$⊢ (\frac{N - m}{2} \in ℤ \land 0 \in ℤ \land M \in ℤ) \to (\frac{N - m}{2} \in (0 \dots M) \leftrightarrow (0 \leq \frac{N - m}{2} \land \frac{N - m}{2} \leq M))$
263	257 261 230 262	syl3anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (\frac{N - m}{2} \in (0 \dots M) \leftrightarrow (0 \leq \frac{N - m}{2} \land \frac{N - m}{2} \leq M))$
264	201 260 263	mpbir2and	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to \frac{N - m}{2} \in (0 \dots M)$
265		oveq2	$⊢ k = \frac{N - m}{2} \to 2 k = 2 (\frac{N - m}{2})$
266	265	oveq2d	$⊢ k = \frac{N - m}{2} \to N - 2 k = N - 2 (\frac{N - m}{2})$
267		ovex	$⊢ N - 2 (\frac{N - m}{2}) \in V$
268	266 134 267	fvmpt	$⊢ \frac{N - m}{2} \in (0 \dots M) \to (k \in (0 \dots M) ⟼ N - 2 k) (\frac{N - m}{2}) = N - 2 (\frac{N - m}{2})$
269	264 268	syl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (k \in (0 \dots M) ⟼ N - 2 k) (\frac{N - m}{2}) = N - 2 (\frac{N - m}{2})$
270	195	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - m \in ℂ$
271	270 223 251	divcan2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 (\frac{N - m}{2}) = N - m$
272	271	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - 2 (\frac{N - m}{2}) = N - (N - m)$
273	237 238	nncand	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to N - (N - m) = m$
274	269 272 273	3eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (k \in (0 \dots M) ⟼ N - 2 k) (\frac{N - m}{2}) = m$
275	138	ffnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) ⟼ N - 2 k) Fn (0 \dots M)$
276		fnfvelrn	$⊢ ((k \in (0 \dots M) ⟼ N - 2 k) Fn (0 \dots M) \land \frac{N - m}{2} \in (0 \dots M)) \to (k \in (0 \dots M) ⟼ N - 2 k) (\frac{N - m}{2}) \in ran (k \in (0 \dots M) ⟼ N - 2 k)$
277	275 264 276	syl2an2r	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to (k \in (0 \dots M) ⟼ N - 2 k) (\frac{N - m}{2}) \in ran (k \in (0 \dots M) ⟼ N - 2 k)$
278	274 277	eqeltrrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ran (k \in (0 \dots M) ⟼ N - 2 k)$
279	278	expr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\frac{m + 1}{2} \in ℤ \to m \in ran (k \in (0 \dots M) ⟼ N - 2 k))$
280	194 279	orim12d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to ((\frac{m}{2} \in ℤ \lor \frac{m + 1}{2} \in ℤ) \to (i^{m} \in ℝ \lor m \in ran (k \in (0 \dots M) ⟼ N - 2 k)))$
281	167 280	mpd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (i^{m} \in ℝ \lor m \in ran (k \in (0 \dots M) ⟼ N - 2 k))$
282	281	orcomd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (m \in ran (k \in (0 \dots M) ⟼ N - 2 k) \lor i^{m} \in ℝ)$
283	282	ord	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in (0 \dots N)) \to (\neg m \in ran (k \in (0 \dots M) ⟼ N - 2 k) \to i^{m} \in ℝ)$
284	283	impr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \neg m \in ran (k \in (0 \dots M) ⟼ N - 2 k))) \to i^{m} \in ℝ$
285	163 284	sylan2b	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to i^{m} \in ℝ$
286	162 285	remulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to {(\frac{1}{\tan A})}^{N - m} i^{m} \in ℝ$
287	161 286	remulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m} \in ℝ$
288	287	reim0d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land m \in ((0 \dots N) ∖ ran (k \in (0 \dots M) ⟼ N - 2 k))) \to ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = 0$
289		fzfid	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (0 \dots N) \in Fin$
290	139 157 288 289	fsumss	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sum_{m \in ran (k \in (0 \dots M) ⟼ N - 2 k)} ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = \sum_{m = 0}^{N} ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m})$
291		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
292	291	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℕ_{0}$
293		nn0mulcl	$⊢ (2 \in ℕ_{0} \land j \in ℕ_{0}) \to 2 j \in ℕ_{0}$
294	76 292 293	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℕ_{0}$
295	294	nn0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℤ$
296		bccl	$⊢ (N \in ℕ_{0} \land 2 j \in ℤ) \to (\binom{N}{2 j}) \in ℕ_{0}$
297	15 295 296	syl2an2r	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℕ_{0}$
298	297	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℝ$
299		fznn0sub	$⊢ j \in (0 \dots M) \to M - j \in ℕ_{0}$
300	299	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to M - j \in ℕ_{0}$
301		reexpcl	$⊢ (- 1 \in ℝ \land M - j \in ℕ_{0}) \to {(- 1)}^{M - j} \in ℝ$
302	190 300 301	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} \in ℝ$
303	298 302	remulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} \in ℝ$
304		2z	$⊢ 2 \in ℤ$
305		znegcl	$⊢ 2 \in ℤ \to - 2 \in ℤ$
306	304 305	ax-mp	$⊢ - 2 \in ℤ$
307		rpexpcl	$⊢ (\tan A \in ℝ^{+} \land - 2 \in ℤ) \to {\tan A}^{- 2} \in ℝ^{+}$
308	4 306 307	sylancl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℝ^{+}$
309	308	rpred	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℝ$
310		reexpcl	$⊢ ({\tan A}^{- 2} \in ℝ \land j \in ℕ_{0}) \to {({\tan A}^{- 2})}^{j} \in ℝ$
311	309 291 310	syl2an	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {({\tan A}^{- 2})}^{j} \in ℝ$
312	303 311	remulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℝ$
313	312	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ$
314		mulcl	$⊢ (i \in ℂ \land (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ) \to i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ$
315	7 313 314	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ$
316	315	addid2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 0 + i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
317	297	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℂ$
318	302	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} \in ℂ$
319	311	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {({\tan A}^{- 2})}^{j} \in ℂ$
320	317 318 319	mulassd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
321	320	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
322	7	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i \in ℂ$
323	318 319	mulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ$
324	322 317 323	mul12d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = (\binom{N}{2 j}) i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
325	321 324	eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = (\binom{N}{2 j}) i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
326		bccmpl	$⊢ (N \in ℕ_{0} \land 2 j \in ℤ) \to (\binom{N}{2 j}) = (\binom{N}{N - 2 j})$
327	15 295 326	syl2an2r	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) = (\binom{N}{N - 2 j})$
328	109	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N \in ℂ$
329	294	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℂ$
330	328 329	nncand	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N - (N - 2 j) = 2 j$
331	330	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(\frac{1}{\tan A})}^{N - (N - 2 j)} = {(\frac{1}{\tan A})}^{2 j}$
332	4	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \in ℝ^{+}$
333	332	rpcnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \in ℂ$
334		expneg	$⊢ (\tan A \in ℂ \land 2 j \in ℕ_{0}) \to {\tan A}^{- 2 j} = \frac{1}{{\tan A}^{2 j}}$
335	333 294 334	syl2anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{- 2 j} = \frac{1}{{\tan A}^{2 j}}$
336	292	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℂ$
337		mulneg1	$⊢ (2 \in ℂ \land j \in ℂ) \to -2 j = - 2 j$
338	111 336 337	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to -2 j = - 2 j$
339	338	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{-2 j} = {\tan A}^{- 2 j}$
340	332	rpne0d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \neq 0$
341	333 340 295	exprecd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(\frac{1}{\tan A})}^{2 j} = \frac{1}{{\tan A}^{2 j}}$
342	335 339 341	3eqtr4d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{-2 j} = {(\frac{1}{\tan A})}^{2 j}$
343	306	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to - 2 \in ℤ$
344	292	nn0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℤ$
345		expmulz	$⊢ ((\tan A \in ℂ \land \tan A \neq 0) \land (- 2 \in ℤ \land j \in ℤ)) \to {\tan A}^{-2 j} = {({\tan A}^{- 2})}^{j}$
346	333 340 343 344 345	syl22anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{-2 j} = {({\tan A}^{- 2})}^{j}$
347	331 342 346	3eqtr2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(\frac{1}{\tan A})}^{N - (N - 2 j)} = {({\tan A}^{- 2})}^{j}$
348	1	oveq1i	$⊢ N - 2 j = 2 \cdot M + 1 - 2 j$
349	12	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M \in ℕ$
350	349	nncnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M \in ℂ$
351		1cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 1 \in ℂ$
352	350 351 329	addsubd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M + 1 - 2 j = 2 \cdot M - 2 j + 1$
353		2cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \in ℂ$
354	224	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to M \in ℂ$
355	353 354 336	subdid	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 (M - j) = 2 \cdot M - 2 j$
356	355	oveq1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 (M - j) + 1 = 2 \cdot M - 2 j + 1$
357	352 356	eqtr4d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M + 1 - 2 j = 2 (M - j) + 1$
358	348 357	syl5eq	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N - 2 j = 2 (M - j) + 1$
359	358	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{N - 2 j} = i^{2 (M - j) + 1}$
360		nn0mulcl	$⊢ (2 \in ℕ_{0} \land M - j \in ℕ_{0}) \to 2 (M - j) \in ℕ_{0}$
361	76 300 360	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 (M - j) \in ℕ_{0}$
362		expp1	$⊢ (i \in ℂ \land 2 (M - j) \in ℕ_{0}) \to i^{2 (M - j) + 1} = i^{2 (M - j)} i$
363	7 361 362	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j) + 1} = i^{2 (M - j)} i$
364	76	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \in ℕ_{0}$
365	322 300 364	expmuld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j)} = {(i^{2})}^{M - j}$
366	168	oveq1i	$⊢ {(i^{2})}^{M - j} = {(- 1)}^{M - j}$
367	365 366	syl6eq	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j)} = {(- 1)}^{M - j}$
368	367	oveq1d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j)} i = {(- 1)}^{M - j} i$
369	359 363 368	3eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{N - 2 j} = {(- 1)}^{M - j} i$
370		mulcom	$⊢ ({(- 1)}^{M - j} \in ℂ \land i \in ℂ) \to {(- 1)}^{M - j} i = i {(- 1)}^{M - j}$
371	318 7 370	sylancl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} i = i {(- 1)}^{M - j}$
372	369 371	eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{N - 2 j} = i {(- 1)}^{M - j}$
373	347 372	oveq12d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j} = {({\tan A}^{- 2})}^{j} i {(- 1)}^{M - j}$
374		mulcl	$⊢ (i \in ℂ \land {(- 1)}^{M - j} \in ℂ) \to i {(- 1)}^{M - j} \in ℂ$
375	7 318 374	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i {(- 1)}^{M - j} \in ℂ$
376	375 319	mulcomd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = {({\tan A}^{- 2})}^{j} i {(- 1)}^{M - j}$
377	322 318 319	mulassd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
378	373 376 377	3eqtr2rd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}$
379	327 378	oveq12d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) i {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = (\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}$
380	316 325 379	3eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 0 + i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} = (\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}$
381	380	fveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to ℑ (0 + i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}) = ℑ ((\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j})$
382		0re	$⊢ 0 \in ℝ$
383		crim	$⊢ (0 \in ℝ \land (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℝ) \to ℑ (0 + i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}) = (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
384	382 312 383	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to ℑ (0 + i (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}) = (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
385	381 384	eqtr3d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to ℑ ((\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}) = (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
386	385	sumeq2dv	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sum_{j = 0}^{M} ℑ ((\binom{N}{N - 2 j}) {(\frac{1}{\tan A})}^{N - (N - 2 j)} i^{N - 2 j}) = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
387	158 290 386	3eqtr3d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \sum_{m = 0}^{N} ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
388	289 154	fsumim	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ℑ (\sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = \sum_{m = 0}^{N} ℑ ((\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m})$
389	308	rpcnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℂ$
390		oveq1	$⊢ t = {\tan A}^{- 2} \to t^{j} = {({\tan A}^{- 2})}^{j}$
391	390	oveq2d	$⊢ t = {\tan A}^{- 2} \to (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j} = (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
392	391	sumeq2sdv	$⊢ t = {\tan A}^{- 2} \to \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j} = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
393		sumex	$⊢ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in V$
394	392 2 393	fvmpt	$⊢ {\tan A}^{- 2} \in ℂ \to P ({\tan A}^{- 2}) = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
395	389 394	syl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to P ({\tan A}^{- 2}) = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j}$
396	387 388 395	3eqtr4d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ℑ (\sum_{m = 0}^{N} (\binom{N}{m}) {(\frac{1}{\tan A})}^{N - m} i^{m}) = P ({\tan A}^{- 2})$
397	52 59	rerpdivcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos N A}{{\sin A}^{N}} \in ℝ$
398	54 59	rerpdivcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\sin N A}{{\sin A}^{N}} \in ℝ$
399	397 398	crimd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to ℑ ((\frac{\cos N A}{{\sin A}^{N}}) + i (\frac{\sin N A}{{\sin A}^{N}})) = \frac{\sin N A}{{\sin A}^{N}}$
400	67 396 399	3eqtr3d	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to P ({\tan A}^{- 2}) = \frac{\sin N A}{{\sin A}^{N}}$

Metamath Proof Explorer

Theorem basellem3

Proof