---

Step * of Lemma int-rdiv-cancel

No Annotations
∀a:ℤ. ∀n,m:ℕ+.  ((r(m * a))/m * n = (r(a))/n ∈ ℝ)
BY
{ (Auto
   THEN (Assert (r(m * a))/m * n ∈ ℝ BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN EqTypeCD 
   THEN Auto
   THEN (FunExt  THENA Auto)
   THEN RepUR ``int-to-real int-rdiv`` 0
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN Reduce 0
   THEN Subst' 2 * x * m * a ~ m * 2 * x * a 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\mBbbZ{}.  \mforall{}n,m:\mBbbN{}\msupplus{}.    ((r(m  *  a))/m  *  n  =  (r(a))/n)


By

---

Latex:
(Auto
  THEN  (Assert  (r(m  *  a))/m  *  n  \mmember{}  \mBbbR{}  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD 
  THEN  Auto
  THEN  (FunExt    THENA  Auto)
  THEN  RepUR  ``int-to-real  int-rdiv``  0
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Subst'  2  *  x  *  m  *  a  \msim{}  m  *  2  *  x  *  a  0
  THEN  Auto)

---

Home Index