This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zringunit

Description: The units of ZZ are the integers with norm 1 , i.e. 1 and -u 1 . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

Ref Expression
Assertion zringunit 
|- ( A e. ( Unit ` ZZring ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) )

Proof

Step Hyp Ref Expression
1 zringbas 
 |-  ZZ = ( Base ` ZZring )
2 eqid 
 |-  ( Unit ` ZZring ) = ( Unit ` ZZring )
3 1 2 unitcl 
 |-  ( A e. ( Unit ` ZZring ) -> A e. ZZ )
4 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
5 zgz 
 |-  ( x e. ZZ -> x e. Z[i] )
6 5 ssriv 
 |-  ZZ C_ Z[i]
7 gzsubrg 
 |-  Z[i] e. ( SubRing ` CCfld )
8 eqid 
 |-  ( CCfld |`s Z[i] ) = ( CCfld |`s Z[i] )
9 8 subsubrg 
 |-  ( Z[i] e. ( SubRing ` CCfld ) -> ( ZZ e. ( SubRing ` ( CCfld |`s Z[i] ) ) <-> ( ZZ e. ( SubRing ` CCfld ) /\ ZZ C_ Z[i] ) ) )
10 7 9 ax-mp 
 |-  ( ZZ e. ( SubRing ` ( CCfld |`s Z[i] ) ) <-> ( ZZ e. ( SubRing ` CCfld ) /\ ZZ C_ Z[i] ) )
11 4 6 10 mpbir2an 
 |-  ZZ e. ( SubRing ` ( CCfld |`s Z[i] ) )
12 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
13 ressabs 
 |-  ( ( Z[i] e. ( SubRing ` CCfld ) /\ ZZ C_ Z[i] ) -> ( ( CCfld |`s Z[i] ) |`s ZZ ) = ( CCfld |`s ZZ ) )
14 7 6 13 mp2an 
 |-  ( ( CCfld |`s Z[i] ) |`s ZZ ) = ( CCfld |`s ZZ )
15 12 14 eqtr4i 
 |-  ZZring = ( ( CCfld |`s Z[i] ) |`s ZZ )
16 eqid 
 |-  ( Unit ` ( CCfld |`s Z[i] ) ) = ( Unit ` ( CCfld |`s Z[i] ) )
17 15 16 2 subrguss 
 |-  ( ZZ e. ( SubRing ` ( CCfld |`s Z[i] ) ) -> ( Unit ` ZZring ) C_ ( Unit ` ( CCfld |`s Z[i] ) ) )
18 11 17 ax-mp 
 |-  ( Unit ` ZZring ) C_ ( Unit ` ( CCfld |`s Z[i] ) )
19 18 sseli 
 |-  ( A e. ( Unit ` ZZring ) -> A e. ( Unit ` ( CCfld |`s Z[i] ) ) )
20 8 gzrngunit 
 |-  ( A e. ( Unit ` ( CCfld |`s Z[i] ) ) <-> ( A e. Z[i] /\ ( abs ` A ) = 1 ) )
21 20 simprbi 
 |-  ( A e. ( Unit ` ( CCfld |`s Z[i] ) ) -> ( abs ` A ) = 1 )
22 19 21 syl 
 |-  ( A e. ( Unit ` ZZring ) -> ( abs ` A ) = 1 )
23 3 22 jca 
 |-  ( A e. ( Unit ` ZZring ) -> ( A e. ZZ /\ ( abs ` A ) = 1 ) )
24 zcn 
 |-  ( A e. ZZ -> A e. CC )
25 24 adantr 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A e. CC )
26 simpr 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( abs ` A ) = 1 )
27 ax-1ne0 
 |-  1 =/= 0
28 27 a1i 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> 1 =/= 0 )
29 26 28 eqnetrd 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( abs ` A ) =/= 0 )
30 fveq2 
 |-  ( A = 0 -> ( abs ` A ) = ( abs ` 0 ) )
31 abs0 
 |-  ( abs ` 0 ) = 0
32 30 31 eqtrdi 
 |-  ( A = 0 -> ( abs ` A ) = 0 )
33 32 necon3i 
 |-  ( ( abs ` A ) =/= 0 -> A =/= 0 )
34 29 33 syl 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A =/= 0 )
35 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
36 25 34 35 sylanbrc 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A e. ( CC \ { 0 } ) )
37 simpl 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A e. ZZ )
38 cnfldinv 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
39 25 34 38 syl2anc 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = ( 1 / A ) )
40 zre 
 |-  ( A e. ZZ -> A e. RR )
41 40 adantr 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A e. RR )
42 absresq 
 |-  ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
43 41 42 syl 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
44 26 oveq1d 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = ( 1 ^ 2 ) )
45 sq1 
 |-  ( 1 ^ 2 ) = 1
46 44 45 eqtrdi 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( abs ` A ) ^ 2 ) = 1 )
47 25 sqvald 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( A ^ 2 ) = ( A x. A ) )
48 43 46 47 3eqtr3rd 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( A x. A ) = 1 )
49 1cnd 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> 1 e. CC )
50 49 25 25 34 divmuld 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( 1 / A ) = A <-> ( A x. A ) = 1 ) )
51 48 50 mpbird 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( 1 / A ) = A )
52 39 51 eqtrd 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) = A )
53 52 37 eqeltrd 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> ( ( invr ` CCfld ) ` A ) e. ZZ )
54 cnfldbas 
 |-  CC = ( Base ` CCfld )
55 cnfld0 
 |-  0 = ( 0g ` CCfld )
56 cndrng 
 |-  CCfld e. DivRing
57 54 55 56 drngui 
 |-  ( CC \ { 0 } ) = ( Unit ` CCfld )
58 eqid 
 |-  ( invr ` CCfld ) = ( invr ` CCfld )
59 12 57 2 58 subrgunit 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ( A e. ( Unit ` ZZring ) <-> ( A e. ( CC \ { 0 } ) /\ A e. ZZ /\ ( ( invr ` CCfld ) ` A ) e. ZZ ) ) )
60 4 59 ax-mp 
 |-  ( A e. ( Unit ` ZZring ) <-> ( A e. ( CC \ { 0 } ) /\ A e. ZZ /\ ( ( invr ` CCfld ) ` A ) e. ZZ ) )
61 36 37 53 60 syl3anbrc 
 |-  ( ( A e. ZZ /\ ( abs ` A ) = 1 ) -> A e. ( Unit ` ZZring ) )
62 23 61 impbii 
 |-  ( A e. ( Unit ` ZZring ) <-> ( A e. ZZ /\ ( abs ` A ) = 1 ) )