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	⊢ ℤring ∉ DivRing

Proof

Step	Hyp	Ref	Expression
1		1ne2	⊢ 1 ≠ 2
2	1	nesymi	⊢ ¬ 2 = 1
3		2re	⊢ 2 ∈ ℝ
4		0le2	⊢ 0 ≤ 2
5		absid	⊢ ( ( 2 ∈ ℝ ∧ 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 ∈ ℤ ∧ ( abs ‘ 2 ) = 1 )
10		zringunit	⊢ ( 2 ∈ ( Unit ‘ ℤring ) ↔ ( 2 ∈ ℤ ∧ ( abs ‘ 2 ) = 1 ) )
11	9 10	mtbir	⊢ ¬ 2 ∈ ( Unit ‘ ℤring )
12		zringbas	⊢ ℤ = ( Base ‘ ℤring )
13		eqid	⊢ ( Unit ‘ ℤring ) = ( Unit ‘ ℤring )
14		zring0	⊢ 0 = ( 0g ‘ ℤring )
15	12 13 14	isdrng	⊢ ( ℤring ∈ DivRing ↔ ( ℤring ∈ Ring ∧ ( Unit ‘ ℤring ) = ( ℤ ∖ { 0 } ) ) )
16		2z	⊢ 2 ∈ ℤ
17		2ne0	⊢ 2 ≠ 0
18		eldifsn	⊢ ( 2 ∈ ( ℤ ∖ { 0 } ) ↔ ( 2 ∈ ℤ ∧ 2 ≠ 0 ) )
19	16 17 18	mpbir2an	⊢ 2 ∈ ( ℤ ∖ { 0 } )
20		id	⊢ ( ( Unit ‘ ℤring ) = ( ℤ ∖ { 0 } ) → ( Unit ‘ ℤring ) = ( ℤ ∖ { 0 } ) )
21	19 20	eleqtrrid	⊢ ( ( Unit ‘ ℤring ) = ( ℤ ∖ { 0 } ) → 2 ∈ ( Unit ‘ ℤring ) )
22	15 21	simplbiim	⊢ ( ℤring ∈ DivRing → 2 ∈ ( Unit ‘ ℤring ) )
23	11 22	mto	⊢ ¬ ℤring ∈ DivRing
24	23	nelir	⊢ ℤring ∉ DivRing