basellem2

Description: Lemma for basel . Show that P is a polynomial of degree M , and compute its coefficient function. (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	basellem2	$⊢ M \in ℕ \to (P \in Poly (ℂ) \land \deg (P) = M \land coeff (P) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - 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		ssidd	$⊢ M \in ℕ \to ℂ \subseteq ℂ$
4		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
5		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
6		oveq2	$⊢ n = j \to 2 n = 2 j$
7	6	oveq2d	$⊢ n = j \to (\binom{N}{2 n}) = (\binom{N}{2 j})$
8		oveq2	$⊢ n = j \to M - n = M - j$
9	8	oveq2d	$⊢ n = j \to {(- 1)}^{M - n} = {(- 1)}^{M - j}$
10	7 9	oveq12d	$⊢ n = j \to (\binom{N}{2 n}) {(- 1)}^{M - n} = (\binom{N}{2 j}) {(- 1)}^{M - j}$
11		eqid	$⊢ (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n})$
12		ovex	$⊢ (\binom{N}{2 j}) {(- 1)}^{M - j} \in V$
13	10 11 12	fvmpt	$⊢ j \in ℕ_{0} \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = (\binom{N}{2 j}) {(- 1)}^{M - j}$
14	5 13	syl	$⊢ j \in (0 \dots M) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = (\binom{N}{2 j}) {(- 1)}^{M - j}$
15	14	adantl	$⊢ (M \in ℕ \land j \in (0 \dots M)) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = (\binom{N}{2 j}) {(- 1)}^{M - j}$
16		2nn	$⊢ 2 \in ℕ$
17		nnmulcl	$⊢ (2 \in ℕ \land M \in ℕ) \to 2 \cdot M \in ℕ$
18	16 17	mpan	$⊢ M \in ℕ \to 2 \cdot M \in ℕ$
19	18	peano2nnd	$⊢ M \in ℕ \to 2 \cdot M + 1 \in ℕ$
20	1 19	eqeltrid	$⊢ M \in ℕ \to N \in ℕ$
21	20	nnnn0d	$⊢ M \in ℕ \to N \in ℕ_{0}$
22		2z	$⊢ 2 \in ℤ$
23		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
24		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
25	22 23 24	sylancr	$⊢ n \in ℕ_{0} \to 2 n \in ℤ$
26		bccl	$⊢ (N \in ℕ_{0} \land 2 n \in ℤ) \to (\binom{N}{2 n}) \in ℕ_{0}$
27	21 25 26	syl2an	$⊢ (M \in ℕ \land n \in ℕ_{0}) \to (\binom{N}{2 n}) \in ℕ_{0}$
28	27	nn0cnd	$⊢ (M \in ℕ \land n \in ℕ_{0}) \to (\binom{N}{2 n}) \in ℂ$
29		neg1cn	$⊢ - 1 \in ℂ$
30		neg1ne0	$⊢ - 1 \neq 0$
31		nnz	$⊢ M \in ℕ \to M \in ℤ$
32		zsubcl	$⊢ (M \in ℤ \land n \in ℤ) \to M - n \in ℤ$
33	31 23 32	syl2an	$⊢ (M \in ℕ \land n \in ℕ_{0}) \to M - n \in ℤ$
34		expclz	$⊢ (- 1 \in ℂ \land - 1 \neq 0 \land M - n \in ℤ) \to {(- 1)}^{M - n} \in ℂ$
35	29 30 33 34	mp3an12i	$⊢ (M \in ℕ \land n \in ℕ_{0}) \to {(- 1)}^{M - n} \in ℂ$
36	28 35	mulcld	$⊢ (M \in ℕ \land n \in ℕ_{0}) \to (\binom{N}{2 n}) {(- 1)}^{M - n} \in ℂ$
37	36	fmpttd	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) : ℕ_{0} ⟶ ℂ$
38		ffvelrn	$⊢ ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) : ℕ_{0} ⟶ ℂ \land j \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \in ℂ$
39	37 5 38	syl2an	$⊢ (M \in ℕ \land j \in (0 \dots M)) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \in ℂ$
40	15 39	eqeltrrd	$⊢ (M \in ℕ \land j \in (0 \dots M)) \to (\binom{N}{2 j}) {(- 1)}^{M - j} \in ℂ$
41	3 4 40	elplyd	$⊢ M \in ℕ \to (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j}) \in Poly (ℂ)$
42	2 41	eqeltrid	$⊢ M \in ℕ \to P \in Poly (ℂ)$
43		nnre	$⊢ M \in ℕ \to M \in ℝ$
44		nn0re	$⊢ j \in ℕ_{0} \to j \in ℝ$
45		ltnle	$⊢ (M \in ℝ \land j \in ℝ) \to (M < j \leftrightarrow \neg j \leq M)$
46	43 44 45	syl2an	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to (M < j \leftrightarrow \neg j \leq M)$
47	13	ad2antlr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = (\binom{N}{2 j}) {(- 1)}^{M - j}$
48	21	ad2antrr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to N \in ℕ_{0}$
49		nn0z	$⊢ j \in ℕ_{0} \to j \in ℤ$
50	49	ad2antlr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to j \in ℤ$
51		zmulcl	$⊢ (2 \in ℤ \land j \in ℤ) \to 2 j \in ℤ$
52	22 50 51	sylancr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 j \in ℤ$
53		ax-1cn	$⊢ 1 \in ℂ$
54	53	2timesi	$⊢ 2 \cdot 1 = 1 + 1$
55	54	oveq2i	$⊢ 2 \cdot M + 2 \cdot 1 = 2 \cdot M + 1 + 1$
56		2cnd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 \in ℂ$
57		nncn	$⊢ M \in ℕ \to M \in ℂ$
58	57	ad2antrr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to M \in ℂ$
59	53	a1i	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 1 \in ℂ$
60	56 58 59	adddid	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 (M + 1) = 2 \cdot M + 2 \cdot 1$
61	1	oveq1i	$⊢ N + 1 = 2 \cdot M + 1 + 1$
62	18	ad2antrr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 \cdot M \in ℕ$
63	62	nncnd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 \cdot M \in ℂ$
64	63 59 59	addassd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 \cdot M + 1 + 1 = 2 \cdot M + 1 + 1$
65	61 64	syl5eq	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to N + 1 = 2 \cdot M + 1 + 1$
66	55 60 65	3eqtr4a	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 (M + 1) = N + 1$
67		zltp1le	$⊢ (M \in ℤ \land j \in ℤ) \to (M < j \leftrightarrow M + 1 \leq j)$
68	31 49 67	syl2an	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to (M < j \leftrightarrow M + 1 \leq j)$
69	68	biimpa	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to M + 1 \leq j$
70	43	ad2antrr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to M \in ℝ$
71		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
72	70 71	syl	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to M + 1 \in ℝ$
73	44	ad2antlr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to j \in ℝ$
74		2re	$⊢ 2 \in ℝ$
75		2pos	$⊢ 0 < 2$
76	74 75	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
77	76	a1i	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (2 \in ℝ \land 0 < 2)$
78		lemul2	$⊢ (M + 1 \in ℝ \land j \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (M + 1 \leq j \leftrightarrow 2 (M + 1) \leq 2 j)$
79	72 73 77 78	syl3anc	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (M + 1 \leq j \leftrightarrow 2 (M + 1) \leq 2 j)$
80	69 79	mpbid	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 2 (M + 1) \leq 2 j$
81	66 80	eqbrtrrd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to N + 1 \leq 2 j$
82	20	nnzd	$⊢ M \in ℕ \to N \in ℤ$
83	82	ad2antrr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to N \in ℤ$
84		zltp1le	$⊢ (N \in ℤ \land 2 j \in ℤ) \to (N < 2 j \leftrightarrow N + 1 \leq 2 j)$
85	83 52 84	syl2anc	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (N < 2 j \leftrightarrow N + 1 \leq 2 j)$
86	81 85	mpbird	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to N < 2 j$
87	86	olcd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (2 j < 0 \lor N < 2 j)$
88		bcval4	$⊢ (N \in ℕ_{0} \land 2 j \in ℤ \land (2 j < 0 \lor N < 2 j)) \to (\binom{N}{2 j}) = 0$
89	48 52 87 88	syl3anc	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (\binom{N}{2 j}) = 0$
90	89	oveq1d	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (\binom{N}{2 j}) {(- 1)}^{M - j} = 0 \cdot {(- 1)}^{M - j}$
91		zsubcl	$⊢ (M \in ℤ \land j \in ℤ) \to M - j \in ℤ$
92	31 49 91	syl2an	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to M - j \in ℤ$
93		expclz	$⊢ (- 1 \in ℂ \land - 1 \neq 0 \land M - j \in ℤ) \to {(- 1)}^{M - j} \in ℂ$
94	29 30 92 93	mp3an12i	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to {(- 1)}^{M - j} \in ℂ$
95	94	adantr	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to {(- 1)}^{M - j} \in ℂ$
96	95	mul02d	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to 0 \cdot {(- 1)}^{M - j} = 0$
97	47 90 96	3eqtrd	$⊢ ((M \in ℕ \land j \in ℕ_{0}) \land M < j) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = 0$
98	97	ex	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to (M < j \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = 0)$
99	46 98	sylbird	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to (\neg j \leq M \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) = 0)$
100	99	necon1ad	$⊢ (M \in ℕ \land j \in ℕ_{0}) \to ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \neq 0 \to j \leq M)$
101	100	ralrimiva	$⊢ M \in ℕ \to \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \neq 0 \to j \leq M)$
102		plyco0	$⊢ (M \in ℕ_{0} \land (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) : ℕ_{0} ⟶ ℂ) \to ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \neq 0 \to j \leq M))$
103	4 37 102	syl2anc	$⊢ M \in ℕ \to ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) [ℤ_{\geq (M + 1)}] = \{0\} \leftrightarrow \forall j \in ℕ_{0} ((n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) \neq 0 \to j \leq M))$
104	101 103	mpbird	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) [ℤ_{\geq (M + 1)}] = \{0\}$
105	14	oveq1d	$⊢ j \in (0 \dots M) \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) t^{j} = (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j}$
106	105	sumeq2i	$⊢ \sum_{j = 0}^{M} (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) t^{j} = \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j}$
107	106	mpteq2i	$⊢ (t \in ℂ ⟼ \sum_{j = 0}^{M} (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) t^{j}) = (t \in ℂ ⟼ \sum_{j = 0}^{M} (\binom{N}{2 j}) {(- 1)}^{M - j} t^{j})$
108	2 107	eqtr4i	$⊢ P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) t^{j})$
109	108	a1i	$⊢ M \in ℕ \to P = (t \in ℂ ⟼ \sum_{j = 0}^{M} (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (j) t^{j})$
110		oveq2	$⊢ n = M \to 2 n = 2 \cdot M$
111	110	oveq2d	$⊢ n = M \to (\binom{N}{2 n}) = (\binom{N}{2 \cdot M})$
112		oveq2	$⊢ n = M \to M - n = M - M$
113	112	oveq2d	$⊢ n = M \to {(- 1)}^{M - n} = {(- 1)}^{M - M}$
114	111 113	oveq12d	$⊢ n = M \to (\binom{N}{2 n}) {(- 1)}^{M - n} = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
115		ovex	$⊢ (\binom{N}{2 \cdot M}) {(- 1)}^{M - M} \in V$
116	114 11 115	fvmpt	$⊢ M \in ℕ_{0} \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
117	4 116	syl	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) = (\binom{N}{2 \cdot M}) {(- 1)}^{M - M}$
118	57	subidd	$⊢ M \in ℕ \to M - M = 0$
119	118	oveq2d	$⊢ M \in ℕ \to {(- 1)}^{M - M} = {(- 1)}^{0}$
120		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
121	29 120	ax-mp	$⊢ {(- 1)}^{0} = 1$
122	119 121	eqtrdi	$⊢ M \in ℕ \to {(- 1)}^{M - M} = 1$
123	122	oveq2d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) {(- 1)}^{M - M} = (\binom{N}{2 \cdot M}) \cdot 1$
124	18	nnred	$⊢ M \in ℕ \to 2 \cdot M \in ℝ$
125	124	lep1d	$⊢ M \in ℕ \to 2 \cdot M \leq 2 \cdot M + 1$
126	125 1	breqtrrdi	$⊢ M \in ℕ \to 2 \cdot M \leq N$
127	18	nnnn0d	$⊢ M \in ℕ \to 2 \cdot M \in ℕ_{0}$
128		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
129	127 128	eleqtrdi	$⊢ M \in ℕ \to 2 \cdot M \in ℤ_{\geq 0}$
130		elfz5	$⊢ (2 \cdot M \in ℤ_{\geq 0} \land N \in ℤ) \to (2 \cdot M \in (0 \dots N) \leftrightarrow 2 \cdot M \leq N)$
131	129 82 130	syl2anc	$⊢ M \in ℕ \to (2 \cdot M \in (0 \dots N) \leftrightarrow 2 \cdot M \leq N)$
132	126 131	mpbird	$⊢ M \in ℕ \to 2 \cdot M \in (0 \dots N)$
133		bccl2	$⊢ 2 \cdot M \in (0 \dots N) \to (\binom{N}{2 \cdot M}) \in ℕ$
134	132 133	syl	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \in ℕ$
135	134	nncnd	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \in ℂ$
136	135	mulid1d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \cdot 1 = (\binom{N}{2 \cdot M})$
137	117 123 136	3eqtrd	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) = (\binom{N}{2 \cdot M})$
138	134	nnne0d	$⊢ M \in ℕ \to (\binom{N}{2 \cdot M}) \neq 0$
139	137 138	eqnetrd	$⊢ M \in ℕ \to (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}) (M) \neq 0$
140	42 4 37 104 109 139	dgreq	$⊢ M \in ℕ \to \deg (P) = M$
141	42 4 37 104 109	coeeq	$⊢ M \in ℕ \to coeff (P) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n})$
142	42 140 141	3jca	$⊢ M \in ℕ \to (P \in Poly (ℂ) \land \deg (P) = M \land coeff (P) = (n \in ℕ_{0} ⟼ (\binom{N}{2 n}) {(- 1)}^{M - n}))$

Metamath Proof Explorer

Theorem basellem2

Proof