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	sselid	$⊢ ((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	eqtr3id	$⊢ ((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		0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 0 \in ℤ$
196		nnz	$⊢ M \in ℕ \to M \in ℤ$
197	196	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M \in ℤ$
198	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 ℂ$
199	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}$
200	199	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ℂ$
201		1cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 1 \in ℂ$
202	198 200 201	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$
203		2t1e2	$⊢ 2 \cdot 1 = 2$
204		df-2	$⊢ 2 = 1 + 1$
205	203 204	eqtr2i	$⊢ 1 + 1 = 2 \cdot 1$
206	205	oveq2i	$⊢ 2 \cdot M + 1 + 1 = 2 \cdot M + 2 \cdot 1$
207	1	oveq1i	$⊢ N + 1 = 2 \cdot M + 1 + 1$
208	12	nncnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to 2 \cdot M \in ℂ$
209	208	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 ℂ$
210	209 201 201	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$
211	207 210	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$
212		2cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to 2 \in ℂ$
213		nncn	$⊢ M \in ℕ \to M \in ℂ$
214	213	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to M \in ℂ$
215	212 214 201	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$
216	206 211 215	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)$
217	216	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)$
218	202 217	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)$
219	218	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}$
220	197	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 ℤ$
221	220	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 ℂ$
222		mulcl	$⊢ (2 \in ℂ \land M + 1 \in ℂ) \to 2 (M + 1) \in ℂ$
223	111 221 222	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 ℂ$
224		peano2cn	$⊢ m \in ℂ \to m + 1 \in ℂ$
225	200 224	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 ℂ$
226	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)$
227		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})$
228	223 225 226 227	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})$
229	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$
230	221 212 229	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$
231	230	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})$
232	219 228 231	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})$
233		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 ℤ$
234	220 233	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 ℤ$
235	232 234	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 ℤ$
236	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}$
237		nn0re	$⊢ N - m \in ℕ_{0} \to N - m \in ℝ$
238		nn0ge0	$⊢ N - m \in ℕ_{0} \to 0 \leq N - m$
239		divge0	$⊢ ((N - m \in ℝ \land 0 \leq N - m) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{N - m}{2}$
240	90 91 239	mpanr12	$⊢ (N - m \in ℝ \land 0 \leq N - m) \to 0 \leq \frac{N - m}{2}$
241	237 238 240	syl2anc	$⊢ N - m \in ℕ_{0} \to 0 \leq \frac{N - m}{2}$
242	236 241	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}$
243	236	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 ℝ$
244	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 ℝ$
245		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
246	244 245	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 ℝ$
247	199 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$
248	199	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land (m \in (0 \dots N) \land \frac{m + 1}{2} \in ℤ)) \to m \in ℝ$
249	244 248	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)$
250	247 249	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$
251	244	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$
252	243 244 246 250 251	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$
253	252 216	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)$
254	220	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 ℝ$
255	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)$
256		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))$
257	243 254 255 256	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))$
258	253 257	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$
259		zleltp1	$⊢ (\frac{N - m}{2} \in ℤ \land M \in ℤ) \to (\frac{N - m}{2} \leq M \leftrightarrow \frac{N - m}{2} < M + 1)$
260	235 197 259	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)$
261	258 260	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$
262	195 197 235 242 261	elfzd	$⊢ ((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)$
263		oveq2	$⊢ k = \frac{N - m}{2} \to 2 k = 2 (\frac{N - m}{2})$
264	263	oveq2d	$⊢ k = \frac{N - m}{2} \to N - 2 k = N - 2 (\frac{N - m}{2})$
265		ovex	$⊢ N - 2 (\frac{N - m}{2}) \in V$
266	264 134 265	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})$
267	262 266	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})$
268	236	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 ℂ$
269	268 212 229	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$
270	269	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)$
271	198 200	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$
272	267 270 271	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$
273	138	ffnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (k \in (0 \dots M) ⟼ N - 2 k) Fn (0 \dots M)$
274		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)$
275	273 262 274	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)$
276	272 275	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)$
277	276	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))$
278	194 277	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)))$
279	167 278	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))$
280	279	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 ℝ)$
281	280	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 ℝ)$
282	281	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 ℝ$
283	163 282	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 ℝ$
284	162 283	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 ℝ$
285	161 284	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 ℝ$
286	285	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$
287		fzfid	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to (0 \dots N) \in Fin$
288	139 157 286 287	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})$
289		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
290	289	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℕ_{0}$
291		nn0mulcl	$⊢ (2 \in ℕ_{0} \land j \in ℕ_{0}) \to 2 j \in ℕ_{0}$
292	76 290 291	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℕ_{0}$
293	292	nn0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℤ$
294		bccl	$⊢ (N \in ℕ_{0} \land 2 j \in ℤ) \to (\binom{N}{2 j}) \in ℕ_{0}$
295	15 293 294	syl2an2r	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℕ_{0}$
296	295	nn0red	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℝ$
297		fznn0sub	$⊢ j \in (0 \dots M) \to M - j \in ℕ_{0}$
298	297	adantl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to M - j \in ℕ_{0}$
299		reexpcl	$⊢ (- 1 \in ℝ \land M - j \in ℕ_{0}) \to {(- 1)}^{M - j} \in ℝ$
300	190 298 299	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} \in ℝ$
301	296 300	remulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} \in ℝ$
302		2z	$⊢ 2 \in ℤ$
303		znegcl	$⊢ 2 \in ℤ \to - 2 \in ℤ$
304	302 303	ax-mp	$⊢ - 2 \in ℤ$
305		rpexpcl	$⊢ (\tan A \in ℝ^{+} \land - 2 \in ℤ) \to {\tan A}^{- 2} \in ℝ^{+}$
306	4 304 305	sylancl	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℝ^{+}$
307	306	rpred	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℝ$
308		reexpcl	$⊢ ({\tan A}^{- 2} \in ℝ \land j \in ℕ_{0}) \to {({\tan A}^{- 2})}^{j} \in ℝ$
309	307 289 308	syl2an	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {({\tan A}^{- 2})}^{j} \in ℝ$
310	301 309	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 ℝ$
311	310	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 ℂ$
312		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 ℂ$
313	7 311 312	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 ℂ$
314	313	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}$
315	295	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to (\binom{N}{2 j}) \in ℂ$
316	300	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} \in ℂ$
317	309	recnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {({\tan A}^{- 2})}^{j} \in ℂ$
318	315 316 317	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}$
319	318	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}$
320	7	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i \in ℂ$
321	316 317	mulcld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in ℂ$
322	320 315 321	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}$
323	319 322	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}$
324		bccmpl	$⊢ (N \in ℕ_{0} \land 2 j \in ℤ) \to (\binom{N}{2 j}) = (\binom{N}{N - 2 j})$
325	15 293 324	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})$
326	109	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N \in ℂ$
327	292	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 j \in ℂ$
328	326 327	nncand	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N - (N - 2 j) = 2 j$
329	328	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}$
330	4	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \in ℝ^{+}$
331	330	rpcnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \in ℂ$
332		expneg	$⊢ (\tan A \in ℂ \land 2 j \in ℕ_{0}) \to {\tan A}^{- 2 j} = \frac{1}{{\tan A}^{2 j}}$
333	331 292 332	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}}$
334	290	nn0cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℂ$
335		mulneg1	$⊢ (2 \in ℂ \land j \in ℂ) \to -2 j = - 2 j$
336	111 334 335	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to -2 j = - 2 j$
337	336	oveq2d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{-2 j} = {\tan A}^{- 2 j}$
338	330	rpne0d	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to \tan A \neq 0$
339	331 338 293	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}}$
340	333 337 339	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}$
341	304	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to - 2 \in ℤ$
342	290	nn0zd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to j \in ℤ$
343		expmulz	$⊢ ((\tan A \in ℂ \land \tan A \neq 0) \land (- 2 \in ℤ \land j \in ℤ)) \to {\tan A}^{-2 j} = {({\tan A}^{- 2})}^{j}$
344	331 338 341 342 343	syl22anc	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {\tan A}^{-2 j} = {({\tan A}^{- 2})}^{j}$
345	329 340 344	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}$
346	1	oveq1i	$⊢ N - 2 j = 2 \cdot M + 1 - 2 j$
347	12	adantr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M \in ℕ$
348	347	nncnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \cdot M \in ℂ$
349		1cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 1 \in ℂ$
350	348 349 327	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$
351		2cnd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \in ℂ$
352	213	ad2antrr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to M \in ℂ$
353	351 352 334	subdid	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 (M - j) = 2 \cdot M - 2 j$
354	353	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$
355	350 354	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$
356	346 355	syl5eq	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to N - 2 j = 2 (M - j) + 1$
357	356	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}$
358		nn0mulcl	$⊢ (2 \in ℕ_{0} \land M - j \in ℕ_{0}) \to 2 (M - j) \in ℕ_{0}$
359	76 298 358	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 (M - j) \in ℕ_{0}$
360		expp1	$⊢ (i \in ℂ \land 2 (M - j) \in ℕ_{0}) \to i^{2 (M - j) + 1} = i^{2 (M - j)} i$
361	7 359 360	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$
362	76	a1i	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to 2 \in ℕ_{0}$
363	320 298 362	expmuld	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j)} = {(i^{2})}^{M - j}$
364	168	oveq1i	$⊢ {(i^{2})}^{M - j} = {(- 1)}^{M - j}$
365	363 364	eqtrdi	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{2 (M - j)} = {(- 1)}^{M - j}$
366	365	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$
367	357 361 366	3eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{N - 2 j} = {(- 1)}^{M - j} i$
368		mulcom	$⊢ ({(- 1)}^{M - j} \in ℂ \land i \in ℂ) \to {(- 1)}^{M - j} i = i {(- 1)}^{M - j}$
369	316 7 368	sylancl	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to {(- 1)}^{M - j} i = i {(- 1)}^{M - j}$
370	367 369	eqtrd	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i^{N - 2 j} = i {(- 1)}^{M - j}$
371	345 370	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}$
372		mulcl	$⊢ (i \in ℂ \land {(- 1)}^{M - j} \in ℂ) \to i {(- 1)}^{M - j} \in ℂ$
373	7 316 372	sylancr	$⊢ ((M \in ℕ \land A \in (0, \frac{π}{2})) \land j \in (0 \dots M)) \to i {(- 1)}^{M - j} \in ℂ$
374	373 317	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}$
375	320 316 317	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}$
376	371 374 375	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}$
377	325 376	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}$
378	314 323 377	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}$
379	378	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})$
380		0re	$⊢ 0 \in ℝ$
381		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}$
382	380 310 381	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}$
383	379 382	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}$
384	383	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}$
385	158 288 384	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}$
386	287 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})$
387	306	rpcnd	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to {\tan A}^{- 2} \in ℂ$
388		oveq1	$⊢ t = {\tan A}^{- 2} \to t^{j} = {({\tan A}^{- 2})}^{j}$
389	388	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}$
390	389	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}$
391		sumex	$⊢ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} {({\tan A}^{- 2})}^{j} \in V$
392	390 2 391	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}$
393	387 392	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}$
394	385 386 393	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})$
395	52 59	rerpdivcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\cos N A}{{\sin A}^{N}} \in ℝ$
396	54 59	rerpdivcld	$⊢ (M \in ℕ \land A \in (0, \frac{π}{2})) \to \frac{\sin N A}{{\sin A}^{N}} \in ℝ$
397	395 396	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}}$
398	67 394 397	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