Step |
Hyp |
Ref |
Expression |
1 |
|
0nn0 |
โข 0 โ โ0 |
2 |
|
bpolyval |
โข ( ( 0 โ โ0 โง ๐ โ โ ) โ ( 0 BernPoly ๐ ) = ( ( ๐ โ 0 ) โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) ) |
3 |
1 2
|
mpan |
โข ( ๐ โ โ โ ( 0 BernPoly ๐ ) = ( ( ๐ โ 0 ) โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) ) |
4 |
|
exp0 |
โข ( ๐ โ โ โ ( ๐ โ 0 ) = 1 ) |
5 |
4
|
oveq1d |
โข ( ๐ โ โ โ ( ( ๐ โ 0 ) โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) = ( 1 โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) ) |
6 |
|
risefall0lem |
โข ( 0 ... ( 0 โ 1 ) ) = โ
|
7 |
6
|
sumeq1i |
โข ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) = ฮฃ ๐ โ โ
( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) |
8 |
|
sum0 |
โข ฮฃ ๐ โ โ
( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) = 0 |
9 |
7 8
|
eqtri |
โข ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) = 0 |
10 |
9
|
oveq2i |
โข ( 1 โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) = ( 1 โ 0 ) |
11 |
|
1m0e1 |
โข ( 1 โ 0 ) = 1 |
12 |
10 11
|
eqtri |
โข ( 1 โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) = 1 |
13 |
5 12
|
eqtrdi |
โข ( ๐ โ โ โ ( ( ๐ โ 0 ) โ ฮฃ ๐ โ ( 0 ... ( 0 โ 1 ) ) ( ( 0 C ๐ ) ยท ( ( ๐ BernPoly ๐ ) / ( ( 0 โ ๐ ) + 1 ) ) ) ) = 1 ) |
14 |
3 13
|
eqtrd |
โข ( ๐ โ โ โ ( 0 BernPoly ๐ ) = 1 ) |