---

Step * 1 1 of Lemma qinv-negative


1. v : ℚ
2. v < 0
3. ¬(v = 0 ∈ ℚ)
4. ¬↑qeq(v;0)
⊢ 0 < 1/v * v
BY
{ (((RWO "qmul_com" 0 THENM RWO "qmul_inv" 0) THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(((RWO  "qmul\_com"  0  THENM  RWO  "qmul\_inv"  0)  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index