Step |
Hyp |
Ref |
Expression |
1 |
|
fvex |
⊢ ( ♯ ‘ dom 𝑐 ) ∈ V |
2 |
|
oveq2 |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑋 ↑ 𝑛 ) = ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) ) |
3 |
|
oveq1 |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑛 C 𝑚 ) = ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) ) |
4 |
|
oveq1 |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( 𝑛 − 𝑚 ) = ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) ) |
5 |
4
|
oveq1d |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑛 − 𝑚 ) + 1 ) = ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) |
6 |
5
|
oveq2d |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) = ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) |
7 |
3 6
|
oveq12d |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) |
8 |
7
|
sumeq2sdv |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) |
9 |
2 8
|
oveq12d |
⊢ ( 𝑛 = ( ♯ ‘ dom 𝑐 ) → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) |
10 |
1 9
|
csbie |
⊢ ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) |
11 |
|
oveq2 |
⊢ ( 𝑚 = 𝑘 → ( 𝑛 C 𝑚 ) = ( 𝑛 C 𝑘 ) ) |
12 |
|
fveq2 |
⊢ ( 𝑚 = 𝑘 → ( 𝑐 ‘ 𝑚 ) = ( 𝑐 ‘ 𝑘 ) ) |
13 |
|
oveq2 |
⊢ ( 𝑚 = 𝑘 → ( 𝑛 − 𝑚 ) = ( 𝑛 − 𝑘 ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝑚 = 𝑘 → ( ( 𝑛 − 𝑚 ) + 1 ) = ( ( 𝑛 − 𝑘 ) + 1 ) ) |
15 |
12 14
|
oveq12d |
⊢ ( 𝑚 = 𝑘 → ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) = ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) |
16 |
11 15
|
oveq12d |
⊢ ( 𝑚 = 𝑘 → ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) |
17 |
16
|
cbvsumv |
⊢ Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑐 ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) |
18 |
|
dmeq |
⊢ ( 𝑐 = 𝑔 → dom 𝑐 = dom 𝑔 ) |
19 |
|
fveq1 |
⊢ ( 𝑐 = 𝑔 → ( 𝑐 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) ) |
20 |
19
|
oveq1d |
⊢ ( 𝑐 = 𝑔 → ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) = ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) |
21 |
20
|
oveq2d |
⊢ ( 𝑐 = 𝑔 → ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) |
22 |
21
|
adantr |
⊢ ( ( 𝑐 = 𝑔 ∧ 𝑘 ∈ dom 𝑐 ) → ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) |
23 |
18 22
|
sumeq12dv |
⊢ ( 𝑐 = 𝑔 → Σ 𝑘 ∈ dom 𝑐 ( ( 𝑛 C 𝑘 ) · ( ( 𝑐 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) |
24 |
17 23
|
syl5eq |
⊢ ( 𝑐 = 𝑔 → Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) = Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) |
25 |
24
|
oveq2d |
⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
26 |
25
|
csbeq2dv |
⊢ ( 𝑐 = 𝑔 → ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑚 ∈ dom 𝑐 ( ( 𝑛 C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( 𝑛 − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
27 |
10 26
|
syl5eqr |
⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
28 |
18
|
fveq2d |
⊢ ( 𝑐 = 𝑔 → ( ♯ ‘ dom 𝑐 ) = ( ♯ ‘ dom 𝑔 ) ) |
29 |
28
|
csbeq1d |
⊢ ( 𝑐 = 𝑔 → ⦋ ( ♯ ‘ dom 𝑐 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
30 |
27 29
|
eqtrd |
⊢ ( 𝑐 = 𝑔 → ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) = ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
31 |
30
|
cbvmptv |
⊢ ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) = ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑋 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) |
32 |
|
eqid |
⊢ wrecs ( < , ℕ0 , ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) ) = wrecs ( < , ℕ0 , ( 𝑐 ∈ V ↦ ( ( 𝑋 ↑ ( ♯ ‘ dom 𝑐 ) ) − Σ 𝑚 ∈ dom 𝑐 ( ( ( ♯ ‘ dom 𝑐 ) C 𝑚 ) · ( ( 𝑐 ‘ 𝑚 ) / ( ( ( ♯ ‘ dom 𝑐 ) − 𝑚 ) + 1 ) ) ) ) ) ) |
33 |
31 32
|
bpolylem |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |