---

Step * 1 of Lemma derivative-rdiv


1. I : Interval
2. f1 : I ⟶ℝ
3. f2 : I ⟶ℝ
4. g1 : I ⟶ℝ
5. g2 : I ⟶ℝ
6. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g1[x] = g1[y]))
7. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g2[x] = g2[y]))
8. f2[x]≠r0 for x ∈ I
9. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f2[x] = f2[y]))
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. d((r1/f2[x]))/dx = λx.(-(g2[x])/f2[x] * f2[x]) on I
13. ∀x:ℝ. ((x ∈ I) ⇒ f2[x] ≠ r0)
14. d(f1[x] * (r1/f2[x]))/dx = λx.(f1[x] * (-(g2[x])/f2[x] * f2[x])) + ((r1/f2[x]) * g1[x]) on I
⊢ d((f1[x]/f2[x]))/dx = λx.((f2[x] * g1[x]) - f1[x] * g2[x]/f2[x] * f2[x]) on I
BY
{ (DerivativeFunctionality (-1) THEN Auto THEN BLemma `rmul-nonzero` THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f1  :  I  {}\mrightarrow{}\mBbbR{}
3.  f2  :  I  {}\mrightarrow{}\mBbbR{}
4.  g1  :  I  {}\mrightarrow{}\mBbbR{}
5.  g2  :  I  {}\mrightarrow{}\mBbbR{}
6.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g1[x]  =  g1[y]))
7.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g2[x]  =  g2[y]))
8.  f2[x]\mneq{}r0  for  x  \mmember{}  I
9.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f2[x]  =  f2[y]))
10.  d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
11.  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
12.  d((r1/f2[x]))/dx  =  \mlambda{}x.(-(g2[x])/f2[x]  *  f2[x])  on  I
13.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  f2[x]  \mneq{}  r0)
14.  d(f1[x]  *  (r1/f2[x]))/dx  =  \mlambda{}x.(f1[x]  *  (-(g2[x])/f2[x]  *  f2[x]))  +  ((r1/f2[x])  *  g1[x])  on  I
\mvdash{}  d((f1[x]/f2[x]))/dx  =  \mlambda{}x.((f2[x]  *  g1[x])  -  f1[x]  *  g2[x]/f2[x]  *  f2[x])  on  I


By

---

Latex:
(DerivativeFunctionality  (-1)  THEN  Auto  THEN  BLemma  `rmul-nonzero`  THEN  Auto)

---

Home Index