---

Step * 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. ¬↑qeq((p/q);0)
⊢ ↑qeq((p/q) * 1/(p/q);1)
BY
{ (QArithReduce2 (-1) THENA Try (Complete (Auto)))⋅ }

1
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)

---

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.  \mneg{}\muparrow{}qeq((p/q);0)
\mvdash{}  \muparrow{}qeq((p/q)  *  1/(p/q);1)


By

---

Latex:
(QArithReduce2  (-1)  THENA  Try  (Complete  (Auto)))\mcdot{}

---

Home Index