Step | Hyp | Ref
| Expression |
1 | | vx |
. . 3
setvar ๐ฅ |
2 | | cA |
. . 3
class ๐ด |
3 | | cB |
. . 3
class ๐ต |
4 | 1, 2, 3 | citg 25135 |
. 2
class
โซ๐ด๐ต d๐ฅ |
5 | | cc0 11110 |
. . . 4
class
0 |
6 | | c3 12268 |
. . . 4
class
3 |
7 | | cfz 13484 |
. . . 4
class
... |
8 | 5, 6, 7 | co 7409 |
. . 3
class
(0...3) |
9 | | ci 11112 |
. . . . 5
class
i |
10 | | vk |
. . . . . 6
setvar ๐ |
11 | 10 | cv 1541 |
. . . . 5
class ๐ |
12 | | cexp 14027 |
. . . . 5
class
โ |
13 | 9, 11, 12 | co 7409 |
. . . 4
class
(iโ๐) |
14 | | cr 11109 |
. . . . . 6
class
โ |
15 | | vy |
. . . . . . 7
setvar ๐ฆ |
16 | | cdiv 11871 |
. . . . . . . . 9
class
/ |
17 | 3, 13, 16 | co 7409 |
. . . . . . . 8
class (๐ต / (iโ๐)) |
18 | | cre 15044 |
. . . . . . . 8
class
โ |
19 | 17, 18 | cfv 6544 |
. . . . . . 7
class
(โโ(๐ต /
(iโ๐))) |
20 | 1 | cv 1541 |
. . . . . . . . . 10
class ๐ฅ |
21 | 20, 2 | wcel 2107 |
. . . . . . . . 9
wff ๐ฅ โ ๐ด |
22 | 15 | cv 1541 |
. . . . . . . . . 10
class ๐ฆ |
23 | | cle 11249 |
. . . . . . . . . 10
class
โค |
24 | 5, 22, 23 | wbr 5149 |
. . . . . . . . 9
wff 0 โค
๐ฆ |
25 | 21, 24 | wa 397 |
. . . . . . . 8
wff (๐ฅ โ ๐ด โง 0 โค ๐ฆ) |
26 | 25, 22, 5 | cif 4529 |
. . . . . . 7
class if((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0) |
27 | 15, 19, 26 | csb 3894 |
. . . . . 6
class
โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0) |
28 | 1, 14, 27 | cmpt 5232 |
. . . . 5
class (๐ฅ โ โ โฆ
โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0)) |
29 | | citg2 25133 |
. . . . 5
class
โซ2 |
30 | 28, 29 | cfv 6544 |
. . . 4
class
(โซ2โ(๐ฅ โ โ โฆ
โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0))) |
31 | | cmul 11115 |
. . . 4
class
ยท |
32 | 13, 30, 31 | co 7409 |
. . 3
class
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0)))) |
33 | 8, 32, 10 | csu 15632 |
. 2
class
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0)))) |
34 | 4, 33 | wceq 1542 |
1
wff โซ๐ด๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
โฆ(โโ(๐ต / (iโ๐))) / ๐ฆโฆif((๐ฅ โ ๐ด โง 0 โค ๐ฆ), ๐ฆ, 0)))) |