---

Step * of Lemma qabs-non-zero

∀[q:ℚ]. uiff(0 < |q|;¬(q = 0 ∈ ℚ))
BY
{ Auto }

1
1. q : ℚ
2. 0 < |q|
⊢ ¬(q = 0 ∈ ℚ)

2
1. q : ℚ
2. ¬(q = 0 ∈ ℚ)
⊢ 0 < |q|

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  uiff(0  <  |q|;\mneg{}(q  =  0))


By

---

Latex:
Auto

---

Home Index