Theorem zringndrg

Description: The integers are not a division ring, and therefore not a field. (Contributed by AV, 22-Oct-2021)

	Ref	Expression
Assertion	zringndrg	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\notin \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		1ne2	$$⊢1\ne 2$$
2	1	nesymi	$$⊢\neg 2=1$$
3		2re	$$⊢2\in ℝ$$
4		0le2	$$⊢0\le 2$$
5		absid	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$$
6	3 4 5	mp2an	$$⊢\left|2\right|=2$$
7	6	eqeq1i	$$⊢\left|2\right|=1\leftrightarrow 2=1$$
8	2 7	mtbir	$$⊢\neg \left|2\right|=1$$
9	8	intnan	$$⊢\neg \left(2\in \mathbb{Z}\wedge \left|2\right|=1\right)$$
10		zringunit	$$⊢2\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\leftrightarrow \left(2\in \mathbb{Z}\wedge \left|2\right|=1\right)$$
11	9 10	mtbir	$$⊢\neg 2\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
12		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
13		eqid	$$⊢\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
14		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
15	12 13 14	isdrng	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{DivRing}\leftrightarrow \left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathbb{Z}\setminus \left\{0\right\}\right)$$
16		2z	$$⊢2\in \mathbb{Z}$$
17		2ne0	$$⊢2\ne 0$$
18		eldifsn	$$⊢2\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)\leftrightarrow \left(2\in \mathbb{Z}\wedge 2\ne 0\right)$$
19	16 17 18	mpbir2an	$$⊢2\in \left(\mathbb{Z}\setminus \left\{0\right\}\right)$$
20		id	$$⊢\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathbb{Z}\setminus \left\{0\right\}\to \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathbb{Z}\setminus \left\{0\right\}$$
21	19 20	eleqtrrid	$$⊢\mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathbb{Z}\setminus \left\{0\right\}\to 2\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
22	15 21	simplbiim	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{DivRing}\to 2\in \mathrm{Unit}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
23	11 22	mto	$$⊢\neg {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{DivRing}$$
24	23	nelir	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\notin \mathrm{DivRing}$$