bpolyval

Description: The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014)

		Ref	Expression
	Assertion	bpolyval	$⊢ (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		fvex	$⊢ \|dom c\| \in V$
2		oveq2	$⊢ n = \|dom c\| \to X^{n} = X^{\|dom c\|}$
3		oveq1	$⊢ n = \|dom c\| \to (\binom{n}{m}) = (\binom{\|dom c\|}{m})$
4		oveq1	$⊢ n = \|dom c\| \to n - m = \|dom c\| - m$
5	4	oveq1d	$⊢ n = \|dom c\| \to n - m + 1 = \|dom c\| - m + 1$
6	5	oveq2d	$⊢ n = \|dom c\| \to \frac{c (m)}{n - m + 1} = \frac{c (m)}{\|dom c\| - m + 1}$
7	3 6	oveq12d	$⊢ n = \|dom c\| \to (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})$
8	7	sumeq2sdv	$⊢ n = \|dom c\| \to \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})$
9	2 8	oveq12d	$⊢ n = \|dom c\| \to X^{n} - \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})$
10	1 9	csbie	$⊢ ⦋ \|dom c\| / n ⦌ (X^{n} - \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1})) = X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})$
11		oveq2	$⊢ m = k \to (\binom{n}{m}) = (\binom{n}{k})$
12		fveq2	$⊢ m = k \to c (m) = c (k)$
13		oveq2	$⊢ m = k \to n - m = n - k$
14	13	oveq1d	$⊢ m = k \to n - m + 1 = n - k + 1$
15	12 14	oveq12d	$⊢ m = k \to \frac{c (m)}{n - m + 1} = \frac{c (k)}{n - k + 1}$
16	11 15	oveq12d	$⊢ m = k \to (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = (\binom{n}{k}) (\frac{c (k)}{n - k + 1})$
17	16	cbvsumv	$⊢ \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = \sum_{k \in dom c} (\binom{n}{k}) (\frac{c (k)}{n - k + 1})$
18		dmeq	$⊢ c = g \to dom c = dom g$
19		fveq1	$⊢ c = g \to c (k) = g (k)$
20	19	oveq1d	$⊢ c = g \to \frac{c (k)}{n - k + 1} = \frac{g (k)}{n - k + 1}$
21	20	oveq2d	$⊢ c = g \to (\binom{n}{k}) (\frac{c (k)}{n - k + 1}) = (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
22	21	adantr	$⊢ (c = g \land k \in dom c) \to (\binom{n}{k}) (\frac{c (k)}{n - k + 1}) = (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
23	18 22	sumeq12dv	$⊢ c = g \to \sum_{k \in dom c} (\binom{n}{k}) (\frac{c (k)}{n - k + 1}) = \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
24	17 23	eqtrid	$⊢ c = g \to \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
25	24	oveq2d	$⊢ c = g \to X^{n} - \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1}) = X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})$
26	25	csbeq2dv	$⊢ c = g \to ⦋ \|dom c\| / n ⦌ (X^{n} - \sum_{m \in dom c} (\binom{n}{m}) (\frac{c (m)}{n - m + 1})) = ⦋ \|dom c\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))$
27	10 26	eqtr3id	$⊢ c = g \to X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1}) = ⦋ \|dom c\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))$
28	18	fveq2d	$⊢ c = g \to \|dom c\| = \|dom g\|$
29	28	csbeq1d	$⊢ c = g \to ⦋ \|dom c\| / 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}))$
30	27 29	eqtrd	$⊢ c = g \to X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1}) = ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1}))$
31	30	cbvmptv	$⊢ (c \in V ⟼ X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})) = (g \in V ⟼ ⦋ \|dom g\| / n ⦌ (X^{n} - \sum_{k \in dom g} (\binom{n}{k}) (\frac{g (k)}{n - k + 1})))$
32		eqid	$⊢ wrecs (< ℕ_{0} (c \in V ⟼ X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1}))) = wrecs (< ℕ_{0} (c \in V ⟼ X^{\|dom c\|} - \sum_{m \in dom c} (\binom{\|dom c\|}{m}) (\frac{c (m)}{\|dom c\| - m + 1})))$
33	31 32	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})$

Metamath Proof Explorer

Theorem bpolyval

Proof