This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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