---

Step * 1 of Lemma qmul_inv


1. r : ℚ
2. ¬(r = 0 ∈ ℚ)
⊢ ↑qeq(r * 1/r;1)
BY
{ (MoveToConcl (-1) THEN (ElimRationals THENA Auto)) }

1
1. r : ℚ
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. r = (p/q) ∈ ℚ
7. ¬↑qeq(q;0)
⊢ (¬((p/q) = 0 ∈ ℚ)) ⇒ (↑qeq((p/q) * 1/(p/q);1))

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  \mneg{}(r  =  0)
\mvdash{}  \muparrow{}qeq(r  *  1/r;1)


By

---

Latex:
(MoveToConcl  (-1)  THEN  (ElimRationals  THENA  Auto))

---

Home Index