Step | Hyp | Ref
| Expression |
1 | | cexp 10521 |
. 2
class
โ |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | cc 7811 |
. . 3
class
โ |
5 | | cz 9255 |
. . 3
class
โค |
6 | 3 | cv 1352 |
. . . . 5
class ๐ฆ |
7 | | cc0 7813 |
. . . . 5
class
0 |
8 | 6, 7 | wceq 1353 |
. . . 4
wff ๐ฆ = 0 |
9 | | c1 7814 |
. . . 4
class
1 |
10 | | clt 7994 |
. . . . . 6
class
< |
11 | 7, 6, 10 | wbr 4005 |
. . . . 5
wff 0 <
๐ฆ |
12 | | cmul 7818 |
. . . . . . 7
class
ยท |
13 | | cn 8921 |
. . . . . . . 8
class
โ |
14 | 2 | cv 1352 |
. . . . . . . . 9
class ๐ฅ |
15 | 14 | csn 3594 |
. . . . . . . 8
class {๐ฅ} |
16 | 13, 15 | cxp 4626 |
. . . . . . 7
class (โ
ร {๐ฅ}) |
17 | 12, 16, 9 | cseq 10447 |
. . . . . 6
class seq1(
ยท , (โ ร {๐ฅ})) |
18 | 6, 17 | cfv 5218 |
. . . . 5
class (seq1(
ยท , (โ ร {๐ฅ}))โ๐ฆ) |
19 | 6 | cneg 8131 |
. . . . . . 7
class -๐ฆ |
20 | 19, 17 | cfv 5218 |
. . . . . 6
class (seq1(
ยท , (โ ร {๐ฅ}))โ-๐ฆ) |
21 | | cdiv 8631 |
. . . . . 6
class
/ |
22 | 9, 20, 21 | co 5877 |
. . . . 5
class (1 /
(seq1( ยท , (โ ร {๐ฅ}))โ-๐ฆ)) |
23 | 11, 18, 22 | cif 3536 |
. . . 4
class if(0 <
๐ฆ, (seq1( ยท ,
(โ ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท , (โ ร
{๐ฅ}))โ-๐ฆ))) |
24 | 8, 9, 23 | cif 3536 |
. . 3
class if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ
ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ)))) |
25 | 2, 3, 4, 5, 24 | cmpo 5879 |
. 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( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ))))) |