---

Step * of Lemma rmul-inverse-is-rinv

∀[x:ℝ]. ∀[t:ℝ]. t = rinv(x) supposing (x * t) = r1 supposing x ≠ r0
BY
{ (Auto THEN ((InstLemma `rmul-one` [⌜rinv(x)⌝])⋅ THENA Auto)) }

1
1. x : ℝ
2. x ≠ r0
3. t : ℝ
4. (x * t) = r1
5. (rinv(x) * r1) = rinv(x)
⊢ t = rinv(x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[t:\mBbbR{}].  t  =  rinv(x)  supposing  (x  *  t)  =  r1  supposing  x  \mneq{}  r0


By

---

Latex:
(Auto  THEN  ((InstLemma  `rmul-one`  [\mkleeneopen{}rinv(x)\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index