Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . 5
โข (๐ = ๐ โ (๐ BernPoly ๐) = (๐ BernPoly ๐)) |
2 | 1 | eleq1d 2819 |
. . . 4
โข (๐ = ๐ โ ((๐ BernPoly ๐) โ โ โ (๐ BernPoly ๐) โ โ)) |
3 | 2 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ BernPoly ๐) โ โ) โ (๐ โ โ โ (๐ BernPoly ๐) โ โ))) |
4 | | oveq1 7365 |
. . . . 5
โข (๐ = ๐ โ (๐ BernPoly ๐) = (๐ BernPoly ๐)) |
5 | 4 | eleq1d 2819 |
. . . 4
โข (๐ = ๐ โ ((๐ BernPoly ๐) โ โ โ (๐ BernPoly ๐) โ โ)) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ โ โ (๐ BernPoly ๐) โ โ) โ (๐ โ โ โ (๐ BernPoly ๐) โ โ))) |
7 | | r19.21v 3173 |
. . . 4
โข
(โ๐ โ
(0...(๐ โ 1))(๐ โ โ โ (๐ BernPoly ๐) โ โ) โ (๐ โ โ โ โ๐ โ (0...(๐ โ 1))(๐ BernPoly ๐) โ โ)) |
8 | | bpolyval 15937 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
9 | 8 | 3adant3 1133 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
10 | | simp2 1138 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ๐ โ โ) |
11 | | simp1 1137 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ๐ โ โ0) |
12 | 10, 11 | expcld 14057 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (๐โ๐) โ โ) |
13 | | fzfid 13884 |
. . . . . . . . 9
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (0...(๐ โ 1)) โ
Fin) |
14 | | elfzelz 13447 |
. . . . . . . . . . . 12
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โค) |
15 | | bccl 14228 |
. . . . . . . . . . . 12
โข ((๐ โ โ0
โง ๐ โ โค)
โ (๐C๐) โ
โ0) |
16 | 11, 14, 15 | syl2an 597 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐C๐) โ
โ0) |
17 | 16 | nn0cnd 12480 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐C๐) โ โ) |
18 | | oveq1 7365 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ (๐ BernPoly ๐) = (๐ BernPoly ๐)) |
19 | 18 | eleq1d 2819 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((๐ BernPoly ๐) โ โ โ (๐ BernPoly ๐) โ โ)) |
20 | 19 | rspccva 3579 |
. . . . . . . . . . . 12
โข
((โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ โง ๐ โ (0...(๐ โ 1))) โ (๐ BernPoly ๐) โ โ) |
21 | 20 | 3ad2antl3 1188 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ (๐ BernPoly ๐) โ โ) |
22 | | fzssp1 13490 |
. . . . . . . . . . . . . . 15
โข
(0...(๐ โ 1))
โ (0...((๐ โ 1)
+ 1)) |
23 | 11 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ๐ โ โ) |
24 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ |
25 | | npcan 11415 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
26 | 23, 24, 25 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ((๐ โ 1) + 1) = ๐) |
27 | 26 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (0...((๐ โ 1) + 1)) = (0...๐)) |
28 | 22, 27 | sseqtrid 3997 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (0...(๐ โ 1)) โ (0...๐)) |
29 | 28 | sselda 3945 |
. . . . . . . . . . . . 13
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ๐ โ (0...๐)) |
30 | | fznn0sub 13479 |
. . . . . . . . . . . . 13
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
31 | | nn0p1nn 12457 |
. . . . . . . . . . . . 13
โข ((๐ โ ๐) โ โ0 โ ((๐ โ ๐) + 1) โ โ) |
32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . 12
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((๐ โ ๐) + 1) โ โ) |
33 | 32 | nncnd 12174 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((๐ โ ๐) + 1) โ โ) |
34 | 32 | nnne0d 12208 |
. . . . . . . . . . 11
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((๐ โ ๐) + 1) โ 0) |
35 | 21, 33, 34 | divcld 11936 |
. . . . . . . . . 10
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) โ โ) |
36 | 17, 35 | mulcld 11180 |
. . . . . . . . 9
โข (((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โง ๐ โ (0...(๐ โ 1))) โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) โ โ) |
37 | 13, 36 | fsumcl 15623 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) โ โ) |
38 | 12, 37 | subcld 11517 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) โ โ) |
39 | 9, 38 | eqeltrd 2834 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ
โง โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (๐ BernPoly ๐) โ โ) |
40 | 39 | 3exp 1120 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ โ
โ (โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ โ (๐ BernPoly ๐) โ โ))) |
41 | 40 | a2d 29 |
. . . 4
โข (๐ โ โ0
โ ((๐ โ โ
โ โ๐ โ
(0...(๐ โ 1))(๐ BernPoly ๐) โ โ) โ (๐ โ โ โ (๐ BernPoly ๐) โ โ))) |
42 | 7, 41 | biimtrid 241 |
. . 3
โข (๐ โ โ0
โ (โ๐ โ
(0...(๐ โ 1))(๐ โ โ โ (๐ BernPoly ๐) โ โ) โ (๐ โ โ โ (๐ BernPoly ๐) โ โ))) |
43 | 3, 6, 42 | nn0sinds 13900 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โ (๐ BernPoly ๐) โ
โ)) |
44 | 43 | imp 408 |
1
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) โ
โ) |