---

Step * 1 of Lemma non-neg-qmul


1. a : ℚ
2. b : ℚ
⊢ (0 ≤ a) ⇒ (0 ≤ b) ⇒ (0 ≤ (a * b))
BY
{ xxx((RWO "qle-iff" 0 THEN Auto) THEN D -2)xxx }

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

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

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  (0  \mleq{}  a)  {}\mRightarrow{}  (0  \mleq{}  b)  {}\mRightarrow{}  (0  \mleq{}  (a  *  b))


By

---

Latex:
xxx((RWO  "qle-iff"  0  THEN  Auto)  THEN  D  -2)xxx

---

Home Index