---

Step * 1 of Lemma qinv-negative

.....antecedent..... 
1. v : ℚ
2. v < 0
3. ¬(v = 0 ∈ ℚ)
4. ¬↑qeq(v;0)
⊢ 0 < v * (1/v)
BY
{ (RepUR ``qdiv`` 0 THEN QNorm 0) }

1
1. v : ℚ
2. v < 0
3. ¬(v = 0 ∈ ℚ)
4. ¬↑qeq(v;0)
⊢ 0 < 1/v * v

---

Latex:

---

Latex:
.....antecedent..... 
1.  v  :  \mBbbQ{}
2.  v  <  0
3.  \mneg{}(v  =  0)
4.  \mneg{}\muparrow{}qeq(v;0)
\mvdash{}  0  <  v  *  (1/v)


By

---

Latex:
(RepUR  ``qdiv``  0  THEN  QNorm  0)

---

Home Index