bpolylem

	Ref	Expression
Hypotheses	bpoly.1	$⊢ G = (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))$
	bpoly.2	$⊢ F = wrecs (< ℕ_{0} G)$
Assertion	bpolylem	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$

Proof

Step	Hyp	Ref	Expression
1		bpoly.1	$⊢ G = (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))$
2		bpoly.2	$⊢ F = wrecs (< ℕ_{0} G)$
3		oveq1	$⊢ x = X \to x^{n} = X^{n}$
4	3	oveq1d	$⊢ x = X \to x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}) = X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
5	4	csbeq2dv	$⊢ x = X \to ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})) = ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))$
6	5	mpteq2dv	$⊢ x = X \to (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))) = (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))$
7	6 1	eqtr4di	$⊢ x = X \to (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))) = G$
8		wrecseq3	$⊢ (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))) = G \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) = wrecs (< ℕ_{0} G)$
9	7 8	syl	$⊢ x = X \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) = wrecs (< ℕ_{0} G)$
10	9 2	eqtr4di	$⊢ x = X \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) = F$
11	10	fveq1d	$⊢ x = X \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) (m) = F (m)$
12		fveq2	$⊢ m = N \to F (m) = F (N)$
13	11 12	sylan9eqr	$⊢ (m = N \land x = X) \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) (m) = F (N)$
14		df-bpoly	$⊢ BernPoly = (m \in ℕ_{0}, x \in ℂ ⟼ wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) (m))$
15		fvex	$⊢ F (N) \in V$
16	13 14 15	ovmpoa	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X = F (N)$
17		ltweuz	$⊢ < We ℤ_{\geq 0}$
18		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
19		weeq2	$⊢ ℕ_{0} = ℤ_{\geq 0} \to (< We ℕ_{0} \leftrightarrow < We ℤ_{\geq 0})$
20	18 19	ax-mp	$⊢ < We ℕ_{0} \leftrightarrow < We ℤ_{\geq 0}$
21	17 20	mpbir	$⊢ < We ℕ_{0}$
22		nn0ex	$⊢ ℕ_{0} \in V$
23		exse	$⊢ ℕ_{0} \in V \to < Se ℕ_{0}$
24	22 23	ax-mp	$⊢ < Se ℕ_{0}$
25	2	wfr2	$⊢ ((< We ℕ_{0} \land < Se ℕ_{0}) \land N \in ℕ_{0}) \to F (N) = G ({F ↾}_{Pred (< ℕ_{0} N)})$
26	21 24 25	mpanl12	$⊢ N \in ℕ_{0} \to F (N) = G ({F ↾}_{Pred (< ℕ_{0} N)})$
27	26	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to F (N) = G ({F ↾}_{Pred (< ℕ_{0} N)})$
28		prednn0	$⊢ N \in ℕ_{0} \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$
29	28	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$
30	29	reseq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to {F ↾}_{Pred (< ℕ_{0} N)} = {F ↾}_{(0 \dots N - 1)}$
31	30	fveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to G ({F ↾}_{Pred (< ℕ_{0} N)}) = G ({F ↾}_{(0 \dots N - 1)})$
32	2	wfrfun	$⊢ (< We ℕ_{0} \land < Se ℕ_{0}) \to Fun F$
33	21 24 32	mp2an	$⊢ Fun F$
34		ovex	$⊢ (0 \dots N - 1) \in V$
35		resfunexg	$⊢ (Fun F \land (0 \dots N - 1) \in V) \to {F ↾}_{(0 \dots N - 1)} \in V$
36	33 34 35	mp2an	$⊢ {F ↾}_{(0 \dots N - 1)} \in V$
37		dmeq	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to dom g = dom ({F ↾}_{(0 \dots N - 1)})$
38	2	wfr1	$⊢ (< We ℕ_{0} \land < Se ℕ_{0}) \to F Fn ℕ_{0}$
39	21 24 38	mp2an	$⊢ F Fn ℕ_{0}$
40		fz0ssnn0	$⊢ (0 \dots N - 1) \subseteq ℕ_{0}$
41		fnssres	$⊢ (F Fn ℕ_{0} \land (0 \dots N - 1) \subseteq ℕ_{0}) \to ({F ↾}_{(0 \dots N - 1)}) Fn (0 \dots N - 1)$
42	39 40 41	mp2an	$⊢ ({F ↾}_{(0 \dots N - 1)}) Fn (0 \dots N - 1)$
43	42	fndmi	$⊢ dom ({F ↾}_{(0 \dots N - 1)}) = (0 \dots N - 1)$
44	37 43	eqtrdi	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to dom g = (0 \dots N - 1)$
45	44	fveq2d	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to \|dom g\| = \|(0 \dots N - 1)\|$
46		fveq1	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to g (k) = ({F ↾}_{(0 \dots N - 1)}) (k)$
47		fvres	$⊢ k \in (0 \dots N - 1) \to ({F ↾}_{(0 \dots N - 1)}) (k) = F (k)$
48	46 47	sylan9eq	$⊢ (g = {F ↾}_{(0 \dots N - 1)} \land k \in (0 \dots N - 1)) \to g (k) = F (k)$
49	48	oveq1d	$⊢ (g = {F ↾}_{(0 \dots N - 1)} \land k \in (0 \dots N - 1)) \to \frac{g (k)}{n - k + 1} = \frac{F (k)}{n - k + 1}$
50	49	oveq2d	$⊢ (g = {F ↾}_{(0 \dots N - 1)} \land k \in (0 \dots N - 1)) \to (\binom{n}{k}) (\frac{g (k)}{n - k + 1}) = (\binom{n}{k}) (\frac{F (k)}{n - k + 1})$
51	44 50	sumeq12rdv	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}) = \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})$
52	51	oveq2d	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}) = X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})$
53	45 52	csbeq12dv	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})) = ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}))$
54		ovex	$⊢ X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) \in V$
55	54	csbex	$⊢ ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) \in V$
56	53 1 55	fvmpt	$⊢ {F ↾}_{(0 \dots N - 1)} \in V \to G ({F ↾}_{(0 \dots N - 1)}) = ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}))$
57	36 56	ax-mp	$⊢ G ({F ↾}_{(0 \dots N - 1)}) = ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}))$
58		nfcvd	$⊢ N \in ℕ_{0} \to \underline{Ⅎ} n (X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1}))$
59		oveq2	$⊢ n = N \to X^{n} = X^{N}$
60		oveq1	$⊢ n = N \to (\binom{n}{k}) = (\binom{N}{k})$
61		oveq1	$⊢ n = N \to n - k = N - k$
62	61	oveq1d	$⊢ n = N \to n - k + 1 = N - k + 1$
63	62	oveq2d	$⊢ n = N \to \frac{F (k)}{n - k + 1} = \frac{F (k)}{N - k + 1}$
64	60 63	oveq12d	$⊢ n = N \to (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) = (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
65	64	sumeq2sdv	$⊢ n = N \to \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) = \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
66	59 65	oveq12d	$⊢ n = N \to X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
67	58 66	csbiegf	$⊢ N \in ℕ_{0} \to ⦋ N / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
68	67	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to ⦋ N / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
69		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
70		fz01en	$⊢ N \in ℤ \to (0 \dots N - 1) \approx (1 \dots N)$
71	69 70	syl	$⊢ N \in ℕ_{0} \to (0 \dots N - 1) \approx (1 \dots N)$
72		fzfi	$⊢ (0 \dots N - 1) \in Fin$
73		fzfi	$⊢ (1 \dots N) \in Fin$
74		hashen	$⊢ ((0 \dots N - 1) \in Fin \land (1 \dots N) \in Fin) \to (\|(0 \dots N - 1)\| = \|(1 \dots N)\| \leftrightarrow (0 \dots N - 1) \approx (1 \dots N))$
75	72 73 74	mp2an	$⊢ \|(0 \dots N - 1)\| = \|(1 \dots N)\| \leftrightarrow (0 \dots N - 1) \approx (1 \dots N)$
76	71 75	sylibr	$⊢ N \in ℕ_{0} \to \|(0 \dots N - 1)\| = \|(1 \dots N)\|$
77		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
78	76 77	eqtrd	$⊢ N \in ℕ_{0} \to \|(0 \dots N - 1)\| = N$
79	78	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \|(0 \dots N - 1)\| = N$
80	79	csbeq1d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) = ⦋ N / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}))$
81		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
82		simpr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X \in ℂ$
83		fveq2	$⊢ m = k \to F (m) = F (k)$
84	11 83	sylan9eqr	$⊢ (m = k \land x = X) \to wrecs (< ℕ_{0} (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (x^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))) (m) = F (k)$
85		fvex	$⊢ F (k) \in V$
86	84 14 85	ovmpoa	$⊢ (k \in ℕ_{0} \land X \in ℂ) \to k BernPoly X = F (k)$
87	81 82 86	syl2anr	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to k BernPoly X = F (k)$
88	87	oveq1d	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to \frac{k BernPoly X}{N - k + 1} = \frac{F (k)}{N - k + 1}$
89	88	oveq2d	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
90	89	sumeq2dv	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
91	90	oveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
92	68 80 91	3eqtr4d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
93	57 92	eqtrid	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to G ({F ↾}_{(0 \dots N - 1)}) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
94	31 93	eqtrd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to G ({F ↾}_{Pred (< ℕ_{0} N)}) = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
95	16 27 94	3eqtrd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$

Metamath Proof Explorer

Theorem bpolylem

Proof