---

Step * of Lemma qabs-positive-iff

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index