Step | Hyp | Ref
| Expression |
1 | | crisefac 15948 |
. 2
class
RiseFac |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vn |
. . 3
setvar ๐ |
4 | | cc 11107 |
. . 3
class
โ |
5 | | cn0 12471 |
. . 3
class
โ0 |
6 | | cc0 11109 |
. . . . 5
class
0 |
7 | 3 | cv 1540 |
. . . . . 6
class ๐ |
8 | | c1 11110 |
. . . . . 6
class
1 |
9 | | cmin 11443 |
. . . . . 6
class
โ |
10 | 7, 8, 9 | co 7408 |
. . . . 5
class (๐ โ 1) |
11 | | cfz 13483 |
. . . . 5
class
... |
12 | 6, 10, 11 | co 7408 |
. . . 4
class
(0...(๐ โ
1)) |
13 | 2 | cv 1540 |
. . . . 5
class ๐ฅ |
14 | | vk |
. . . . . 6
setvar ๐ |
15 | 14 | cv 1540 |
. . . . 5
class ๐ |
16 | | caddc 11112 |
. . . . 5
class
+ |
17 | 13, 15, 16 | co 7408 |
. . . 4
class (๐ฅ + ๐) |
18 | 12, 17, 14 | cprod 15848 |
. . 3
class
โ๐ โ
(0...(๐ โ 1))(๐ฅ + ๐) |
19 | 2, 3, 4, 5, 18 | cmpo 7410 |
. 2
class (๐ฅ โ โ, ๐ โ โ0
โฆ โ๐ โ
(0...(๐ โ 1))(๐ฅ + ๐)) |
20 | 1, 19 | wceq 1541 |
1
wff RiseFac =
(๐ฅ โ โ, ๐ โ โ0
โฆ โ๐ โ
(0...(๐ โ 1))(๐ฅ + ๐)) |