---

Step * of Lemma qmul_reverses_qle

∀[a,b,c:ℚ].  uiff(a ≤ b;(c * b) ≤ (c * a)) supposing c < 0
BY
{ ((UnivCD THENA Auto) THEN (Assert 0 < -(c) BY (QAdd ⌜c⌝ 0⋅ THEN Auto))) }

1
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. c < 0
5. 0 < -(c)
⊢ uiff(a ≤ b;(c * b) ≤ (c * a))

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbQ{}].    uiff(a  \mleq{}  b;(c  *  b)  \mleq{}  (c  *  a))  supposing  c  <  0


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Assert  0  <  -(c)  BY  (QAdd  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index