---

Step * 1 of Lemma qmul-zero-div

.....equality..... 
1. a : ℚ
2. b : ℤ-o
⊢ (0/b) = 0 ∈ ℚ
BY
{ xxx(D -1 THEN xxxUnfold `qdiv` 0xxx THEN xxx(QNorm 0 THEN Auto)xxx)xxx }

1
1. a : ℚ
2. b : ℤ
3. b ≠ 0
⊢ ¬↑qeq(b;0)

---

Latex:

---

Latex:
.....equality..... 
1.  a  :  \mBbbQ{}
2.  b  :  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  (0/b)  =  0


By

---

Latex:
xxx(D  -1  THEN  xxxUnfold  `qdiv`  0xxx  THEN  xxx(QNorm  0  THEN  Auto)xxx)xxx

---

Home Index