---

Step * of Lemma qmul-ident-div

∀[r,s:ℚ].  ((r/r) * s) = s ∈ ℚ supposing ¬(r = 0 ∈ ℚ)
BY
{ xxx(xxxAutoxxx THEN (RWO "qdiv-self" 0 THENA Auto))xxx }

1
1. r : ℚ
2. s : ℚ
3. ¬(r = 0 ∈ ℚ)
⊢ (1 * s) = s ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[r,s:\mBbbQ{}].    ((r/r)  *  s)  =  s  supposing  \mneg{}(r  =  0)


By

---

Latex:
xxx(xxxAutoxxx  THEN  (RWO  "qdiv-self"  0  THENA  Auto))xxx

---

Home Index