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}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}ℤ\left[i\right]$
Assertion gzrngunit ${⊢}{A}\in \mathrm{Unit}\left({Z}\right)↔\left({A}\in ℤ\left[i\right]\wedge \left|{A}\right|=1\right)$

Proof

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