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({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
2		eqid	$$⊢\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
3	1 2	unitcl	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to A\in \mathbb{Z}$$
4		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
5		zgz	$$⊢x\in \mathbb{Z}\to x\in \mathbb{Z}\left[i\right]$$
6	5	ssriv	$$⊢\mathbb{Z}\subseteq \mathbb{Z}\left[i\right]$$
7		gzsubrg	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
8		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]$$
9	8	subsubrg	$$⊢\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \left(\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)\leftrightarrow \left(\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \mathbb{Z}\subseteq \mathbb{Z}\left[i\right]\right)\right)$$
10	7 9	ax-mp	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)\leftrightarrow \left(\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \mathbb{Z}\subseteq \mathbb{Z}\left[i\right]\right)$$
11	4 6 10	mpbir2an	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)$$
12		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
13		ressabs	$$⊢\left(\mathbb{Z}\left[i\right]\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \mathbb{Z}\subseteq \mathbb{Z}\left[i\right]\right)\to \left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right){\upharpoonright }_{𝑠}\mathbb{Z}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
14	7 6 13	mp2an	$$⊢\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right){\upharpoonright }_{𝑠}\mathbb{Z}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
15	12 14	eqtr4i	$$⊢{\mathbb{Z}}_{\mathrm{ring}}=\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right){\upharpoonright }_{𝑠}\mathbb{Z}$$
16		eqid	$$⊢\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)$$
17	15 16 2	subrguss	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)\to \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\subseteq \mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)$$
18	11 17	ax-mp	$$⊢\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\subseteq \mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)$$
19	18	sseli	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to A\in \mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)$$
20	8	gzrngunit	$$⊢A\in \mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)\leftrightarrow \left(A\in \mathbb{Z}\left[i\right]\wedge \left|A\right|=1\right)$$
21	20	simprbi	$$⊢A\in \mathrm{Unit}\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}\left[i\right]\right)\to \left|A\right|=1$$
22	19 21	syl	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to \left|A\right|=1$$
23	3 22	jca	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to \left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)$$
24		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
25	24	adantr	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to A\in ℂ$$
26		simpr	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to \left|A\right|=1$$
27		ax-1ne0	$$⊢1\ne 0$$
28	27	a1i	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to 1\ne 0$$
29	26 28	eqnetrd	$$⊢\left(A\in \mathbb{Z}\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	eqtrdi	$$⊢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 \mathbb{Z}\wedge \left|A\right|=1\right)\to A\ne 0$$
35		eldifsn	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(A\in ℂ\wedge A\ne 0\right)$$
36	25 34 35	sylanbrc	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to A\in \left(ℂ\setminus \left\{0\right\}\right)$$
37		simpl	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to A\in \mathbb{Z}$$
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 \mathbb{Z}\wedge \left|A\right|=1\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=\frac{1}{A}$$
40		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
41	40	adantr	$$⊢\left(A\in \mathbb{Z}\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 \mathbb{Z}\wedge \left|A\right|=1\right)\to {\left|A\right|}^2=A^2$$
44	26	oveq1d	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to {\left|A\right|}^2=1^2$$
45		sq1	$$⊢1^2=1$$
46	44 45	eqtrdi	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to {\left|A\right|}^2=1$$
47	25	sqvald	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to A^2=AA$$
48	43 46 47	3eqtr3rd	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to AA=1$$
49		1cnd	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to 1\in ℂ$$
50	49 25 25 34	divmuld	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to \left(\frac{1}{A}=A\leftrightarrow AA=1\right)$$
51	48 50	mpbird	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to \frac{1}{A}=A$$
52	39 51	eqtrd	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=A$$
53	52 37	eqeltrd	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\in \mathbb{Z}$$
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	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \left(A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge A\in \mathbb{Z}\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\in \mathbb{Z}\right)\right)$$
60	4 59	ax-mp	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge A\in \mathbb{Z}\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\in \mathbb{Z}\right)$$
61	36 37 53 60	syl3anbrc	$$⊢\left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)\to A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
62	23 61	impbii	$$⊢A\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left(A\in \mathbb{Z}\wedge \left|A\right|=1\right)$$