---

Step * of Lemma derivative-rdiv

∀I:Interval. ∀f1,f2,g1,g2:I ⟶ℝ.
  ((∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g1[x] = g1[y])))
  ⇒ (∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (g2[x] = g2[y])))
  ⇒ f2[x]≠r0 for x ∈ I
  ⇒ (∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f2[x] = f2[y])))
  ⇒ d(f1[x])/dx = λx.g1[x] on I
  ⇒ d(f2[x])/dx = λx.g2[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
{ (Auto
   THEN (InstLemma `derivative-rinv` [⌜I⌝;⌜f2⌝;⌜g2⌝]⋅ THENA Auto)
   THEN (InstLemma `nonzero-on-implies` [⌜I⌝;⌜f2⌝]⋅ THENA Auto)
   THEN (InstLemma `derivative-mul` [⌜I⌝;⌜f1⌝;⌜λ2x.(r1/f2[x])⌝;⌜g1⌝;⌜λ2x.(-(g2[x])/f2[x] * f2[x])⌝]⋅
         THENA (Auto
                THEN Try ((RepUR ``so_lambda r-ap`` 0 THEN (MemTypeCD THEN Reduce 0) THEN Auto))
                THEN Repeat (First [BLemma `rdiv_functionality`
                                   ; BLemma `rminus_functionality` 
                                   ; BLemma `rmul_functionality`
                                   ; BLemma `rmul-nonzero`
                                   ; BackThruSomeHyp
                                   ] THENA Auto⋅)
                THEN Auto)
         )) }

1
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

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f1,f2,g1,g2:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g1[x]  =  g1[y])))
    {}\mRightarrow{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g2[x]  =  g2[y])))
    {}\mRightarrow{}  f2[x]\mneq{}r0  for  x  \mmember{}  I
    {}\mRightarrow{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f2[x]  =  f2[y])))
    {}\mRightarrow{}  d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
    {}\mRightarrow{}  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
    {}\mRightarrow{}  d((f1[x]/f2[x]))/dx  =  \mlambda{}x.((f2[x]  *  g1[x])  -  f1[x]  *  g2[x]/f2[x]  *  f2[x])  on  I)


By

---

Latex:
(Auto
  THEN  (InstLemma  `derivative-rinv`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{};\mkleeneopen{}g2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `nonzero-on-implies`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `derivative-mul`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(r1/f2[x])\mkleeneclose{};\mkleeneopen{}g1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(-(g2[x])/f2[x]  *  f2[x])\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((RepUR  ``so\_lambda  r-ap``  0  THEN  (MemTypeCD  THEN  Reduce  0)  THEN  Auto))
                            THEN  Repeat  (First  [BLemma  `rdiv\_functionality`
                                                                  ;  BLemma  `rminus\_functionality` 
                                                                  ;  BLemma  `rmul\_functionality`
                                                                  ;  BLemma  `rmul-nonzero`
                                                                  ;  BackThruSomeHyp
                                                                  ]  THENA  Auto\mcdot{})
                            THEN  Auto)
              ))

---

Home Index