Step | Hyp | Ref
| Expression |
1 | | cufd 32313 |
. 2
class
UFD |
2 | | vr |
. . . . . . 7
setvar ๐ |
3 | 2 | cv 1541 |
. . . . . 6
class ๐ |
4 | | cabv 20318 |
. . . . . 6
class
AbsVal |
5 | 3, 4 | cfv 6500 |
. . . . 5
class
(AbsValโ๐) |
6 | | c0 4286 |
. . . . 5
class
โ
|
7 | 5, 6 | wne 2940 |
. . . 4
wff
(AbsValโ๐)
โ โ
|
8 | | vi |
. . . . . . . 8
setvar ๐ |
9 | 8 | cv 1541 |
. . . . . . 7
class ๐ |
10 | | crpm 20151 |
. . . . . . . 8
class
RPrime |
11 | 3, 10 | cfv 6500 |
. . . . . . 7
class
(RPrimeโ๐) |
12 | 9, 11 | cin 3913 |
. . . . . 6
class (๐ โฉ (RPrimeโ๐)) |
13 | 12, 6 | wne 2940 |
. . . . 5
wff (๐ โฉ (RPrimeโ๐)) โ โ
|
14 | | cprmidl 32262 |
. . . . . 6
class
PrmIdeal |
15 | 3, 14 | cfv 6500 |
. . . . 5
class
(PrmIdealโ๐) |
16 | 13, 8, 15 | wral 3061 |
. . . 4
wff
โ๐ โ
(PrmIdealโ๐)(๐ โฉ (RPrimeโ๐)) โ โ
|
17 | 7, 16 | wa 397 |
. . 3
wff
((AbsValโ๐)
โ โ
โง โ๐ โ (PrmIdealโ๐)(๐ โฉ (RPrimeโ๐)) โ โ
) |
18 | | ccrg 19973 |
. . 3
class
CRing |
19 | 17, 2, 18 | crab 3406 |
. 2
class {๐ โ CRing โฃ
((AbsValโ๐) โ
โ
โง โ๐
โ (PrmIdealโ๐)(๐ โฉ (RPrimeโ๐)) โ โ
)} |
20 | 1, 19 | wceq 1542 |
1
wff UFD =
{๐ โ CRing โฃ
((AbsValโ๐) โ
โ
โง โ๐
โ (PrmIdealโ๐)(๐ โฉ (RPrimeโ๐)) โ โ
)} |