Theorem bpolysum

Description: A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 22-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	1 2	eleqtrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
4		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
5		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
6	1 4 5	syl2an	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
7	6	nn0cnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
8		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
9		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → 𝑋 ∈ ℂ )
10		bpolycl	⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ )
11	8 9 10	syl2anr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ )
12		fznn0sub	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
13	12	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 )
14		nn0p1nn	⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ0 → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℕ )
15	13 14	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℕ )
16	15	nncnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℂ )
17	15	nnne0d	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ≠ 0 )
18	11 16 17	divcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ )
19	7 18	mulcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
20		oveq2	⊢ ( 𝑘 = 𝑁 → ( 𝑁 C 𝑘 ) = ( 𝑁 C 𝑁 ) )
21		oveq1	⊢ ( 𝑘 = 𝑁 → ( 𝑘 BernPoly 𝑋 ) = ( 𝑁 BernPoly 𝑋 ) )
22		oveq2	⊢ ( 𝑘 = 𝑁 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 𝑁 ) )
23	22	oveq1d	⊢ ( 𝑘 = 𝑁 → ( ( 𝑁 − 𝑘 ) + 1 ) = ( ( 𝑁 − 𝑁 ) + 1 ) )
24	21 23	oveq12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) )
25	20 24	oveq12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( 𝑁 C 𝑁 ) · ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) ) )
26	3 19 25	fsumm1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) + ( ( 𝑁 C 𝑁 ) · ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) ) ) )
27		bcnn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 𝑁 ) = 1 )
28	27	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 C 𝑁 ) = 1 )
29		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
30	29	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → 𝑁 ∈ ℂ )
31	30	subidd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 − 𝑁 ) = 0 )
32	31	oveq1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 − 𝑁 ) + 1 ) = ( 0 + 1 ) )
33		0p1e1	⊢ ( 0 + 1 ) = 1
34	32 33	eqtrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 − 𝑁 ) + 1 ) = 1 )
35	34	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) = ( ( 𝑁 BernPoly 𝑋 ) / 1 ) )
36		bpolycl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ )
37	36	div1d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 BernPoly 𝑋 ) / 1 ) = ( 𝑁 BernPoly 𝑋 ) )
38	35 37	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) = ( 𝑁 BernPoly 𝑋 ) )
39	28 38	oveq12d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 C 𝑁 ) · ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) ) = ( 1 · ( 𝑁 BernPoly 𝑋 ) ) )
40	36	mullidd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 1 · ( 𝑁 BernPoly 𝑋 ) ) = ( 𝑁 BernPoly 𝑋 ) )
41	39 40	eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 C 𝑁 ) · ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) ) = ( 𝑁 BernPoly 𝑋 ) )
42	41	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) + ( ( 𝑁 C 𝑁 ) · ( ( 𝑁 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑁 ) + 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) + ( 𝑁 BernPoly 𝑋 ) ) )
43		bpolyval	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
44	43	eqcomd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( 𝑁 BernPoly 𝑋 ) )
45		expcl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑁 ) ∈ ℂ )
46	45	ancoms	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ↑ 𝑁 ) ∈ ℂ )
47		fzfid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
48		fzssp1	⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) )
49		ax-1cn	⊢ 1 ∈ ℂ
50		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
51	30 49 50	sylancl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
52	51	oveq2d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
53	48 52	sseqtrid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
54	53	sselda	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
55	54 19	syldan	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
56	47 55	fsumcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ )
57	46 56 36	subaddd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( 𝑁 BernPoly 𝑋 ) ↔ ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) + ( 𝑁 BernPoly 𝑋 ) ) = ( 𝑋 ↑ 𝑁 ) ) )
58	44 57	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) + ( 𝑁 BernPoly 𝑋 ) ) = ( 𝑋 ↑ 𝑁 ) )
59	26 42 58	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( 𝑋 ↑ 𝑁 ) )