Step | Hyp | Ref
| Expression |
1 | | crmy 41629 |
. 2
class
Yrm |
2 | | va |
. . 3
setvar ๐ |
3 | | vn |
. . 3
setvar ๐ |
4 | | c2 12266 |
. . . 4
class
2 |
5 | | cuz 12821 |
. . . 4
class
โคโฅ |
6 | 4, 5 | cfv 6543 |
. . 3
class
(โคโฅโ2) |
7 | | cz 12557 |
. . 3
class
โค |
8 | 2 | cv 1540 |
. . . . . . 7
class ๐ |
9 | | cexp 14026 |
. . . . . . . . . 10
class
โ |
10 | 8, 4, 9 | co 7408 |
. . . . . . . . 9
class (๐โ2) |
11 | | c1 11110 |
. . . . . . . . 9
class
1 |
12 | | cmin 11443 |
. . . . . . . . 9
class
โ |
13 | 10, 11, 12 | co 7408 |
. . . . . . . 8
class ((๐โ2) โ
1) |
14 | | csqrt 15179 |
. . . . . . . 8
class
โ |
15 | 13, 14 | cfv 6543 |
. . . . . . 7
class
(โโ((๐โ2) โ 1)) |
16 | | caddc 11112 |
. . . . . . 7
class
+ |
17 | 8, 15, 16 | co 7408 |
. . . . . 6
class (๐ + (โโ((๐โ2) โ
1))) |
18 | 3 | cv 1540 |
. . . . . 6
class ๐ |
19 | 17, 18, 9 | co 7408 |
. . . . 5
class ((๐ + (โโ((๐โ2) โ 1)))โ๐) |
20 | | vb |
. . . . . . 7
setvar ๐ |
21 | | cn0 12471 |
. . . . . . . 8
class
โ0 |
22 | 21, 7 | cxp 5674 |
. . . . . . 7
class
(โ0 ร โค) |
23 | 20 | cv 1540 |
. . . . . . . . 9
class ๐ |
24 | | c1st 7972 |
. . . . . . . . 9
class
1st |
25 | 23, 24 | cfv 6543 |
. . . . . . . 8
class
(1st โ๐) |
26 | | c2nd 7973 |
. . . . . . . . . 10
class
2nd |
27 | 23, 26 | cfv 6543 |
. . . . . . . . 9
class
(2nd โ๐) |
28 | | cmul 11114 |
. . . . . . . . 9
class
ยท |
29 | 15, 27, 28 | co 7408 |
. . . . . . . 8
class
((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)) |
30 | 25, 29, 16 | co 7408 |
. . . . . . 7
class
((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))) |
31 | 20, 22, 30 | cmpt 5231 |
. . . . . 6
class (๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) |
32 | 31 | ccnv 5675 |
. . . . 5
class โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) |
33 | 19, 32 | cfv 6543 |
. . . 4
class (โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)) |
34 | 33, 26 | cfv 6543 |
. . 3
class
(2nd โ(โก(๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐))) |
35 | 2, 3, 6, 7, 34 | cmpo 7410 |
. 2
class (๐ โ
(โคโฅโ2), ๐ โ โค โฆ (2nd
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)))) |
36 | 1, 35 | wceq 1541 |
1
wff
Yrm = (๐ โ
(โคโฅโ2), ๐ โ โค โฆ (2nd
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)))) |