---

Step * of Lemma qmul_preserves_qle2

∀[a,b,c:ℚ].  ((c * a) ≤ (c * b)) supposing ((a ≤ b) and (0 ≤ c))
BY
{ ((UnivCD THENA Auto) THEN (((RWO "qle-iff" (-2)) THENM D -2) THENA Auto)) }

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

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (((RWO  "qle-iff"  (-2))  THENM  D  -2)  THENA  Auto))

---

Home Index