Theorem bpolycl

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

	Ref	Expression
Assertion	bpolycl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 BernPoly 𝑋 ) = ( 𝑘 BernPoly 𝑋 ) )
2	1	eleq1d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ↔ ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) )
3	2	imbi2d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑋 ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ↔ ( 𝑋 ∈ ℂ → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ) )
4		oveq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 BernPoly 𝑋 ) = ( 𝑁 BernPoly 𝑋 ) )
5	4	eleq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ↔ ( 𝑁 BernPoly 𝑋 ) ∈ ℂ ) )
6	5	imbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑋 ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ↔ ( 𝑋 ∈ ℂ → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ ) ) )
7		r19.21v	⊢ ( ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑋 ∈ ℂ → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ↔ ( 𝑋 ∈ ℂ → ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) )
8		bpolyval	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑛 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( ( 𝑛 C 𝑚 ) · ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) )
9	8	3adant3	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑛 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( ( 𝑛 C 𝑚 ) · ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) )
10		simp2	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → 𝑋 ∈ ℂ )
11		simp1	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → 𝑛 ∈ ℕ0 )
12	10 11	expcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑋 ↑ 𝑛 ) ∈ ℂ )
13		fzfid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 0 ... ( 𝑛 − 1 ) ) ∈ Fin )
14		elfzelz	⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) → 𝑚 ∈ ℤ )
15		bccl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℤ ) → ( 𝑛 C 𝑚 ) ∈ ℕ0 )
16	11 14 15	syl2an	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝑛 C 𝑚 ) ∈ ℕ0 )
17	16	nn0cnd	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝑛 C 𝑚 ) ∈ ℂ )
18		oveq1	⊢ ( 𝑘 = 𝑚 → ( 𝑘 BernPoly 𝑋 ) = ( 𝑚 BernPoly 𝑋 ) )
19	18	eleq1d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ↔ ( 𝑚 BernPoly 𝑋 ) ∈ ℂ ) )
20	19	rspccva	⊢ ( ( ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝑚 BernPoly 𝑋 ) ∈ ℂ )
21	20	3ad2antl3	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( 𝑚 BernPoly 𝑋 ) ∈ ℂ )
22		fzssp1	⊢ ( 0 ... ( 𝑛 − 1 ) ) ⊆ ( 0 ... ( ( 𝑛 − 1 ) + 1 ) )
23	11	nn0cnd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → 𝑛 ∈ ℂ )
24		ax-1cn	⊢ 1 ∈ ℂ
25		npcan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
26	23 24 25	sylancl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
27	26	oveq2d	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 0 ... ( ( 𝑛 − 1 ) + 1 ) ) = ( 0 ... 𝑛 ) )
28	22 27	sseqtrid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 0 ... ( 𝑛 − 1 ) ) ⊆ ( 0 ... 𝑛 ) )
29	28	sselda	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → 𝑚 ∈ ( 0 ... 𝑛 ) )
30		fznn0sub	⊢ ( 𝑚 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑚 ) ∈ ℕ0 )
31		nn0p1nn	⊢ ( ( 𝑛 − 𝑚 ) ∈ ℕ0 → ( ( 𝑛 − 𝑚 ) + 1 ) ∈ ℕ )
32	29 30 31	3syl	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( ( 𝑛 − 𝑚 ) + 1 ) ∈ ℕ )
33	32	nncnd	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( ( 𝑛 − 𝑚 ) + 1 ) ∈ ℂ )
34	32	nnne0d	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( ( 𝑛 − 𝑚 ) + 1 ) ≠ 0 )
35	21 33 34	divcld	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ∈ ℂ )
36	17 35	mulcld	⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ) → ( ( 𝑛 C 𝑚 ) · ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ∈ ℂ )
37	13 36	fsumcl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( ( 𝑛 C 𝑚 ) · ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ∈ ℂ )
38	12 37	subcld	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( ( 𝑛 C 𝑚 ) · ( ( 𝑚 BernPoly 𝑋 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) ∈ ℂ )
39	9 38	eqeltrd	⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ )
40	39	3exp	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑋 ∈ ℂ → ( ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ) )
41	40	a2d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑋 ∈ ℂ → ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑋 ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ) )
42	7 41	biimtrid	⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑋 ∈ ℂ → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑋 ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ) )
43	3 6 42	nn0sinds	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ ℂ → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ ) )
44	43	imp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ )