Step | Hyp | Ref
| Expression |
1 | | crmy 41271 |
. 2
class
Yrm |
2 | | va |
. . 3
setvar ๐ |
3 | | vn |
. . 3
setvar ๐ |
4 | | c2 12216 |
. . . 4
class
2 |
5 | | cuz 12771 |
. . . 4
class
โคโฅ |
6 | 4, 5 | cfv 6500 |
. . 3
class
(โคโฅโ2) |
7 | | cz 12507 |
. . 3
class
โค |
8 | 2 | cv 1541 |
. . . . . . 7
class ๐ |
9 | | cexp 13976 |
. . . . . . . . . 10
class
โ |
10 | 8, 4, 9 | co 7361 |
. . . . . . . . 9
class (๐โ2) |
11 | | c1 11060 |
. . . . . . . . 9
class
1 |
12 | | cmin 11393 |
. . . . . . . . 9
class
โ |
13 | 10, 11, 12 | co 7361 |
. . . . . . . 8
class ((๐โ2) โ
1) |
14 | | csqrt 15127 |
. . . . . . . 8
class
โ |
15 | 13, 14 | cfv 6500 |
. . . . . . 7
class
(โโ((๐โ2) โ 1)) |
16 | | caddc 11062 |
. . . . . . 7
class
+ |
17 | 8, 15, 16 | co 7361 |
. . . . . 6
class (๐ + (โโ((๐โ2) โ
1))) |
18 | 3 | cv 1541 |
. . . . . 6
class ๐ |
19 | 17, 18, 9 | co 7361 |
. . . . 5
class ((๐ + (โโ((๐โ2) โ 1)))โ๐) |
20 | | vb |
. . . . . . 7
setvar ๐ |
21 | | cn0 12421 |
. . . . . . . 8
class
โ0 |
22 | 21, 7 | cxp 5635 |
. . . . . . 7
class
(โ0 ร โค) |
23 | 20 | cv 1541 |
. . . . . . . . 9
class ๐ |
24 | | c1st 7923 |
. . . . . . . . 9
class
1st |
25 | 23, 24 | cfv 6500 |
. . . . . . . 8
class
(1st โ๐) |
26 | | c2nd 7924 |
. . . . . . . . . 10
class
2nd |
27 | 23, 26 | cfv 6500 |
. . . . . . . . 9
class
(2nd โ๐) |
28 | | cmul 11064 |
. . . . . . . . 9
class
ยท |
29 | 15, 27, 28 | co 7361 |
. . . . . . . 8
class
((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)) |
30 | 25, 29, 16 | co 7361 |
. . . . . . 7
class
((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))) |
31 | 20, 22, 30 | cmpt 5192 |
. . . . . 6
class (๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) |
32 | 31 | ccnv 5636 |
. . . . 5
class โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐)))) |
33 | 19, 32 | cfv 6500 |
. . . 4
class (โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)) |
34 | 33, 26 | cfv 6500 |
. . 3
class
(2nd โ(โก(๐ โ (โ0
ร โค) โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐))) |
35 | 2, 3, 6, 7, 34 | cmpo 7363 |
. 2
class (๐ โ
(โคโฅโ2), ๐ โ โค โฆ (2nd
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)))) |
36 | 1, 35 | wceq 1542 |
1
wff
Yrm = (๐ โ
(โคโฅโ2), ๐ โ โค โฆ (2nd
โ(โก(๐ โ (โ0 ร โค)
โฆ ((1st โ๐) + ((โโ((๐โ2) โ 1)) ยท (2nd
โ๐))))โ((๐ + (โโ((๐โ2) โ 1)))โ๐)))) |