Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ0) |
2 | | nn0uz 12810 |
. . . 4
โข
โ0 = (โคโฅโ0) |
3 | 1, 2 | eleqtrdi 2844 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
(โคโฅโ0)) |
4 | | elfzelz 13447 |
. . . . . 6
โข (๐ โ (0...๐) โ ๐ โ โค) |
5 | | bccl 14228 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
6 | 1, 4, 5 | syl2an 597 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ (๐C๐) โ
โ0) |
7 | 6 | nn0cnd 12480 |
. . . 4
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
8 | | elfznn0 13540 |
. . . . . 6
โข (๐ โ (0...๐) โ ๐ โ โ0) |
9 | | simpr 486 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
10 | | bpolycl 15940 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) โ
โ) |
11 | 8, 9, 10 | syl2anr 598 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ (๐ BernPoly ๐) โ โ) |
12 | | fznn0sub 13479 |
. . . . . . . 8
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
13 | 12 | adantl 483 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ (๐ โ ๐) โ
โ0) |
14 | | nn0p1nn 12457 |
. . . . . . 7
โข ((๐ โ ๐) โ โ0 โ ((๐ โ ๐) + 1) โ โ) |
15 | 13, 14 | syl 17 |
. . . . . 6
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ ((๐ โ ๐) + 1) โ โ) |
16 | 15 | nncnd 12174 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ ((๐ โ ๐) + 1) โ โ) |
17 | 15 | nnne0d 12208 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ ((๐ โ ๐) + 1) โ 0) |
18 | 11, 16, 17 | divcld 11936 |
. . . 4
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) โ โ) |
19 | 7, 18 | mulcld 11180 |
. . 3
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) โ โ) |
20 | | oveq2 7366 |
. . . 4
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
21 | | oveq1 7365 |
. . . . 5
โข (๐ = ๐ โ (๐ BernPoly ๐) = (๐ BernPoly ๐)) |
22 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
23 | 22 | oveq1d 7373 |
. . . . 5
โข (๐ = ๐ โ ((๐ โ ๐) + 1) = ((๐ โ ๐) + 1)) |
24 | 21, 23 | oveq12d 7376 |
. . . 4
โข (๐ = ๐ โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) = ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) |
25 | 20, 24 | oveq12d 7376 |
. . 3
โข (๐ = ๐ โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) |
26 | 3, 19, 25 | fsumm1 15641 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...๐)((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) + ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
27 | | bcnn 14218 |
. . . . . 6
โข (๐ โ โ0
โ (๐C๐) = 1) |
28 | 27 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐C๐) = 1) |
29 | | nn0cn 12428 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
31 | 30 | subidd 11505 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ โ ๐) = 0) |
32 | 31 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ ๐) + 1) = (0 +
1)) |
33 | | 0p1e1 12280 |
. . . . . . . 8
โข (0 + 1) =
1 |
34 | 32, 33 | eqtrdi 2789 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ ๐) + 1) = 1) |
35 | 34 | oveq2d 7374 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) = ((๐ BernPoly ๐) / 1)) |
36 | | bpolycl 15940 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) โ
โ) |
37 | 36 | div1d 11928 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ BernPoly ๐) / 1) = (๐ BernPoly ๐)) |
38 | 35, 37 | eqtrd 2773 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) = (๐ BernPoly ๐)) |
39 | 28, 38 | oveq12d 7376 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = (1 ยท (๐ BernPoly ๐))) |
40 | 36 | mulid2d 11178 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ (1 ยท (๐
BernPoly ๐)) = (๐ BernPoly ๐)) |
41 | 39, 40 | eqtrd 2773 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = (๐ BernPoly ๐)) |
42 | 41 | oveq2d 7374 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ (ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) + ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) = (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) + (๐ BernPoly ๐))) |
43 | | bpolyval 15937 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
44 | 43 | eqcomd 2739 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) = (๐ BernPoly ๐)) |
45 | | expcl 13991 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐โ๐) โ
โ) |
46 | 45 | ancoms 460 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐โ๐) โ
โ) |
47 | | fzfid 13884 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ (0...(๐ โ 1))
โ Fin) |
48 | | fzssp1 13490 |
. . . . . . . 8
โข
(0...(๐ โ 1))
โ (0...((๐ โ 1)
+ 1)) |
49 | | ax-1cn 11114 |
. . . . . . . . . 10
โข 1 โ
โ |
50 | | npcan 11415 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
51 | 30, 49, 50 | sylancl 587 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐ โ 1) + 1)
= ๐) |
52 | 51 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (0...((๐ โ 1)
+ 1)) = (0...๐)) |
53 | 48, 52 | sseqtrid 3997 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ)
โ (0...(๐ โ 1))
โ (0...๐)) |
54 | 53 | sselda 3945 |
. . . . . 6
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ๐ โ (0...๐)) |
55 | 54, 19 | syldan 592 |
. . . . 5
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) โ โ) |
56 | 47, 55 | fsumcl 15623 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) โ โ) |
57 | 46, 56, 36 | subaddd 11535 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ (((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) = (๐ BernPoly ๐) โ (ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) + (๐ BernPoly ๐)) = (๐โ๐))) |
58 | 44, 57 | mpbid 231 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ (ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) + (๐ BernPoly ๐)) = (๐โ๐)) |
59 | 26, 42, 58 | 3eqtrd 2777 |
1
โข ((๐ โ โ0
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...๐)((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = (๐โ๐)) |