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 ∈ Unit ⁡ ℤ ring ↔ A ∈ ℤ ∧ A = 1

Proof

Step Hyp Ref Expression
1 zringbas ⊢ ℤ = Base ℤ ring
2 eqid ⊢ Unit ⁡ ℤ ring = Unit ⁡ ℤ ring
3 1 2 unitcl ⊢ A ∈ Unit ⁡ ℤ ring → A ∈ ℤ
4 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
5 zgz ⊢ x ∈ ℤ → x ∈ ℤ i
6 5 ssriv ⊢ ℤ ⊆ ℤ i
7 gzsubrg ⊢ ℤ i ∈ SubRing ⁡ ℂ fld
8 eqid ⊢ ℂ fld ↾ 𝑠 ℤ i = ℂ fld ↾ 𝑠 ℤ i
9 8 subsubrg ⊢ ℤ i ∈ SubRing ⁡ ℂ fld → ℤ ∈ SubRing ⁡ ℂ fld ↾ 𝑠 ℤ i ↔ ℤ ∈ SubRing ⁡ ℂ fld ∧ ℤ ⊆ ℤ i
10 7 9 ax-mp ⊢ ℤ ∈ SubRing ⁡ ℂ fld ↾ 𝑠 ℤ i ↔ ℤ ∈ SubRing ⁡ ℂ fld ∧ ℤ ⊆ ℤ i
11 4 6 10 mpbir2an ⊢ ℤ ∈ SubRing ⁡ ℂ fld ↾ 𝑠 ℤ i
12 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
13 ressabs ⊢ ℤ i ∈ SubRing ⁡ ℂ fld ∧ ℤ ⊆ ℤ i → ℂ fld ↾ 𝑠 ℤ i ↾ 𝑠 ℤ = ℂ fld ↾ 𝑠 ℤ
14 7 6 13 mp2an ⊢ ℂ fld ↾ 𝑠 ℤ i ↾ 𝑠 ℤ = ℂ fld ↾ 𝑠 ℤ
15 12 14 eqtr4i ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ i ↾ 𝑠 ℤ
16 eqid ⊢ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i = Unit ⁡ ℂ fld ↾ 𝑠 ℤ i
17 15 16 2 subrguss ⊢ ℤ ∈ SubRing ⁡ ℂ fld ↾ 𝑠 ℤ i → Unit ⁡ ℤ ring ⊆ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i
18 11 17 ax-mp ⊢ Unit ⁡ ℤ ring ⊆ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i
19 18 sseli ⊢ A ∈ Unit ⁡ ℤ ring → A ∈ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i
20 8 gzrngunit ⊢ A ∈ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i ↔ A ∈ ℤ i ∧ A = 1
21 20 simprbi ⊢ A ∈ Unit ⁡ ℂ fld ↾ 𝑠 ℤ i → A = 1
22 19 21 syl ⊢ A ∈ Unit ⁡ ℤ ring → A = 1
23 3 22 jca ⊢ A ∈ Unit ⁡ ℤ ring → A ∈ ℤ ∧ A = 1
24 zcn ⊢ A ∈ ℤ → A ∈ ℂ
25 24 adantr ⊢ A ∈ ℤ ∧ A = 1 → A ∈ ℂ
26 simpr ⊢ A ∈ ℤ ∧ A = 1 → A = 1
27 ax-1ne0 ⊢ 1 ≠ 0
28 27 a1i ⊢ A ∈ ℤ ∧ A = 1 → 1 ≠ 0
29 26 28 eqnetrd ⊢ A ∈ ℤ ∧ A = 1 → A ≠ 0
30 fveq2 ⊢ A = 0 → A = 0
31 abs0 ⊢ 0 = 0
32 30 31 syl6eq ⊢ A = 0 → A = 0
33 32 necon3i ⊢ A ≠ 0 → A ≠ 0
34 29 33 syl ⊢ A ∈ ℤ ∧ A = 1 → A ≠ 0
35 eldifsn ⊢ A ∈ ℂ ∖ 0 ↔ A ∈ ℂ ∧ A ≠ 0
36 25 34 35 sylanbrc ⊢ A ∈ ℤ ∧ A = 1 → A ∈ ℂ ∖ 0
37 simpl ⊢ A ∈ ℤ ∧ A = 1 → A ∈ ℤ
38 cnfldinv ⊢ A ∈ ℂ ∧ A ≠ 0 → inv r ⁡ ℂ fld ⁡ A = 1 A
39 25 34 38 syl2anc ⊢ A ∈ ℤ ∧ A = 1 → inv r ⁡ ℂ fld ⁡ A = 1 A
40 zre ⊢ A ∈ ℤ → A ∈ ℝ
41 40 adantr ⊢ A ∈ ℤ ∧ A = 1 → A ∈ ℝ
42 absresq ⊢ A ∈ ℝ → A 2 = A 2
43 41 42 syl ⊢ A ∈ ℤ ∧ A = 1 → A 2 = A 2
44 26 oveq1d ⊢ A ∈ ℤ ∧ A = 1 → A 2 = 1 2
45 sq1 ⊢ 1 2 = 1
46 44 45 syl6eq ⊢ A ∈ ℤ ∧ A = 1 → A 2 = 1
47 25 sqvald ⊢ A ∈ ℤ ∧ A = 1 → A 2 = A ⁢ A
48 43 46 47 3eqtr3rd ⊢ A ∈ ℤ ∧ A = 1 → A ⁢ A = 1
49 1cnd ⊢ A ∈ ℤ ∧ A = 1 → 1 ∈ ℂ
50 49 25 25 34 divmuld ⊢ A ∈ ℤ ∧ A = 1 → 1 A = A ↔ A ⁢ A = 1
51 48 50 mpbird ⊢ A ∈ ℤ ∧ A = 1 → 1 A = A
52 39 51 eqtrd ⊢ A ∈ ℤ ∧ A = 1 → inv r ⁡ ℂ fld ⁡ A = A
53 52 37 eqeltrd ⊢ A ∈ ℤ ∧ A = 1 → inv r ⁡ ℂ fld ⁡ A ∈ ℤ
54 cnfldbas ⊢ ℂ = Base ℂ fld
55 cnfld0 ⊢ 0 = 0 ℂ fld
56 cndrng ⊢ ℂ fld ∈ DivRing
57 54 55 56 drngui ⊢ ℂ ∖ 0 = Unit ⁡ ℂ fld
58 eqid ⊢ inv r ⁡ ℂ fld = inv r ⁡ ℂ fld
59 12 57 2 58 subrgunit ⊢ ℤ ∈ SubRing ⁡ ℂ fld → A ∈ Unit ⁡ ℤ ring ↔ A ∈ ℂ ∖ 0 ∧ A ∈ ℤ ∧ inv r ⁡ ℂ fld ⁡ A ∈ ℤ
60 4 59 ax-mp ⊢ A ∈ Unit ⁡ ℤ ring ↔ A ∈ ℂ ∖ 0 ∧ A ∈ ℤ ∧ inv r ⁡ ℂ fld ⁡ A ∈ ℤ
61 36 37 53 60 syl3anbrc ⊢ A ∈ ℤ ∧ A = 1 → A ∈ Unit ⁡ ℤ ring
62 23 61 impbii ⊢ A ∈ Unit ⁡ ℤ ring ↔ A ∈ ℤ ∧ A = 1