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 ( 𝐴 ∈ ( Unit ‘ ℤring ) ↔ ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) )

Proof

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