---

Step * of Lemma int-rinv-cancel

∀[a:ℤ]. ∀[b:ℤ-o]. ∀[x:ℝ].  ((r(a * b) * rinv(r(b)) * x) = (r(a) * x))
BY
{ (Auto
   THEN (RWO "rmul_assoc<" 0 THENM BLemma `rmul_functionality`)
   THEN Auto
   THEN RWW "rmul-int< rmul_assoc rmul-rinv1" 0
   THEN Auto) }

1
.....rewrite subgoal..... 
1. a : ℤ
2. b : ℤ-o
3. x : ℝ
⊢ rnonzero(r(b))

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[x:\mBbbR{}].    ((r(a  *  b)  *  rinv(r(b))  *  x)  =  (r(a)  *  x))


By

---

Latex:
(Auto
  THEN  (RWO  "rmul\_assoc<"  0  THENM  BLemma  `rmul\_functionality`)
  THEN  Auto
  THEN  RWW  "rmul-int<  rmul\_assoc  rmul-rinv1"  0
  THEN  Auto)

---

Home Index