Metamath Proof Explorer

Theorem gzrngunitlem

Description: Lemma for gzrngunit . (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypothesis gzrng.1 
|- Z = ( CCfld |`s Z[i] )
Assertion gzrngunitlem 
|- ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` A ) )

Proof

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 ) )