---

Step * of Lemma qdiv-non-neg

∀a,b:ℚ.  (0 < b ∧ (0 ≤ a)) ∨ (b < 0 ∧ (a ≤ 0)) ⇐⇒ 0 ≤ (a/b) supposing ¬(b = 0 ∈ ℚ)
BY
{ xxx(xxxAutoxxx THEN SplitOrHyps)xxx }

1
1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. 0 < b ∧ (0 ≤ a)
⊢ 0 ≤ (a/b)

2
1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. b < 0 ∧ (a ≤ 0)
⊢ 0 ≤ (a/b)

3
1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. 0 ≤ (a/b)
⊢ (0 < b ∧ (0 ≤ a)) ∨ (b < 0 ∧ (a ≤ 0))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbQ{}.    (0  <  b  \mwedge{}  (0  \mleq{}  a))  \mvee{}  (b  <  0  \mwedge{}  (a  \mleq{}  0))  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  (a/b)  supposing  \mneg{}(b  =  0)


By

---

Latex:
xxx(xxxAutoxxx  THEN  SplitOrHyps)xxx

---

Home Index