Step | Hyp | Ref
| Expression |
1 | | cexp 10519 |
. 2
class
โ |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | cc 7809 |
. . 3
class
โ |
5 | | cz 9253 |
. . 3
class
โค |
6 | 3 | cv 1352 |
. . . . 5
class ๐ฆ |
7 | | cc0 7811 |
. . . . 5
class
0 |
8 | 6, 7 | wceq 1353 |
. . . 4
wff ๐ฆ = 0 |
9 | | c1 7812 |
. . . 4
class
1 |
10 | | clt 7992 |
. . . . . 6
class
< |
11 | 7, 6, 10 | wbr 4004 |
. . . . 5
wff 0 <
๐ฆ |
12 | | cmul 7816 |
. . . . . . 7
class
ยท |
13 | | cn 8919 |
. . . . . . . 8
class
โ |
14 | 2 | cv 1352 |
. . . . . . . . 9
class ๐ฅ |
15 | 14 | csn 3593 |
. . . . . . . 8
class {๐ฅ} |
16 | 13, 15 | cxp 4625 |
. . . . . . 7
class (โ
ร {๐ฅ}) |
17 | 12, 16, 9 | cseq 10445 |
. . . . . 6
class seq1(
ยท , (โ ร {๐ฅ})) |
18 | 6, 17 | cfv 5217 |
. . . . 5
class (seq1(
ยท , (โ ร {๐ฅ}))โ๐ฆ) |
19 | 6 | cneg 8129 |
. . . . . . 7
class -๐ฆ |
20 | 19, 17 | cfv 5217 |
. . . . . 6
class (seq1(
ยท , (โ ร {๐ฅ}))โ-๐ฆ) |
21 | | cdiv 8629 |
. . . . . 6
class
/ |
22 | 9, 20, 21 | co 5875 |
. . . . 5
class (1 /
(seq1( ยท , (โ ร {๐ฅ}))โ-๐ฆ)) |
23 | 11, 18, 22 | cif 3535 |
. . . 4
class if(0 <
๐ฆ, (seq1( ยท ,
(โ ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท , (โ ร
{๐ฅ}))โ-๐ฆ))) |
24 | 8, 9, 23 | cif 3535 |
. . 3
class if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ
ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ)))) |
25 | 2, 3, 4, 5, 24 | cmpo 5877 |
. 2
class (๐ฅ โ โ, ๐ฆ โ โค โฆ if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ
ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ))))) |
26 | 1, 25 | wceq 1353 |
1
wff โ =
(๐ฅ โ โ, ๐ฆ โ โค โฆ if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ
ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ))))) |