| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1ne2 |
|- 1 =/= 2 |
| 2 |
1
|
nesymi |
|- -. 2 = 1 |
| 3 |
|
2re |
|- 2 e. RR |
| 4 |
|
0le2 |
|- 0 <_ 2 |
| 5 |
|
absid |
|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 ) |
| 6 |
3 4 5
|
mp2an |
|- ( abs ` 2 ) = 2 |
| 7 |
6
|
eqeq1i |
|- ( ( abs ` 2 ) = 1 <-> 2 = 1 ) |
| 8 |
2 7
|
mtbir |
|- -. ( abs ` 2 ) = 1 |
| 9 |
8
|
intnan |
|- -. ( 2 e. ZZ /\ ( abs ` 2 ) = 1 ) |
| 10 |
|
zringunit |
|- ( 2 e. ( Unit ` ZZring ) <-> ( 2 e. ZZ /\ ( abs ` 2 ) = 1 ) ) |
| 11 |
9 10
|
mtbir |
|- -. 2 e. ( Unit ` ZZring ) |
| 12 |
|
zringbas |
|- ZZ = ( Base ` ZZring ) |
| 13 |
|
eqid |
|- ( Unit ` ZZring ) = ( Unit ` ZZring ) |
| 14 |
|
zring0 |
|- 0 = ( 0g ` ZZring ) |
| 15 |
12 13 14
|
isdrng |
|- ( ZZring e. DivRing <-> ( ZZring e. Ring /\ ( Unit ` ZZring ) = ( ZZ \ { 0 } ) ) ) |
| 16 |
|
2z |
|- 2 e. ZZ |
| 17 |
|
2ne0 |
|- 2 =/= 0 |
| 18 |
|
eldifsn |
|- ( 2 e. ( ZZ \ { 0 } ) <-> ( 2 e. ZZ /\ 2 =/= 0 ) ) |
| 19 |
16 17 18
|
mpbir2an |
|- 2 e. ( ZZ \ { 0 } ) |
| 20 |
|
id |
|- ( ( Unit ` ZZring ) = ( ZZ \ { 0 } ) -> ( Unit ` ZZring ) = ( ZZ \ { 0 } ) ) |
| 21 |
19 20
|
eleqtrrid |
|- ( ( Unit ` ZZring ) = ( ZZ \ { 0 } ) -> 2 e. ( Unit ` ZZring ) ) |
| 22 |
15 21
|
simplbiim |
|- ( ZZring e. DivRing -> 2 e. ( Unit ` ZZring ) ) |
| 23 |
11 22
|
mto |
|- -. ZZring e. DivRing |
| 24 |
23
|
nelir |
|- ZZring e/ DivRing |