---

Step * 2 1 of Lemma int_ring_wf


0 ≠ 1 ∧ (∀u,v:ℤ.  ((¬(v = 0 ∈ ℤ)) ⇒ ((u * v) = 0 ∈ ℤ) ⇒ (u = 0 ∈ ℤ)))
BY
{ Auto 
 }

1
1. 0 ≠ 1
2. u : ℤ
3. v : ℤ
4. ¬(v = 0 ∈ ℤ)
5. (u * v) = 0 ∈ ℤ
⊢ u = 0 ∈ ℤ

---

Latex:

---

Latex:

0  \mneq{}  1  \mwedge{}  (\mforall{}u,v:\mBbbZ{}.    ((\mneg{}(v  =  0))  {}\mRightarrow{}  ((u  *  v)  =  0)  {}\mRightarrow{}  (u  =  0)))


By

---

Latex:
Auto 

---

Home Index