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	21 24 2	wfr2	$⊢ N \in ℕ_{0} \to F (N) = G ({F ↾}_{Pred (< ℕ_{0} N)})$
26	25	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to F (N) = G ({F ↾}_{Pred (< ℕ_{0} N)})$
27		prednn0	$⊢ N \in ℕ_{0} \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$
28	27	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$
29	28	reseq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to {F ↾}_{Pred (< ℕ_{0} N)} = {F ↾}_{(0 \dots N - 1)}$
30	29	fveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to G ({F ↾}_{Pred (< ℕ_{0} N)}) = G ({F ↾}_{(0 \dots N - 1)})$
31	21 24 2	wfrfun	$⊢ Fun F$
32		ovex	$⊢ (0 \dots N - 1) \in V$
33		resfunexg	$⊢ (Fun F \land (0 \dots N - 1) \in V) \to {F ↾}_{(0 \dots N - 1)} \in V$
34	31 32 33	mp2an	$⊢ {F ↾}_{(0 \dots N - 1)} \in V$
35		dmeq	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to dom g = dom ({F ↾}_{(0 \dots N - 1)})$
36	21 24 2	wfr1	$⊢ F Fn ℕ_{0}$
37		fz0ssnn0	$⊢ (0 \dots N - 1) \subseteq ℕ_{0}$
38		fnssres	$⊢ (F Fn ℕ_{0} \land (0 \dots N - 1) \subseteq ℕ_{0}) \to ({F ↾}_{(0 \dots N - 1)}) Fn (0 \dots N - 1)$
39	36 37 38	mp2an	$⊢ ({F ↾}_{(0 \dots N - 1)}) Fn (0 \dots N - 1)$
40	39	fndmi	$⊢ dom ({F ↾}_{(0 \dots N - 1)}) = (0 \dots N - 1)$
41	35 40	eqtrdi	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to dom g = (0 \dots N - 1)$
42		fveq1	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to g (k) = ({F ↾}_{(0 \dots N - 1)}) (k)$
43		fvres	$⊢ k \in (0 \dots N - 1) \to ({F ↾}_{(0 \dots N - 1)}) (k) = F (k)$
44	42 43	sylan9eq	$⊢ (g = {F ↾}_{(0 \dots N - 1)} \land k \in (0 \dots N - 1)) \to g (k) = F (k)$
45	44	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}$
46	45	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})$
47	41 46	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})$
48	47	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})$
49	48	csbeq2dv	$⊢ 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})) = ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}))$
50	41	fveq2d	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to \|dom g\| = \|(0 \dots N - 1)\|$
51	50	csbeq1d	$⊢ g = {F ↾}_{(0 \dots N - 1)} \to ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (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}))$
52	49 51	eqtrd	$⊢ 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}))$
53		ovex	$⊢ X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) \in V$
54	53	csbex	$⊢ ⦋ \|(0 \dots N - 1)\| / n ⦌ (X^{n} - \sum_{k = 0}^{N - 1} (\binom{n}{k}) (\frac{F (k)}{n - k + 1})) \in V$
55	52 1 54	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}))$
56	34 55	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}))$
57		nfcvd	$⊢ N \in ℕ_{0} \to \underline{Ⅎ} n (X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{F (k)}{N - k + 1}))$
58		oveq2	$⊢ n = N \to X^{n} = X^{N}$
59		oveq1	$⊢ n = N \to (\binom{n}{k}) = (\binom{N}{k})$
60		oveq1	$⊢ n = N \to n - k = N - k$
61	60	oveq1d	$⊢ n = N \to n - k + 1 = N - k + 1$
62	61	oveq2d	$⊢ n = N \to \frac{F (k)}{n - k + 1} = \frac{F (k)}{N - k + 1}$
63	59 62	oveq12d	$⊢ n = N \to (\binom{n}{k}) (\frac{F (k)}{n - k + 1}) = (\binom{N}{k}) (\frac{F (k)}{N - k + 1})$
64	63	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})$
65	58 64	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})$
66	57 65	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})$
67	66	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})$
68		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
69		fz01en	$⊢ N \in ℤ \to (0 \dots N - 1) \approx (1 \dots N)$
70	68 69	syl	$⊢ N \in ℕ_{0} \to (0 \dots N - 1) \approx (1 \dots N)$
71		fzfi	$⊢ (0 \dots N - 1) \in Fin$
72		fzfi	$⊢ (1 \dots N) \in Fin$
73		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))$
74	71 72 73	mp2an	$⊢ \|(0 \dots N - 1)\| = \|(1 \dots N)\| \leftrightarrow (0 \dots N - 1) \approx (1 \dots N)$
75	70 74	sylibr	$⊢ N \in ℕ_{0} \to \|(0 \dots N - 1)\| = \|(1 \dots N)\|$
76		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
77	75 76	eqtrd	$⊢ N \in ℕ_{0} \to \|(0 \dots N - 1)\| = N$
78	77	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \|(0 \dots N - 1)\| = N$
79	78	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}))$
80		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
81		simpr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X \in ℂ$
82		fveq2	$⊢ m = k \to F (m) = F (k)$
83	11 82	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)$
84		fvex	$⊢ F (k) \in V$
85	83 14 84	ovmpoa	$⊢ (k \in ℕ_{0} \land X \in ℂ) \to k BernPoly X = F (k)$
86	80 81 85	syl2anr	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to k BernPoly X = F (k)$
87	86	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}$
88	87	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})$
89	88	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})$
90	89	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})$
91	67 79 90	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})$
92	56 91	syl5eq	$⊢ (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})$
93	30 92	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})$
94	16 26 93	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