Theorem bpolyval

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

	Ref	Expression
Assertion	bpolyval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( ♯ ‘ dom 𝑐 ) ∈ V
2		oveq2	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑋 ↑ 𝑛 ) = ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) )
3		oveq1	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑛 C 𝑚 ) = ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) )
4		oveq1	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑛 − 𝑚 ) = ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) )
5	4	oveq1d	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑛 − 𝑚 ) + 1 ) = ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) )
6	5	oveq2d	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) = ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) )
7	3 6	oveq12d	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) )
8	7	sumeq2sdv	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) )
9	2 8	oveq12d	⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) )
10	1 9	csbie	⊢ ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) )
11		oveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑛 C 𝑚 ) = ( 𝑛 C 𝑘 ) )
12		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑐 ‘ 𝑚 ) = ( 𝑐 ‘ 𝑘 ) )
13		oveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑛 − 𝑚 ) = ( 𝑛 − 𝑘 ) )
14	13	oveq1d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑛 − 𝑚 ) + 1 ) = ( ( 𝑛 − 𝑘 ) + 1 ) )
15	12 14	oveq12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) = ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
16	11 15	oveq12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
17	16	cbvsumv	⊢ Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑐 ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
18		dmeq	⊢ ( 𝑐 = 𝑔 → dom 𝑐 = dom 𝑔 )
19		fveq1	⊢ ( 𝑐 = 𝑔 → ( 𝑐 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
20	19	oveq1d	⊢ ( 𝑐 = 𝑔 → ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) = ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
21	20	oveq2d	⊢ ( 𝑐 = 𝑔 → ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
22	21	adantr	⊢ ( ( 𝑐 = 𝑔 ∧ 𝑘 ∈ dom 𝑐 ) → ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
23	18 22	sumeq12dv	⊢ ( 𝑐 = 𝑔 → Σ 𝑘 ∈ dom 𝑐 ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
24	17 23	syl5eq	⊢ ( 𝑐 = 𝑔 → Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
25	24	oveq2d	⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
26	25	csbeq2dv	⊢ ( 𝑐 = 𝑔 → ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
27	10 26	syl5eqr	⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
28	18	fveq2d	⊢ ( 𝑐 = 𝑔 → ( ♯ ‘ dom 𝑐 ) = ( ♯ ‘ dom 𝑔 ) )
29	28	csbeq1d	⊢ ( 𝑐 = 𝑔 → ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
30	27 29	eqtrd	⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
31	30	cbvmptv	⊢ ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) = ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
32		eqid	⊢ wrecs ( < , ℕ0 , ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) ) = wrecs ( < , ℕ0 , ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) )
33	31 32	bpolylem	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )