Metamath Proof Explorer

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 syl5bi ⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑘 ∈ ( 0 ... ( 𝑛 − 1 ) ) ( 𝑋 ∈ ℂ → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) → ( 𝑋 ∈ ℂ → ( 𝑛 BernPoly 𝑋 ) ∈ ℂ ) ) )
43 3 6 42 nn0sinds ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ ℂ → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ ) )
44 43 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) ∈ ℂ )