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 eqtrdi ⊢ 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 eqtrdi ⊢ 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