---

Step * 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)
⊢ (¬((p/q) = 0 ∈ ℚ)) ⇒ (↑qeq((p/q) * 1/(p/q);1))
BY
{ ((D 0 THENA Auto) THEN (RWW "assert-qeq<" (-1) THENA Auto)) }

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

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWW  "assert-qeq<"  (-1)  THENA  Auto))

---

Home Index