Step | Hyp | Ref
| Expression |
1 | | 1nn0 12434 |
. . 3
โข 1 โ
โ0 |
2 | | bpolyval 15937 |
. . 3
โข ((1
โ โ0 โง ๐ โ โ) โ (1 BernPoly ๐) = ((๐โ1) โ ฮฃ๐ โ (0...(1 โ 1))((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))))) |
3 | 1, 2 | mpan 689 |
. 2
โข (๐ โ โ โ (1
BernPoly ๐) = ((๐โ1) โ ฮฃ๐ โ (0...(1 โ
1))((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))))) |
4 | | exp1 13979 |
. . 3
โข (๐ โ โ โ (๐โ1) = ๐) |
5 | | 1m1e0 12230 |
. . . . . 6
โข (1
โ 1) = 0 |
6 | 5 | oveq2i 7369 |
. . . . 5
โข (0...(1
โ 1)) = (0...0) |
7 | 6 | sumeq1i 15588 |
. . . 4
โข
ฮฃ๐ โ
(0...(1 โ 1))((1C๐)
ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = ฮฃ๐ โ (0...0)((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))) |
8 | | 0z 12515 |
. . . . . 6
โข 0 โ
โค |
9 | | bpoly0 15938 |
. . . . . . . . . 10
โข (๐ โ โ โ (0
BernPoly ๐) =
1) |
10 | 9 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ โ โ ((0
BernPoly ๐) / 2) = (1 /
2)) |
11 | 10 | oveq2d 7374 |
. . . . . . . 8
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
2)) = (1 ยท (1 / 2))) |
12 | | halfcn 12373 |
. . . . . . . . 9
โข (1 / 2)
โ โ |
13 | 12 | mulid2i 11165 |
. . . . . . . 8
โข (1
ยท (1 / 2)) = (1 / 2) |
14 | 11, 13 | eqtrdi 2789 |
. . . . . . 7
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
2)) = (1 / 2)) |
15 | 14, 12 | eqeltrdi 2842 |
. . . . . 6
โข (๐ โ โ โ (1
ยท ((0 BernPoly ๐) /
2)) โ โ) |
16 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = 0 โ (1C๐) = (1C0)) |
17 | | bcn0 14216 |
. . . . . . . . . 10
โข (1 โ
โ0 โ (1C0) = 1) |
18 | 1, 17 | ax-mp 5 |
. . . . . . . . 9
โข (1C0) =
1 |
19 | 16, 18 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = 0 โ (1C๐) = 1) |
20 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ BernPoly ๐) = (0 BernPoly ๐)) |
21 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (1 โ ๐) = (1 โ
0)) |
22 | | 1m0e1 12279 |
. . . . . . . . . . . 12
โข (1
โ 0) = 1 |
23 | 21, 22 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ = 0 โ (1 โ ๐) = 1) |
24 | 23 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = 0 โ ((1 โ ๐) + 1) = (1 +
1)) |
25 | | df-2 12221 |
. . . . . . . . . 10
โข 2 = (1 +
1) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . . . 9
โข (๐ = 0 โ ((1 โ ๐) + 1) = 2) |
27 | 20, 26 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = 0 โ ((๐ BernPoly ๐) / ((1 โ ๐) + 1)) = ((0 BernPoly ๐) / 2)) |
28 | 19, 27 | oveq12d 7376 |
. . . . . . 7
โข (๐ = 0 โ ((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 2))) |
29 | 28 | fsum1 15637 |
. . . . . 6
โข ((0
โ โค โง (1 ยท ((0 BernPoly ๐) / 2)) โ โ) โ ฮฃ๐ โ (0...0)((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = (1 ยท ((0 BernPoly ๐) / 2))) |
30 | 8, 15, 29 | sylancr 588 |
. . . . 5
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((1C๐) ยท
((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = (1 ยท ((0
BernPoly ๐) /
2))) |
31 | 30, 14 | eqtrd 2773 |
. . . 4
โข (๐ โ โ โ
ฮฃ๐ โ
(0...0)((1C๐) ยท
((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = (1 /
2)) |
32 | 7, 31 | eqtrid 2785 |
. . 3
โข (๐ โ โ โ
ฮฃ๐ โ (0...(1
โ 1))((1C๐) ยท
((๐ BernPoly ๐) / ((1 โ ๐) + 1))) = (1 /
2)) |
33 | 4, 32 | oveq12d 7376 |
. 2
โข (๐ โ โ โ ((๐โ1) โ ฮฃ๐ โ (0...(1 โ
1))((1C๐) ยท ((๐ BernPoly ๐) / ((1 โ ๐) + 1)))) = (๐ โ (1 / 2))) |
34 | 3, 33 | eqtrd 2773 |
1
โข (๐ โ โ โ (1
BernPoly ๐) = (๐ โ (1 /
2))) |