# 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}\in \mathrm{Unit}\left({ℤ}_{\mathrm{ring}}\right)↔\left({A}\in ℤ\wedge \left|{A}\right|=1\right)$

### Proof

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