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