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	|- ZZring e/ DivRing

Proof

Step	Hyp	Ref	Expression
1		1ne2	|- 1 =/= 2
2	1	nesymi	|- -. 2 = 1
3		2re	|- 2 e. RR
4		0le2	|- 0 <_ 2
5		absid	|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
6	3 4 5	mp2an	|- ( abs ` 2 ) = 2
7	6	eqeq1i	|- ( ( abs ` 2 ) = 1 <-> 2 = 1 )
8	2 7	mtbir	|- -. ( abs ` 2 ) = 1
9	8	intnan	|- -. ( 2 e. ZZ /\ ( abs ` 2 ) = 1 )
10		zringunit	|- ( 2 e. ( Unit ` ZZring ) <-> ( 2 e. ZZ /\ ( abs ` 2 ) = 1 ) )
11	9 10	mtbir	|- -. 2 e. ( Unit ` ZZring )
12		zringbas	|- ZZ = ( Base ` ZZring )
13		eqid	|- ( Unit ` ZZring ) = ( Unit ` ZZring )
14		zring0	|- 0 = ( 0g ` ZZring )
15	12 13 14	isdrng	|- ( ZZring e. DivRing <-> ( ZZring e. Ring /\ ( Unit ` ZZring ) = ( ZZ \ { 0 } ) ) )
16		2z	|- 2 e. ZZ
17		2ne0	|- 2 =/= 0
18		eldifsn	|- ( 2 e. ( ZZ \ { 0 } ) <-> ( 2 e. ZZ /\ 2 =/= 0 ) )
19	16 17 18	mpbir2an	|- 2 e. ( ZZ \ { 0 } )
20		id	|- ( ( Unit ` ZZring ) = ( ZZ \ { 0 } ) -> ( Unit ` ZZring ) = ( ZZ \ { 0 } ) )
21	19 20	eleqtrrid	|- ( ( Unit ` ZZring ) = ( ZZ \ { 0 } ) -> 2 e. ( Unit ` ZZring ) )
22	15 21	simplbiim	|- ( ZZring e. DivRing -> 2 e. ( Unit ` ZZring ) )
23	11 22	mto	|- -. ZZring e. DivRing
24	23	nelir	|- ZZring e/ DivRing