---

Step * of Lemma rat2real-qdiv

∀a:ℚ. ∀b:ℤ-o.  (rat2real((a/b)) = (rat2real(a)/r(b)))
BY
{ (Auto
   THEN ElimRationals
   THEN Auto
   THEN (InstLemma `mk-rational-qdiv` [⌜p⌝;⌜q⌝]⋅ THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)
   THEN RepUR ``rat2real mk-rational qdiv qmul`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN RepUR ``qinv`` 0
   THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))
   THEN 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)
⊢ (r(p * 1))/q * b = ((r(p))/q/r(b))

---

Latex:

---

Latex:
\mforall{}a:\mBbbQ{}.  \mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}.    (rat2real((a/b))  =  (rat2real(a)/r(b)))


By

---

Latex:
(Auto
  THEN  ElimRationals
  THEN  Auto
  THEN  (InstLemma  `mk-rational-qdiv`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  RepUR  ``rat2real  mk-rational  qdiv  qmul``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepUR  ``qinv``  0
  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
  THEN  Auto)

---

Home Index