---

Step * of Lemma fps-deriv-div

No Annotations
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ∀[x:X]. ∀[u:|r|].
    d(f÷g)/dx = (((df/dx*g)-(f*dg/dx))÷(g*g)) ∈ PowerSeries(X;r) supposing (g[{}] * u) = 1 ∈ |r| 
  supposing valueall-type(X)
BY
{ (Auto THEN Assert ⌜((g*g)[{}] * (u * u)) = 1 ∈ |r|⌝⋅) }

1
.....assertion..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. x : X
8. u : |r|
9. (g[{}] * u) = 1 ∈ |r|
⊢ ((g*g)[{}] * (u * u)) = 1 ∈ |r|

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. x : X
8. u : |r|
9. (g[{}] * u) = 1 ∈ |r|
10. ((g*g)[{}] * (u * u)) = 1 ∈ |r|
⊢ d(f÷g)/dx = (((df/dx*g)-(f*dg/dx))÷(g*g)) ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:PowerSeries(X;r)].  \mforall{}[x:X].  \mforall{}[u:|r|].
        d(f\mdiv{}g)/dx  =  (((df/dx*g)-(f*dg/dx))\mdiv{}(g*g))  supposing  (g[\{\}]  *  u)  =  1 
    supposing  valueall-type(X)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}((g*g)[\{\}]  *  (u  *  u))  =  1\mkleeneclose{}\mcdot{})

---

Home Index