---

Step * 1 1 1 1 of Lemma qmul_inv


1. r : ℚ
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. r = (p/q) ∈ ℚ
7. ¬↑qeq(q;0)
8. p * 1 ≠ 0 * q
⊢ ↑qeq((p/q) * 1/(p/q);1)
BY
{ (QArithReduce3 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  p  :  \mBbbZ{}
3.  q  :  \mBbbZ{}
4.  0  <  q
5.  \mneg{}(q  =  0)
6.  r  =  (p/q)
7.  \mneg{}\muparrow{}qeq(q;0)
8.  p  *  1  \mneq{}  0  *  q
\mvdash{}  \muparrow{}qeq((p/q)  *  1/(p/q);1)


By

---

Latex:
(QArithReduce3  0  THEN  Auto)\mcdot{}

---

Home Index