Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ (๐ฅโ๐) = (๐โ๐)) |
2 | 1 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
3 | 2 | csbeq2dv 3863 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ โฆ(โฏโdom
๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
4 | 3 | mpteq2dv 5208 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) = (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))))) |
5 | | bpoly.1 |
. . . . . . . 8
โข ๐บ = (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) = ๐บ) |
7 | | wrecseq3 8252 |
. . . . . . 7
โข ((๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) = ๐บ โ wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))))) = wrecs( < ,
โ0, ๐บ)) |
8 | 6, 7 | syl 17 |
. . . . . 6
โข (๐ฅ = ๐ โ wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))))) = wrecs( < ,
โ0, ๐บ)) |
9 | | bpoly.2 |
. . . . . 6
โข ๐น = wrecs( < ,
โ0, ๐บ) |
10 | 8, 9 | eqtr4di 2791 |
. . . . 5
โข (๐ฅ = ๐ โ wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))))) = ๐น) |
11 | 10 | fveq1d 6845 |
. . . 4
โข (๐ฅ = ๐ โ (wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐) = (๐นโ๐)) |
12 | | fveq2 6843 |
. . . 4
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
13 | 11, 12 | sylan9eqr 2795 |
. . 3
โข ((๐ = ๐ โง ๐ฅ = ๐) โ (wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐) = (๐นโ๐)) |
14 | | df-bpoly 15935 |
. . 3
โข BernPoly
= (๐ โ
โ0, ๐ฅ
โ โ โฆ (wrecs( < , โ0, (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐)) |
15 | | fvex 6856 |
. . 3
โข (๐นโ๐) โ V |
16 | 13, 14, 15 | ovmpoa 7511 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = (๐นโ๐)) |
17 | | ltweuz 13872 |
. . . . 5
โข < We
(โคโฅโ0) |
18 | | nn0uz 12810 |
. . . . . 6
โข
โ0 = (โคโฅโ0) |
19 | | weeq2 5623 |
. . . . . 6
โข
(โ0 = (โคโฅโ0) โ ( < We
โ0 โ < We
(โคโฅโ0))) |
20 | 18, 19 | ax-mp 5 |
. . . . 5
โข ( < We
โ0 โ < We
(โคโฅโ0)) |
21 | 17, 20 | mpbir 230 |
. . . 4
โข < We
โ0 |
22 | | nn0ex 12424 |
. . . . 5
โข
โ0 โ V |
23 | | exse 5597 |
. . . . 5
โข
(โ0 โ V โ < Se
โ0) |
24 | 22, 23 | ax-mp 5 |
. . . 4
โข < Se
โ0 |
25 | 9 | wfr2 8283 |
. . . 4
โข ((( <
We โ0 โง < Se โ0) โง ๐ โ โ0)
โ (๐นโ๐) = (๐บโ(๐น โพ Pred( < , โ0,
๐)))) |
26 | 21, 24, 25 | mpanl12 701 |
. . 3
โข (๐ โ โ0
โ (๐นโ๐) = (๐บโ(๐น โพ Pred( < , โ0,
๐)))) |
27 | 26 | adantr 482 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐นโ๐) = (๐บโ(๐น โพ Pred( < , โ0,
๐)))) |
28 | | prednn0 13571 |
. . . . . 6
โข (๐ โ โ0
โ Pred( < , โ0, ๐) = (0...(๐ โ 1))) |
29 | 28 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ Pred( < , โ0, ๐) = (0...(๐ โ 1))) |
30 | 29 | reseq2d 5938 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐น โพ Pred(
< , โ0, ๐)) = (๐น โพ (0...(๐ โ 1)))) |
31 | 30 | fveq2d 6847 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐บโ(๐น โพ Pred( < ,
โ0, ๐))) =
(๐บโ(๐น โพ (0...(๐ โ 1))))) |
32 | 9 | wfrfun 8279 |
. . . . . . 7
โข (( <
We โ0 โง < Se โ0) โ Fun ๐น) |
33 | 21, 24, 32 | mp2an 691 |
. . . . . 6
โข Fun ๐น |
34 | | ovex 7391 |
. . . . . 6
โข
(0...(๐ โ 1))
โ V |
35 | | resfunexg 7166 |
. . . . . 6
โข ((Fun
๐น โง (0...(๐ โ 1)) โ V) โ
(๐น โพ (0...(๐ โ 1))) โ
V) |
36 | 33, 34, 35 | mp2an 691 |
. . . . 5
โข (๐น โพ (0...(๐ โ 1))) โ V |
37 | | dmeq 5860 |
. . . . . . . . 9
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ dom ๐ = dom (๐น โพ (0...(๐ โ 1)))) |
38 | 9 | wfr1 8282 |
. . . . . . . . . . . 12
โข (( <
We โ0 โง < Se โ0) โ ๐น Fn
โ0) |
39 | 21, 24, 38 | mp2an 691 |
. . . . . . . . . . 11
โข ๐น Fn
โ0 |
40 | | fz0ssnn0 13542 |
. . . . . . . . . . 11
โข
(0...(๐ โ 1))
โ โ0 |
41 | | fnssres 6625 |
. . . . . . . . . . 11
โข ((๐น Fn โ0 โง
(0...(๐ โ 1)) โ
โ0) โ (๐น โพ (0...(๐ โ 1))) Fn (0...(๐ โ 1))) |
42 | 39, 40, 41 | mp2an 691 |
. . . . . . . . . 10
โข (๐น โพ (0...(๐ โ 1))) Fn (0...(๐ โ 1)) |
43 | 42 | fndmi 6607 |
. . . . . . . . 9
โข dom
(๐น โพ (0...(๐ โ 1))) = (0...(๐ โ 1)) |
44 | 37, 43 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ dom ๐ = (0...(๐ โ 1))) |
45 | 44 | fveq2d 6847 |
. . . . . . 7
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ (โฏโdom
๐) =
(โฏโ(0...(๐
โ 1)))) |
46 | | fveq1 6842 |
. . . . . . . . . . . 12
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ (๐โ๐) = ((๐น โพ (0...(๐ โ 1)))โ๐)) |
47 | | fvres 6862 |
. . . . . . . . . . . 12
โข (๐ โ (0...(๐ โ 1)) โ ((๐น โพ (0...(๐ โ 1)))โ๐) = (๐นโ๐)) |
48 | 46, 47 | sylan9eq 2793 |
. . . . . . . . . . 11
โข ((๐ = (๐น โพ (0...(๐ โ 1))) โง ๐ โ (0...(๐ โ 1))) โ (๐โ๐) = (๐นโ๐)) |
49 | 48 | oveq1d 7373 |
. . . . . . . . . 10
โข ((๐ = (๐น โพ (0...(๐ โ 1))) โง ๐ โ (0...(๐ โ 1))) โ ((๐โ๐) / ((๐ โ ๐) + 1)) = ((๐นโ๐) / ((๐ โ ๐) + 1))) |
50 | 49 | oveq2d 7374 |
. . . . . . . . 9
โข ((๐ = (๐น โพ (0...(๐ โ 1))) โง ๐ โ (0...(๐ โ 1))) โ ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
51 | 44, 50 | sumeq12rdv 15597 |
. . . . . . . 8
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
52 | 51 | oveq2d 7374 |
. . . . . . 7
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
53 | 45, 52 | csbeq12dv 3865 |
. . . . . 6
โข (๐ = (๐น โพ (0...(๐ โ 1))) โ
โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) =
โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
54 | | ovex 7391 |
. . . . . . 7
โข ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) โ V |
55 | 54 | csbex 5269 |
. . . . . 6
โข
โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) โ V |
56 | 53, 5, 55 | fvmpt 6949 |
. . . . 5
โข ((๐น โพ (0...(๐ โ 1))) โ V โ (๐บโ(๐น โพ (0...(๐ โ 1)))) =
โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
57 | 36, 56 | ax-mp 5 |
. . . 4
โข (๐บโ(๐น โพ (0...(๐ โ 1)))) =
โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
58 | | nfcvd 2905 |
. . . . . . 7
โข (๐ โ โ0
โ โฒ๐((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
59 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
60 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
61 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
62 | 61 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ โ ๐) + 1) = ((๐ โ ๐) + 1)) |
63 | 62 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐นโ๐) / ((๐ โ ๐) + 1)) = ((๐นโ๐) / ((๐ โ ๐) + 1))) |
64 | 60, 63 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
65 | 64 | sumeq2sdv 15594 |
. . . . . . . 8
โข (๐ = ๐ โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
66 | 59, 65 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
67 | 58, 66 | csbiegf 3890 |
. . . . . 6
โข (๐ โ โ0
โ โฆ๐ /
๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
68 | 67 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ โฆ๐ /
๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
69 | | nn0z 12529 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ๐ โ
โค) |
70 | | fz01en 13475 |
. . . . . . . . . 10
โข (๐ โ โค โ
(0...(๐ โ 1)) โ
(1...๐)) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
โข (๐ โ โ0
โ (0...(๐ โ 1))
โ (1...๐)) |
72 | | fzfi 13883 |
. . . . . . . . . 10
โข
(0...(๐ โ 1))
โ Fin |
73 | | fzfi 13883 |
. . . . . . . . . 10
โข
(1...๐) โ
Fin |
74 | | hashen 14253 |
. . . . . . . . . 10
โข
(((0...(๐ โ
1)) โ Fin โง (1...๐) โ Fin) โ
((โฏโ(0...(๐
โ 1))) = (โฏโ(1...๐)) โ (0...(๐ โ 1)) โ (1...๐))) |
75 | 72, 73, 74 | mp2an 691 |
. . . . . . . . 9
โข
((โฏโ(0...(๐ โ 1))) = (โฏโ(1...๐)) โ (0...(๐ โ 1)) โ (1...๐)) |
76 | 71, 75 | sylibr 233 |
. . . . . . . 8
โข (๐ โ โ0
โ (โฏโ(0...(๐ โ 1))) = (โฏโ(1...๐))) |
77 | | hashfz1 14252 |
. . . . . . . 8
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
78 | 76, 77 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(0...(๐ โ 1))) = ๐) |
79 | 78 | adantr 482 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ (โฏโ(0...(๐ โ 1))) = ๐) |
80 | 79 | csbeq1d 3860 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) = โฆ๐ / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
81 | | elfznn0 13540 |
. . . . . . . . . 10
โข (๐ โ (0...(๐ โ 1)) โ ๐ โ โ0) |
82 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
83 | | fveq2 6843 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐นโ๐) = (๐นโ๐)) |
84 | 11, 83 | sylan9eqr 2795 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ฅ = ๐) โ (wrecs( < , โ0,
(๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐) = (๐นโ๐)) |
85 | | fvex 6856 |
. . . . . . . . . . 11
โข (๐นโ๐) โ V |
86 | 84, 14, 85 | ovmpoa 7511 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = (๐นโ๐)) |
87 | 81, 82, 86 | syl2anr 598 |
. . . . . . . . 9
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ (๐ BernPoly ๐) = (๐นโ๐)) |
88 | 87 | oveq1d 7373 |
. . . . . . . 8
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)) = ((๐นโ๐) / ((๐ โ ๐) + 1))) |
89 | 88 | oveq2d 7374 |
. . . . . . 7
โข (((๐ โ โ0
โง ๐ โ โ)
โง ๐ โ (0...(๐ โ 1))) โ ((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
90 | 89 | sumeq2dv 15593 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ โ)
โ ฮฃ๐ โ
(0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) |
91 | 90 | oveq2d 7374 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ โ)
โ ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1))))) |
92 | 68, 80, 91 | 3eqtr4d 2783 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ โ)
โ โฆ(โฏโ(0...(๐ โ 1))) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐นโ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
93 | 57, 92 | eqtrid 2785 |
. . 3
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐บโ(๐น โพ (0...(๐ โ 1)))) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
94 | 31, 93 | eqtrd 2773 |
. 2
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐บโ(๐น โพ Pred( < ,
โ0, ๐))) =
((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |
95 | 16, 27, 94 | 3eqtrd 2777 |
1
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |