---

Step * 1 of Lemma rat2real-qdiv


1. a : ℚ
2. b : ℤ-o
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. a = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. mk-rational(p;q) ~ (p/q)
⊢ (r(p * 1))/q * b = ((r(p))/q/r(b))
BY
{ ((Assert q * b ∈ ℤ-o BY Auto) THEN (nRMul ⌜r(b)⌝ 0⋅ THENA Auto)) }

1
1. a : ℚ
2. b : ℤ-o
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. a = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
9. mk-rational(p;q) ~ (p/q)
10. q * b ∈ ℤ-o
⊢ ((r(p))/q * b * r(b)) = (r(p))/q

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  0  <  q
6.  \mneg{}(q  =  0)
7.  a  =  (p/q)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  mk-rational(p;q)  \msim{}  (p/q)
\mvdash{}  (r(p  *  1))/q  *  b  =  ((r(p))/q/r(b))


By

---

Latex:
((Assert  q  *  b  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}  BY  Auto)  THEN  (nRMul  \mkleeneopen{}r(b)\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index