---

Step * of Lemma continuous-rdiv

∀I:Interval. ∀f,g:I ⟶ℝ.
  (f[x] continuous for x ∈ I ⇒ g[x] continuous for x ∈ I ⇒ g[x]≠r0 for x ∈ I ⇒ (f[x]/g[x]) continuous for x ∈ I)
BY
{ ((Auto THEN InstLemma `nonzero-on-implies` [⌜I⌝;⌜g⌝]⋅ THEN Auto)
   THEN (Assert f[x] * (r1/g[x]) continuous for x ∈ I BY
               (ProveRealContinuous THEN Auto))
   THEN ContinuousFunctionality (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I
    {}\mRightarrow{}  g[x]\mneq{}r0  for  x  \mmember{}  I
    {}\mRightarrow{}  (f[x]/g[x])  continuous  for  x  \mmember{}  I)


By

---

Latex:
((Auto  THEN  InstLemma  `nonzero-on-implies`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  f[x]  *  (r1/g[x])  continuous  for  x  \mmember{}  I  BY
                          (ProveRealContinuous  THEN  Auto))
  THEN  ContinuousFunctionality  (-1)
  THEN  Auto)

---

Home Index