Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . . 6
โข
(โฏโdom ๐) โ V |
2 | | oveq2 7366 |
. . . . . . 7
โข (๐ = (โฏโdom ๐) โ (๐โ๐) = (๐โ(โฏโdom ๐))) |
3 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = (โฏโdom ๐) โ (๐C๐) = ((โฏโdom ๐)C๐)) |
4 | | oveq1 7365 |
. . . . . . . . . . 11
โข (๐ = (โฏโdom ๐) โ (๐ โ ๐) = ((โฏโdom ๐) โ ๐)) |
5 | 4 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = (โฏโdom ๐) โ ((๐ โ ๐) + 1) = (((โฏโdom ๐) โ ๐) + 1)) |
6 | 5 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = (โฏโdom ๐) โ ((๐โ๐) / ((๐ โ ๐) + 1)) = ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1))) |
7 | 3, 6 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = (โฏโdom ๐) โ ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = (((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))) |
8 | 7 | sumeq2sdv 15594 |
. . . . . . 7
โข (๐ = (โฏโdom ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))) |
9 | 2, 8 | oveq12d 7376 |
. . . . . 6
โข (๐ = (โฏโdom ๐) โ ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1))))) |
10 | 1, 9 | csbie 3892 |
. . . . 5
โข
โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))) |
11 | | oveq2 7366 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐C๐) = (๐C๐)) |
12 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
13 | | oveq2 7366 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ ๐) = (๐ โ ๐)) |
14 | 13 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ โ ๐) + 1) = ((๐ โ ๐) + 1)) |
15 | 12, 14 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐โ๐) / ((๐ โ ๐) + 1)) = ((๐โ๐) / ((๐ โ ๐) + 1))) |
16 | 11, 15 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
17 | 16 | cbvsumv 15586 |
. . . . . . . 8
โข
ฮฃ๐ โ dom
๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) |
18 | | dmeq 5860 |
. . . . . . . . 9
โข (๐ = ๐ โ dom ๐ = dom ๐) |
19 | | fveq1 6842 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
20 | 19 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐โ๐) / ((๐ โ ๐) + 1)) = ((๐โ๐) / ((๐ โ ๐) + 1))) |
21 | 20 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
22 | 21 | adantr 482 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ โ dom ๐) โ ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
23 | 18, 22 | sumeq12dv 15596 |
. . . . . . . 8
โข (๐ = ๐ โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
24 | 17, 23 | eqtrid 2785 |
. . . . . . 7
โข (๐ = ๐ โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) = ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
25 | 24 | oveq2d 7374 |
. . . . . 6
โข (๐ = ๐ โ ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
26 | 25 | csbeq2dv 3863 |
. . . . 5
โข (๐ = ๐ โ โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
27 | 10, 26 | eqtr3id 2787 |
. . . 4
โข (๐ = ๐ โ ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))) = โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
28 | 18 | fveq2d 6847 |
. . . . 5
โข (๐ = ๐ โ (โฏโdom ๐) = (โฏโdom ๐)) |
29 | 28 | csbeq1d 3860 |
. . . 4
โข (๐ = ๐ โ โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) = โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
30 | 27, 29 | eqtrd 2773 |
. . 3
โข (๐ = ๐ โ ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))) = โฆ(โฏโdom
๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
31 | 30 | cbvmptv 5219 |
. 2
โข (๐ โ V โฆ ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1))))) = (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐โ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
32 | | eqid 2733 |
. 2
โข wrecs(
< , โ0, (๐ โ V โฆ ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))))) = wrecs( < ,
โ0, (๐
โ V โฆ ((๐โ(โฏโdom ๐)) โ ฮฃ๐ โ dom ๐(((โฏโdom ๐)C๐) ยท ((๐โ๐) / (((โฏโdom ๐) โ ๐) + 1)))))) |
33 | 31, 32 | bpolylem 15936 |
1
โข ((๐ โ โ0
โง ๐ โ โ)
โ (๐ BernPoly ๐) = ((๐โ๐) โ ฮฃ๐ โ (0...(๐ โ 1))((๐C๐) ยท ((๐ BernPoly ๐) / ((๐ โ ๐) + 1))))) |