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 = fld 𝑠 i
Assertion gzrngunit A Unit Z A i A = 1

Proof

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