Metamath Proof Explorer

Theorem gzrngunit

Description: The units on ZZ [ _i ] are the gaussian integers with norm 1 . (Contributed by Mario Carneiro, 4-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 gzrng.1 
 |-  Z = ( CCfld |`s Z[i] )
2 gzsubrg 
 |-  Z[i] e. ( SubRing ` CCfld )
3 1 subrgbas 
 |-  ( Z[i] e. ( SubRing ` CCfld ) -> Z[i] = ( Base ` Z ) )
4 2 3 ax-mp 
 |-  Z[i] = ( Base ` Z )
5 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
6 4 5 unitcl 
 |-  ( A e. ( Unit ` Z ) -> A e. Z[i] )
7 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
8 eqid 
 |-  ( invr ` Z ) = ( invr ` Z )
9 1 7 5 8 subrginv 
 |-  ( ( Z[i] e. ( SubRing ` CCfld ) /\ A e. ( Unit ` Z ) ) -> ( ( invr ` CCfld ) ` A ) = ( ( invr ` Z ) ` A ) )
10 2 9 mpan 
 |-  ( A e. ( Unit ` Z ) -> ( ( invr ` CCfld ) ` A ) = ( ( invr ` Z ) ` A ) )
11 gzcn 
 |-  ( A e. Z[i] -> A e. CC )
12 6 11 syl 
 |-  ( A e. ( Unit ` Z ) -> A e. CC )
13 0red 
 |-  ( A e. ( Unit ` Z ) -> 0 e. RR )
14 1re 
 |-  1 e. RR
15 14 a1i 
 |-  ( A e. ( Unit ` Z ) -> 1 e. RR )
16 12 abscld 
 |-  ( A e. ( Unit ` Z ) -> ( abs ` A ) e. RR )
17 0lt1 
 |-  0 < 1
18 17 a1i 
 |-  ( A e. ( Unit ` Z ) -> 0 < 1 )
19 1 gzrngunitlem 
 |-  ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` A ) )
20 13 15 16 18 19 ltletrd 
 |-  ( A e. ( Unit ` Z ) -> 0 < ( abs ` A ) )
21 20 gt0ne0d 
 |-  ( A e. ( Unit ` Z ) -> ( abs ` A ) =/= 0 )
22 12 abs00ad 
 |-  ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 0 <-> A = 0 ) )
23 22 necon3bid 
 |-  ( A e. ( Unit ` Z ) -> ( ( abs ` A ) =/= 0 <-> A =/= 0 ) )
24 21 23 mpbid 
 |-  ( A e. ( Unit ` Z ) -> A =/= 0 )
25 cnfldinv 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
26 12 24 25 syl2anc 
 |-  ( A e. ( Unit ` Z ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
27 10 26 eqtr3d 
 |-  ( A e. ( Unit ` Z ) -> ( ( invr ` Z ) ` A ) = ( 1 / A ) )
28 1 subrgring 
 |-  ( Z[i] e. ( SubRing ` CCfld ) -> Z e. Ring )
29 2 28 ax-mp 
 |-  Z e. Ring
30 5 8 unitinvcl 
 |-  ( ( Z e. Ring /\ A e. ( Unit ` Z ) ) -> ( ( invr ` Z ) ` A ) e. ( Unit ` Z ) )
31 29 30 mpan 
 |-  ( A e. ( Unit ` Z ) -> ( ( invr ` Z ) ` A ) e. ( Unit ` Z ) )
32 27 31 eqeltrrd 
 |-  ( A e. ( Unit ` Z ) -> ( 1 / A ) e. ( Unit ` Z ) )
33 1 gzrngunitlem 
 |-  ( ( 1 / A ) e. ( Unit ` Z ) -> 1 <_ ( abs ` ( 1 / A ) ) )
34 32 33 syl 
 |-  ( A e. ( Unit ` Z ) -> 1 <_ ( abs ` ( 1 / A ) ) )
35 1cnd 
 |-  ( A e. ( Unit ` Z ) -> 1 e. CC )
36 35 12 24 absdivd 
 |-  ( A e. ( Unit ` Z ) -> ( abs ` ( 1 / A ) ) = ( ( abs ` 1 ) / ( abs ` A ) ) )
37 34 36 breqtrd 
 |-  ( A e. ( Unit ` Z ) -> 1 <_ ( ( abs ` 1 ) / ( abs ` A ) ) )
38 1div1e1 
 |-  ( 1 / 1 ) = 1
39 abs1 
 |-  ( abs ` 1 ) = 1
40 39 eqcomi 
 |-  1 = ( abs ` 1 )
41 40 oveq1i 
 |-  ( 1 / ( abs ` A ) ) = ( ( abs ` 1 ) / ( abs ` A ) )
42 37 38 41 3brtr4g 
 |-  ( A e. ( Unit ` Z ) -> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) )
43 lerec 
 |-  ( ( ( ( abs ` A ) e. RR /\ 0 < ( abs ` A ) ) /\ ( 1 e. RR /\ 0 < 1 ) ) -> ( ( abs ` A ) <_ 1 <-> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) ) )
44 16 20 15 18 43 syl22anc 
 |-  ( A e. ( Unit ` Z ) -> ( ( abs ` A ) <_ 1 <-> ( 1 / 1 ) <_ ( 1 / ( abs ` A ) ) ) )
45 42 44 mpbird 
 |-  ( A e. ( Unit ` Z ) -> ( abs ` A ) <_ 1 )
46 letri3 
 |-  ( ( ( abs ` A ) e. RR /\ 1 e. RR ) -> ( ( abs ` A ) = 1 <-> ( ( abs ` A ) <_ 1 /\ 1 <_ ( abs ` A ) ) ) )
47 16 14 46 sylancl 
 |-  ( A e. ( Unit ` Z ) -> ( ( abs ` A ) = 1 <-> ( ( abs ` A ) <_ 1 /\ 1 <_ ( abs ` A ) ) ) )
48 45 19 47 mpbir2and 
 |-  ( A e. ( Unit ` Z ) -> ( abs ` A ) = 1 )
49 6 48 jca 
 |-  ( A e. ( Unit ` Z ) -> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )
50 11 adantr 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. CC )
51 simpr 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( abs ` A ) = 1 )
52 ax-1ne0 
 |-  1 =/= 0
53 52 a1i 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> 1 =/= 0 )
54 51 53 eqnetrd 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( abs ` A ) =/= 0 )
55 fveq2 
 |-  ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
56 abs0 
 |-  ( abs ` 0 ) = 0
57 55 56 eqtrdi 
 |-  ( A = 0 -> ( abs ` A ) = 0 )
58 57 necon3i 
 |-  ( ( abs ` A ) =/= 0 -> A =/= 0 )
59 54 58 syl 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A =/= 0 )
60 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
61 50 59 60 sylanbrc 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. ( CC \ { 0 } ) )
62 simpl 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. Z[i] )
63 50 59 25 syl2anc 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
64 50 absvalsqd 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
65 51 oveq1d 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) )
66 sq1 
 |-  ( 1 ^ 2 ) = 1
67 65 66 eqtrdi 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = 1 )
68 64 67 eqtr3d 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( A x. ( * ` A ) ) = 1 )
69 68 oveq1d 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( A x. ( * ` A ) ) / A ) = ( 1 / A ) )
70 50 cjcld 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( * ` A ) e. CC )
71 70 50 59 divcan3d 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( A x. ( * ` A ) ) / A ) = ( * ` A ) )
72 63 69 71 3eqtr2d 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = ( * ` A ) )
73 gzcjcl 
 |-  ( A e. Z[i] -> ( * ` A ) e. Z[i] )
74 73 adantr 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( * ` A ) e. Z[i] )
75 72 74 eqeltrd 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) e. Z[i] )
76 cnfldbas 
 |-  CC = ( Base ` CCfld )
77 cnfld0 
 |-  0 = ( 0g ` CCfld )
78 cndrng 
 |-  CCfld e. DivRing
79 76 77 78 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
80 1 79 5 7 subrgunit 
 |-  ( Z[i] e. ( SubRing ` CCfld ) -> ( A e. ( Unit ` Z ) <-> ( A e. ( CC \ { 0 } ) /\ A e. Z[i] /\ ( ( invr ` CCfld ) ` A ) e. Z[i] ) ) )
81 2 80 ax-mp 
 |-  ( A e. ( Unit ` Z ) <-> ( A e. ( CC \ { 0 } ) /\ A e. Z[i] /\ ( ( invr ` CCfld ) ` A ) e. Z[i] ) )
82 61 62 75 81 syl3anbrc 
 |-  ( ( A e. Z[i] /\ ( abs ` A ) = 1 ) -> A e. ( Unit ` Z ) )
83 49 82 impbii 
 |-  ( A e. ( Unit ` Z ) <-> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )