Theorem gzrngunitlem

Description: Lemma for gzrngunit . (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypothesis	gzrng.1	$$⊢Z={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]$$
Assertion	gzrngunitlem	$$⊢A\in \mathrm{Unit}\left(Z\right)\to 1\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		gzrng.1	$$⊢Z={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]$$
2		sq1	$$⊢1^2=1$$
3		ax-1ne0	$$⊢1\ne 0$$
4		gzsubrg	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
5	1	subrgring	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to Z\in \mathrm{Ring}$$
6		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
7		subrgsubg	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\left[i\right]\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
8		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
9	1 8	subg0	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_Z$$
10	4 7 9	mp2b	$$⊢0=0_Z$$
11		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
12	1 11	subrg1	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 1=1_Z$$
13	4 12	ax-mp	$$⊢1=1_Z$$
14	6 10 13	0unit	$$⊢Z\in \mathrm{Ring}\to \left(0\in \mathrm{Unit}\left(Z\right)\leftrightarrow 1=0\right)$$
15	4 5 14	mp2b	$$⊢0\in \mathrm{Unit}\left(Z\right)\leftrightarrow 1=0$$
16	3 15	nemtbir	$$⊢\neg 0\in \mathrm{Unit}\left(Z\right)$$
17	1	subrgbas	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\left[i\right]={\mathrm{Base}}_Z$$
18	4 17	ax-mp	$$⊢\mathbb{Z}\left[i\right]={\mathrm{Base}}_Z$$
19	18 6	unitcl	$$⊢A\in \mathrm{Unit}\left(Z\right)\to A\in \mathbb{Z}\left[i\right]$$
20		gzabssqcl	$$⊢A\in \mathbb{Z}\left[i\right]\to {\left|A\right|}^2\in {\mathbb{N}}_0$$
21	19 20	syl	$$⊢A\in \mathrm{Unit}\left(Z\right)\to {\left|A\right|}^2\in {\mathbb{N}}_0$$
22		elnn0	$$⊢{\left|A\right|}^2\in {\mathbb{N}}_0\leftrightarrow \left({\left|A\right|}^2\in \mathbb{N}\vee {\left|A\right|}^2=0\right)$$
23	21 22	sylib	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left({\left|A\right|}^2\in \mathbb{N}\vee {\left|A\right|}^2=0\right)$$
24	23	ord	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(\neg {\left|A\right|}^2\in \mathbb{N}\to {\left|A\right|}^2=0\right)$$
25		gzcn	$$⊢A\in \mathbb{Z}\left[i\right]\to A\in ℂ$$
26	19 25	syl	$$⊢A\in \mathrm{Unit}\left(Z\right)\to A\in ℂ$$
27	26	abscld	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left|A\right|\in ℝ$$
28	27	recnd	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left|A\right|\in ℂ$$
29		sqeq0	$$⊢\left|A\right|\in ℂ\to \left({\left|A\right|}^2=0\leftrightarrow \left|A\right|=0\right)$$
30	28 29	syl	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left({\left|A\right|}^2=0\leftrightarrow \left|A\right|=0\right)$$
31	26	abs00ad	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(\left|A\right|=0\leftrightarrow A=0\right)$$
32		eleq1	$$⊢A=0\to \left(A\in \mathrm{Unit}\left(Z\right)\leftrightarrow 0\in \mathrm{Unit}\left(Z\right)\right)$$
33	32	biimpcd	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(A=0\to 0\in \mathrm{Unit}\left(Z\right)\right)$$
34	31 33	sylbid	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(\left|A\right|=0\to 0\in \mathrm{Unit}\left(Z\right)\right)$$
35	30 34	sylbid	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left({\left|A\right|}^2=0\to 0\in \mathrm{Unit}\left(Z\right)\right)$$
36	24 35	syld	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(\neg {\left|A\right|}^2\in \mathbb{N}\to 0\in \mathrm{Unit}\left(Z\right)\right)$$
37	16 36	mt3i	$$⊢A\in \mathrm{Unit}\left(Z\right)\to {\left|A\right|}^2\in \mathbb{N}$$
38	37	nnge1d	$$⊢A\in \mathrm{Unit}\left(Z\right)\to 1\le {\left|A\right|}^2$$
39	2 38	eqbrtrid	$$⊢A\in \mathrm{Unit}\left(Z\right)\to 1^2\le {\left|A\right|}^2$$
40	26	absge0d	$$⊢A\in \mathrm{Unit}\left(Z\right)\to 0\le \left|A\right|$$
41		1re	$$⊢1\in ℝ$$
42		0le1	$$⊢0\le 1$$
43		le2sq	$$⊢\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\right)\to \left(1\le \left|A\right|\leftrightarrow 1^2\le {\left|A\right|}^2\right)$$
44	41 42 43	mpanl12	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to \left(1\le \left|A\right|\leftrightarrow 1^2\le {\left|A\right|}^2\right)$$
45	27 40 44	syl2anc	$$⊢A\in \mathrm{Unit}\left(Z\right)\to \left(1\le \left|A\right|\leftrightarrow 1^2\le {\left|A\right|}^2\right)$$
46	39 45	mpbird	$$⊢A\in \mathrm{Unit}\left(Z\right)\to 1\le \left|A\right|$$