---

Step * of Lemma qneginv-positive

∀[v:ℚ]. 0 < (-1/v) supposing v < 0
BY
{ xxx(Auto
      THEN (FLemma `qinv-negative` [-1] THENA Auto)
      THEN (FLemma `qless-minus` [-1] THEN Auto THEN (Reduce (-1)) THEN NthHypEq (-1) THEN EqCD THEN Auto)⋅)xxx }

1
.....subterm..... T:t
2:n
1. v : ℚ
2. v < 0
3. (1/v) < 0
4. 0 < -((1/v))
⊢ (-1/v) = -((1/v)) ∈ ℚ

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  (FLemma  `qinv-negative`  [-1]  THENA  Auto)
        THEN  (FLemma  `qless-minus`  [-1]
                    THEN  Auto
                    THEN  (Reduce  (-1))
                    THEN  NthHypEq  (-1)
                    THEN  EqCD
                    THEN  Auto)\mcdot{})xxx

---

Home Index