| Step |
Hyp |
Ref |
Expression |
| 1 |
|
gzrng.1 |
|- Z = ( CCfld |`s Z[i] ) |
| 2 |
|
sq1 |
|- ( 1 ^ 2 ) = 1 |
| 3 |
|
ax-1ne0 |
|- 1 =/= 0 |
| 4 |
|
gzsubrg |
|- Z[i] e. ( SubRing ` CCfld ) |
| 5 |
1
|
subrgring |
|- ( Z[i] e. ( SubRing ` CCfld ) -> Z e. Ring ) |
| 6 |
|
eqid |
|- ( Unit ` Z ) = ( Unit ` Z ) |
| 7 |
|
subrgsubg |
|- ( Z[i] e. ( SubRing ` CCfld ) -> Z[i] e. ( SubGrp ` CCfld ) ) |
| 8 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
| 9 |
1 8
|
subg0 |
|- ( Z[i] e. ( SubGrp ` CCfld ) -> 0 = ( 0g ` Z ) ) |
| 10 |
4 7 9
|
mp2b |
|- 0 = ( 0g ` Z ) |
| 11 |
|
cnfld1 |
|- 1 = ( 1r ` CCfld ) |
| 12 |
1 11
|
subrg1 |
|- ( Z[i] e. ( SubRing ` CCfld ) -> 1 = ( 1r ` Z ) ) |
| 13 |
4 12
|
ax-mp |
|- 1 = ( 1r ` Z ) |
| 14 |
6 10 13
|
0unit |
|- ( Z e. Ring -> ( 0 e. ( Unit ` Z ) <-> 1 = 0 ) ) |
| 15 |
4 5 14
|
mp2b |
|- ( 0 e. ( Unit ` Z ) <-> 1 = 0 ) |
| 16 |
3 15
|
nemtbir |
|- -. 0 e. ( Unit ` Z ) |
| 17 |
1
|
subrgbas |
|- ( Z[i] e. ( SubRing ` CCfld ) -> Z[i] = ( Base ` Z ) ) |
| 18 |
4 17
|
ax-mp |
|- Z[i] = ( Base ` Z ) |
| 19 |
18 6
|
unitcl |
|- ( A e. ( Unit ` Z ) -> A e. Z[i] ) |
| 20 |
|
gzabssqcl |
|- ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) e. NN0 ) |
| 21 |
19 20
|
syl |
|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) ^ 2 ) e. NN0 ) |
| 22 |
|
elnn0 |
|- ( ( ( abs ` A ) ^ 2 ) e. NN0 <-> ( ( ( abs ` A ) ^ 2 ) e. NN \/ ( ( abs ` A ) ^ 2 ) = 0 ) ) |
| 23 |
21 22
|
sylib |
|- ( A e. ( Unit ` Z ) -> ( ( ( abs ` A ) ^ 2 ) e. NN \/ ( ( abs ` A ) ^ 2 ) = 0 ) ) |
| 24 |
23
|
ord |
|- ( A e. ( Unit ` Z ) -> ( -. ( ( abs ` A ) ^ 2 ) e. NN -> ( ( abs ` A ) ^ 2 ) = 0 ) ) |
| 25 |
|
gzcn |
|- ( A e. Z[i] -> A e. CC ) |
| 26 |
19 25
|
syl |
|- ( A e. ( Unit ` Z ) -> A e. CC ) |
| 27 |
26
|
abscld |
|- ( A e. ( Unit ` Z ) -> ( abs ` A ) e. RR ) |
| 28 |
27
|
recnd |
|- ( A e. ( Unit ` Z ) -> ( abs ` A ) e. CC ) |
| 29 |
|
sqeq0 |
|- ( ( abs ` A ) e. CC -> ( ( ( abs ` A ) ^ 2 ) = 0 <-> ( abs ` A ) = 0 ) ) |
| 30 |
28 29
|
syl |
|- ( A e. ( Unit ` Z ) -> ( ( ( abs ` A ) ^ 2 ) = 0 <-> ( abs ` A ) = 0 ) ) |
| 31 |
26
|
abs00ad |
|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 0 <-> A = 0 ) ) |
| 32 |
|
eleq1 |
|- ( A = 0 -> ( A e. ( Unit ` Z ) <-> 0 e. ( Unit ` Z ) ) ) |
| 33 |
32
|
biimpcd |
|- ( A e. ( Unit ` Z ) -> ( A = 0 -> 0 e. ( Unit ` Z ) ) ) |
| 34 |
31 33
|
sylbid |
|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 0 -> 0 e. ( Unit ` Z ) ) ) |
| 35 |
30 34
|
sylbid |
|- ( A e. ( Unit ` Z ) -> ( ( ( abs ` A ) ^ 2 ) = 0 -> 0 e. ( Unit ` Z ) ) ) |
| 36 |
24 35
|
syld |
|- ( A e. ( Unit ` Z ) -> ( -. ( ( abs ` A ) ^ 2 ) e. NN -> 0 e. ( Unit ` Z ) ) ) |
| 37 |
16 36
|
mt3i |
|- ( A e. ( Unit ` Z ) -> ( ( abs ` A ) ^ 2 ) e. NN ) |
| 38 |
37
|
nnge1d |
|- ( A e. ( Unit ` Z ) -> 1 <_ ( ( abs ` A ) ^ 2 ) ) |
| 39 |
2 38
|
eqbrtrid |
|- ( A e. ( Unit ` Z ) -> ( 1 ^ 2 ) <_ ( ( abs ` A ) ^ 2 ) ) |
| 40 |
26
|
absge0d |
|- ( A e. ( Unit ` Z ) -> 0 <_ ( abs ` A ) ) |
| 41 |
|
1re |
|- 1 e. RR |
| 42 |
|
0le1 |
|- 0 <_ 1 |
| 43 |
|
le2sq |
|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) -> ( 1 <_ ( abs ` A ) <-> ( 1 ^ 2 ) <_ ( ( abs ` A ) ^ 2 ) ) ) |
| 44 |
41 42 43
|
mpanl12 |
|- ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) -> ( 1 <_ ( abs ` A ) <-> ( 1 ^ 2 ) <_ ( ( abs ` A ) ^ 2 ) ) ) |
| 45 |
27 40 44
|
syl2anc |
|- ( A e. ( Unit ` Z ) -> ( 1 <_ ( abs ` A ) <-> ( 1 ^ 2 ) <_ ( ( abs ` A ) ^ 2 ) ) ) |
| 46 |
39 45
|
mpbird |
|- ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` A ) ) |