Step | Hyp | Ref
| Expression |
1 | | cbp 15934 |
. 2
class
BernPoly |
2 | | vm |
. . 3
setvar ๐ |
3 | | vx |
. . 3
setvar ๐ฅ |
4 | | cn0 12418 |
. . 3
class
โ0 |
5 | | cc 11054 |
. . 3
class
โ |
6 | 2 | cv 1541 |
. . . 4
class ๐ |
7 | | clt 11194 |
. . . . 5
class
< |
8 | | vg |
. . . . . 6
setvar ๐ |
9 | | cvv 3444 |
. . . . . 6
class
V |
10 | | vn |
. . . . . . 7
setvar ๐ |
11 | 8 | cv 1541 |
. . . . . . . . 9
class ๐ |
12 | 11 | cdm 5634 |
. . . . . . . 8
class dom ๐ |
13 | | chash 14236 |
. . . . . . . 8
class
โฏ |
14 | 12, 13 | cfv 6497 |
. . . . . . 7
class
(โฏโdom ๐) |
15 | 3 | cv 1541 |
. . . . . . . . 9
class ๐ฅ |
16 | 10 | cv 1541 |
. . . . . . . . 9
class ๐ |
17 | | cexp 13973 |
. . . . . . . . 9
class
โ |
18 | 15, 16, 17 | co 7358 |
. . . . . . . 8
class (๐ฅโ๐) |
19 | | vk |
. . . . . . . . . . . 12
setvar ๐ |
20 | 19 | cv 1541 |
. . . . . . . . . . 11
class ๐ |
21 | | cbc 14208 |
. . . . . . . . . . 11
class
C |
22 | 16, 20, 21 | co 7358 |
. . . . . . . . . 10
class (๐C๐) |
23 | 20, 11 | cfv 6497 |
. . . . . . . . . . 11
class (๐โ๐) |
24 | | cmin 11390 |
. . . . . . . . . . . . 13
class
โ |
25 | 16, 20, 24 | co 7358 |
. . . . . . . . . . . 12
class (๐ โ ๐) |
26 | | c1 11057 |
. . . . . . . . . . . 12
class
1 |
27 | | caddc 11059 |
. . . . . . . . . . . 12
class
+ |
28 | 25, 26, 27 | co 7358 |
. . . . . . . . . . 11
class ((๐ โ ๐) + 1) |
29 | | cdiv 11817 |
. . . . . . . . . . 11
class
/ |
30 | 23, 28, 29 | co 7358 |
. . . . . . . . . 10
class ((๐โ๐) / ((๐ โ ๐) + 1)) |
31 | | cmul 11061 |
. . . . . . . . . 10
class
ยท |
32 | 22, 30, 31 | co 7358 |
. . . . . . . . 9
class ((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) |
33 | 12, 32, 19 | csu 15576 |
. . . . . . . 8
class
ฮฃ๐ โ dom
๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))) |
34 | 18, 33, 24 | co 7358 |
. . . . . . 7
class ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
35 | 10, 14, 34 | csb 3856 |
. . . . . 6
class
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))) |
36 | 8, 9, 35 | cmpt 5189 |
. . . . 5
class (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))) |
37 | 4, 7, 36 | cwrecs 8243 |
. . . 4
class wrecs(
< , โ0, (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1)))))) |
38 | 6, 37 | cfv 6497 |
. . 3
class (wrecs(
< , โ0, (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐) |
39 | 2, 3, 4, 5, 38 | cmpo 7360 |
. 2
class (๐ โ โ0,
๐ฅ โ โ โฆ
(wrecs( < , โ0, (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐)) |
40 | 1, 39 | wceq 1542 |
1
wff BernPoly =
(๐ โ
โ0, ๐ฅ
โ โ โฆ (wrecs( < , โ0, (๐ โ V โฆ
โฆ(โฏโdom ๐) / ๐โฆ((๐ฅโ๐) โ ฮฃ๐ โ dom ๐((๐C๐) ยท ((๐โ๐) / ((๐ โ ๐) + 1))))))โ๐)) |