Metamath Proof Explorer

Theorem bpolylem

Description: Lemma for bpolyval . (Contributed by Scott Fenton, 22-May-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses bpoly.1 ⊢ 𝐺 = ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
bpoly.2 ⊢ 𝐹 = wrecs ( < , ℕ0 , 𝐺 )
Assertion bpolylem ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 bpoly.1 ⊢ 𝐺 = ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
2 bpoly.2 ⊢ 𝐹 = wrecs ( < , ℕ0 , 𝐺 )
3 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ↑ 𝑛 ) = ( 𝑋 ↑ 𝑛 ) )
4 3 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
5 4 csbeq2dv ⊢ ( 𝑥 = 𝑋 → ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
6 5 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) = ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) )
7 6 1 eqtr4di ⊢ ( 𝑥 = 𝑋 → ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) = 𝐺 )
8 wrecseq3 ⊢ ( ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) = 𝐺 → wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) = wrecs ( < , ℕ0 , 𝐺 ) )
9 7 8 syl ⊢ ( 𝑥 = 𝑋 → wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) = wrecs ( < , ℕ0 , 𝐺 ) )
10 9 2 eqtr4di ⊢ ( 𝑥 = 𝑋 → wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) = 𝐹 )
11 10 fveq1d ⊢ ( 𝑥 = 𝑋 → ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
12 fveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑁 ) )
13 11 12 sylan9eqr ⊢ ( ( 𝑚 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑁 ) )
14 df-bpoly ⊢ BernPoly = ( 𝑚 ∈ ℕ0 , 𝑥 ∈ ℂ ↦ ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) )
15 fvex ⊢ ( 𝐹 ‘ 𝑁 ) ∈ V
16 13 14 15 ovmpoa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( 𝐹 ‘ 𝑁 ) )
17 ltweuz ⊢ < We ( ℤ≥ ‘ 0 )
18 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
19 weeq2 ⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → ( < We ℕ0 ↔ < We ( ℤ≥ ‘ 0 ) ) )
20 18 19 ax-mp ⊢ ( < We ℕ0 ↔ < We ( ℤ≥ ‘ 0 ) )
21 17 20 mpbir ⊢ < We ℕ0
22 nn0ex ⊢ ℕ0 ∈ V
23 exse ⊢ ( ℕ0 ∈ V → < Se ℕ0 )
24 22 23 ax-mp ⊢ < Se ℕ0
25 2 wfr2 ⊢ ( ( ( < We ℕ0 ∧ < Se ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑁 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) ) )
26 21 24 25 mpanl12 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 ‘ 𝑁 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) ) )
27 26 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ‘ 𝑁 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) ) )
28 prednn0 ⊢ ( 𝑁 ∈ ℕ0 → Pred ( < , ℕ0 , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
29 28 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → Pred ( < , ℕ0 , 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
30 29 reseq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) )
31 30 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝐺 ‘ ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) ) = ( 𝐺 ‘ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ) )
32 2 wfrfun ⊢ ( ( < We ℕ0 ∧ < Se ℕ0 ) → Fun 𝐹 )
33 21 24 32 mp2an ⊢ Fun 𝐹
34 ovex ⊢ ( 0 ... ( 𝑁 − 1 ) ) ∈ V
35 resfunexg ⊢ ( ( Fun 𝐹 ∧ ( 0 ... ( 𝑁 − 1 ) ) ∈ V ) → ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∈ V )
36 33 34 35 mp2an ⊢ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∈ V
37 dmeq ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → dom 𝑔 = dom ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) )
38 2 wfr1 ⊢ ( ( < We ℕ0 ∧ < Se ℕ0 ) → 𝐹 Fn ℕ0 )
39 21 24 38 mp2an ⊢ 𝐹 Fn ℕ0
40 fz0ssnn0 ⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ℕ0
41 fnssres ⊢ ( ( 𝐹 Fn ℕ0 ∧ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ℕ0 ) → ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) Fn ( 0 ... ( 𝑁 − 1 ) ) )
42 39 40 41 mp2an ⊢ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) Fn ( 0 ... ( 𝑁 − 1 ) )
43 42 fndmi ⊢ dom ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) = ( 0 ... ( 𝑁 − 1 ) )
44 37 43 eqtrdi ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → dom 𝑔 = ( 0 ... ( 𝑁 − 1 ) ) )
45 44 fveq2d ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ♯ ‘ dom 𝑔 ) = ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) )
46 fveq1 ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ‘ 𝑘 ) )
47 fvres ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
48 46 47 sylan9eq ⊢ ( ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑔 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
49 48 oveq1d ⊢ ( ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
50 49 oveq2d ⊢ ( ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
51 44 50 sumeq12rdv ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
52 51 oveq2d ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
53 45 52 csbeq12dv ⊢ ( 𝑔 = ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) → ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
54 ovex ⊢ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ∈ V
55 54 csbex ⊢ ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ∈ V
56 53 1 55 fvmpt ⊢ ( ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ∈ V → ( 𝐺 ‘ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ) = ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
57 36 56 ax-mp ⊢ ( 𝐺 ‘ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ) = ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
58 nfcvd ⊢ ( 𝑁 ∈ ℕ0 → Ⅎ 𝑛 ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
59 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑋 ↑ 𝑛 ) = ( 𝑋 ↑ 𝑁 ) )
60 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
61 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 𝑘 ) = ( 𝑁 − 𝑘 ) )
62 61 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 − 𝑘 ) + 1 ) = ( ( 𝑁 − 𝑘 ) + 1 ) )
63 62 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) )
64 60 63 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) )
65 64 sumeq2sdv ⊢ ( 𝑛 = 𝑁 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) )
66 59 65 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
67 58 66 csbiegf ⊢ ( 𝑁 ∈ ℕ0 → ⦋ 𝑁 / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
68 67 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ⦋ 𝑁 / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
69 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
70 fz01en ⊢ ( 𝑁 ∈ ℤ → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) )
71 69 70 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) )
72 fzfi ⊢ ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin
73 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
74 hashen ⊢ ( ( ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) ) )
75 72 73 74 mp2an ⊢ ( ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ ( 0 ... ( 𝑁 − 1 ) ) ≈ ( 1 ... 𝑁 ) )
76 71 75 sylibr ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
77 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
78 76 77 eqtrd ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = 𝑁 )
79 78 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) = 𝑁 )
80 79 csbeq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ⦋ 𝑁 / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
81 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
82 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → 𝑋 ∈ ℂ )
83 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
84 11 83 sylan9eqr ⊢ ( ( 𝑚 = 𝑘 ∧ 𝑥 = 𝑋 ) → ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
85 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
86 84 14 85 ovmpoa ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑘 BernPoly 𝑋 ) = ( 𝐹 ‘ 𝑘 ) )
87 81 82 86 syl2anr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 BernPoly 𝑋 ) = ( 𝐹 ‘ 𝑘 ) )
88 87 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) )
89 88 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) )
90 89 sumeq2dv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) )
91 90 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
92 68 80 91 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ⦋ ( ♯ ‘ ( 0 ... ( 𝑁 − 1 ) ) ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐹 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
93 57 92 eqtrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝐺 ‘ ( 𝐹 ↾ ( 0 ... ( 𝑁 − 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
94 31 93 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝐺 ‘ ( 𝐹 ↾ Pred ( < , ℕ0 , 𝑁 ) ) ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )
95 16 27 94 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) )