---

Step * of Lemma qinv-negative

∀[v:ℚ]. (1/v) < 0 supposing v < 0
BY
{ (Auto
   THEN (Assert ¬(v = 0 ∈ ℚ) BY
               (RelRST THEN Auto))
   THEN Auto
   THEN (Assert ¬↑qeq(v;0) BY
               (RW assert_pushdownC 0 THEN Auto))
   THEN (InstLemma `qmul-positive` [⌜v⌝;⌜(1/v)⌝]⋅ THENA Auto)
   THEN D -1
   THEN (Thin (-2))
   THEN D -1) }

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

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

---

Latex:

---

Latex:
\mforall{}[v:\mBbbQ{}].  (1/v)  <  0  supposing  v  <  0


By

---

Latex:
(Auto
  THEN  (Assert  \mneg{}(v  =  0)  BY
                          (RelRST  THEN  Auto))
  THEN  Auto
  THEN  (Assert  \mneg{}\muparrow{}qeq(v;0)  BY
                          (RW  assert\_pushdownC  0  THEN  Auto))
  THEN  (InstLemma  `qmul-positive`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}(1/v)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Thin  (-2))
  THEN  D  -1)

---

Home Index