---

Step * of Lemma qmul_preserves_qle

No Annotations
∀[a,b,c:ℚ].  uiff(a ≤ b;(c * a) ≤ (c * b)) supposing 0 < c
BY
{ ((UnivCD THENA Auto)
   THEN (All (RWO "qle-iff"))
   THEN Auto
   THEN Unhide
   THEN Auto
   THEN ParallelLast
   THEN Try ((BLemma `qmul_preserves_qless` THEN Auto))
   THEN Try ((FLemma `qmul_preserves_qless` [-1] THEN Auto))
   THEN Try ((EqCD THEN Auto))) }

1
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. 0 < c
5. (c * a) = (c * b) ∈ ℚ
⊢ a = b ∈ ℚ

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (All  (RWO  "qle-iff"))
  THEN  Auto
  THEN  Unhide
  THEN  Auto
  THEN  ParallelLast
  THEN  Try  ((BLemma  `qmul\_preserves\_qless`  THEN  Auto))
  THEN  Try  ((FLemma  `qmul\_preserves\_qless`  [-1]  THEN  Auto))
  THEN  Try  ((EqCD  THEN  Auto)))

---

Home Index