---

Step * 1 1 2 1 of Lemma fractional-part-rep

.....assertion..... 
1. p : ℤ
2. q : ℤ
3. (p/q) ∈ ℚ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
7. 0 ≤ (p/q)
8. (p/q) < 1
9. ¬(0 ≤ q)
⊢ (p/q) = (-p/-q) ∈ ℚ
BY
{ xxx(QMul ⌜-q⌝ 0⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  \mBbbZ{}
2.  q  :  \mBbbZ{}
3.  (p/q)  \mmember{}  \mBbbQ{}
4.  0  <  q
5.  \mneg{}(q  =  0)
6.  \mneg{}\muparrow{}qeq(q;0)
7.  0  \mleq{}  (p/q)
8.  (p/q)  <  1
9.  \mneg{}(0  \mleq{}  q)
\mvdash{}  (p/q)  =  (-p/-q)


By

---

Latex:
xxx(QMul  \mkleeneopen{}-q\mkleeneclose{}  0\mcdot{}  THEN  Auto)xxx

---

Home Index