```
(def-constant deriv
"lambda(f:[ii,uu],x:ii, rlim(lambda(z:ii,(z-x)^[-1]*(f(z)-f(x))),x))"
(theory mappings-from-an-interval-to-a-normed-space))
```

```
(def-theorem characterization-of-derivative
"forall(x:ii,f:[ii,uu],v:uu,
deriv(f,x)=v
iff
forall(eps:rr,
0<eps
implies
forsome(z_0:ii,
x<z_0
and
forall(z:ii,
x<z and z<=z_0
implies
norm((z-x)^[-1]*(f(z)-f(x))-v)<=eps))))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(

(unfold-single-defined-constant (0) deriv)
(apply-macete-with-minor-premises iota-free-characterization-of-rlim)
beta-reduce-repeatedly
)))
```

```
(def-theorem existence-of-derivative
"forall(x:ii,f:[ii,uu],
#(deriv(f,x))
iff
forsome(v:uu,
forall(eps:rr,
0<eps
implies
forsome(z_0:ii,
x<z_0
and
forall(z:ii,
x<z and z<=z_0
implies
norm((z-x)^[-1]*(f(z)-f(x))-v)<=eps)))))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "deriv(f,x)=deriv(f,x)")
(incorporate-antecedent "deriv(f,x)=deriv(f,x)")
(apply-macete-with-minor-premises characterization-of-derivative)
direct-inference
(instantiate-existential ("deriv(f,x)"))
(cut-with-single-formula "deriv(f,x)=v")
(apply-macete-with-minor-premises characterization-of-derivative)
)))
```

```
(def-theorem derivative-at-point-bound-lemma
"forall(x:ii,f:[ii,uu],m:rr,
norm(deriv(f,x))<=m
implies
forall(m_0:rr,z_0:ii,
m<m_0 and x<z_0
implies
forsome(z:ii,
x<z and z<=z_0 and norm(f(z)-f(x))<=m_0*(z-x))))"
(theory mappings-from-an-interval-to-a-normed-space)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "deriv(f,x)=deriv(f,x)")
(incorporate-antecedent "deriv(f,x)=deriv(f,x)")
(apply-macete-with-minor-premises characterization-of-derivative)
(force-substitution "(z-x)^[-1]*(f(z)-f(x))-deriv(f,x)"
"1/(z-x)*((f(z)-f(x))-(z-x)*deriv(f,x))" (0))
(apply-macete-with-minor-premises norm-scalar-multiplication)
(apply-macete-with-minor-premises absolute-value-quotient)
(force-substitution "abs(1)/abs(z-x)*norm(f(z)-f(x)-(z-x)*deriv(f,x))<=eps"
"norm(f(z)-f(x)-(z-x)*deriv(f,x))<=eps*(z-x)" (0))
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,  forall(eps:rr, 0<eps implies p))"
("m_0-m"))
simplify
(cut-with-single-formula "forsome(w:ii,x<w and w<=z_\$0 and w<=z_0)")
(antecedent-inference "with(z_0,z_\$0,x:ii,forsome(w:ii,x<w and w<=z_\$0 and w<=z_0));")
(instantiate-existential ("w"))
(instantiate-universal-antecedent "with(m,m_0:rr,f:[ii,uu],z_\$0,x:ii,
forall(z:ii,
x<z and z<=z_\$0
implies
norm(f(z)-f(x)-(z-x)*deriv(f,x))<=(m_0-m)*(z-x)));" ("w"))
(cut-with-single-formula
"norm(f(w)-f(x))-norm((w-x)*deriv(f,x))<=norm(f(w)-f(x)-(w-x)*deriv(f,x))")
(cut-with-single-formula "norm((w-x)*deriv(f,x))<=m*(w-x)")
simplify
(apply-macete-with-minor-premises norm-scalar-multiplication)
(apply-macete-with-minor-premises absolute-value-non-negative)
simplify
(apply-macete-with-minor-premises norm-continuity-lemma)
(instantiate-existential ("min(z_0,z_\$0)"))
(unfold-single-defined-constant (0) min)
(case-split ("z_0<=z_\$0"))
simplify
simplify
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises interval-characterization)
(instantiate-existential ("z_0" "x"))
simplify
(apply-macete-with-minor-premises absolute-value-non-negative)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
(apply-macete-with-minor-premises ns-fractional-expression-manipulation)
simplify
)))

```

```(def-transported-symbols ii%locally%lipschitz%bound
(translation mapint-to-mapint-normed-space)
(renamer identity))
```

```
(def-theorem derivative-bound-lemma
"forall(f:[ii,uu], m:rr,
0<m and forall(x:ii,forsome(y:ii,x<y) implies norm(deriv(f,x))<=m)
implies
forall(m_0:rr,m<m_0 implies ii%locally%lipschitz%bound(f,m_0)))"

(theory mappings-from-an-interval-to-a-normed-space)
(proof
(
(unfold-single-defined-constant (0) ii%locally%lipschitz%bound)
(apply-macete-with-minor-premises derivative-at-point-bound-lemma)
direct-and-antecedent-inference-strategy
simplify
(instantiate-existential ("m"))
(backchain "with(p:prop,  forall(x:ii,p))")
(instantiate-existential ("z"))
)))
```

```
(def-theorem mean-value-theorem
"forall(f:[ii,uu], m:rr, total_q{f,[ii,uu]} and continuous(f)
and 0<m and forall(x:ii,forsome(y:ii,x<y) implies norm(deriv(f,x))<=m)
implies
lipschitz%bound(f,m))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%locally-lipschitz-implies-lipschitz-plus)
(apply-macete-with-minor-premises derivative-bound-lemma)
direct-and-antecedent-inference-strategy
(instantiate-existential ("m"))
)))
```

```
(def-theorem constant-function-lipschitz-characterization
"forall(f:[pp_0,pp_1], total_q{f,[pp_0,pp_1]} and
forall(m:rr, 0<m implies lipschitz%bound(f,m)) implies
forall(x,y:pp_0,f(x)=f(y)))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
(proof
(
unfold-defined-constants
unfold-defined-constants
direct-and-antecedent-inference-strategy
(case-split ("0<dist_0(x,y)"))
(apply-macete-with-minor-premises tr%point-separation-for-distance)
(case-split ("0<dist_1(f(x),f(y))"))
(cut-with-single-formula
"dist_1(f(x),f(y))<=[1/2]*(dist_1(f(x),f(y))/dist_0(x,y))*dist_0(x,y)")
(cut-with-single-formula
"[1/2]*(dist_1(f(x),f(y))/dist_0(x,y))*dist_0(x,y)=[1/2]*dist_1(f(x),f(y))")
(contrapose "with(y,x:pp_0,f:[pp_0,pp_1],0<dist_1(f(x),f(y)));")
simplify
simplify
(backchain "with(p:prop, forall(m:rr, 0<m implies p))")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
simplify-insistently
simplify-insistently
(cut-with-single-formula "0<=dist_1(f(x),f(y))")
simplify
(apply-macete-with-minor-premises tr%positivity-of-distance)
(cut-with-single-formula "x=y")
simplify
(apply-macete-with-minor-premises tr%point-separation-for-distance)
(cut-with-single-formula "0<=dist_0(x,y)")
simplify
(apply-macete-with-minor-premises tr%positivity-of-distance)
)))
```

```
(def-theorem ms-constant-continuous
"forall(y:pp_1,x:pp_0, continuous%at%point(lambda(x:pp_0,y),x))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-existential ("1"))
simplify
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
)))
```

```
(def-theorem mean-value-theorem-corollary-0
"forall(f:[ii,uu],
total_q{f,[ii,uu]}
and
continuous(f)
and
forall(x:ii,forsome(y:ii,x<y) implies deriv(f,x)=v0)
implies
forall(x,y:ii,f(x)=f(y)))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%constant-function-lipschitz-characterization)
(apply-macete-with-minor-premises mean-value-theorem)
direct-and-antecedent-inference-strategy
(backchain "with(f:[ii,uu], forall(x:ii,forsome(y:ii,x<y) implies deriv(f,x)=v0))")
direct-and-antecedent-inference-strategy
auto-instantiate-existential
simplify
)))
```

```
"forall(f,g:[ii,uu],x:ii,
#(deriv(f,x)) and #(deriv(g,x))
implies
deriv(lambda(x:ii,f(x)+g(x)),x)=deriv(f,x)+deriv(g,x))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(

(unfold-single-defined-constant-globally deriv)
(force-substitution
"(z_\$0-x)^[-1]*((f(z_\$0)+g(z_\$0))-(f(x)+g(x)))"
"lambda(z_\$0:ii,(z_\$0-x)^[-1]*(f(z_\$0)-f(x)))(z_\$0)+
lambda(z_\$0:ii,(z_\$0-x)^[-1]*(g(z_\$0)-g(x)))(z_\$0)"
(0))
(move-to-sibling 1)
simplify
simplify
)))
```

```
(def-theorem deriv-of-constant
"forall(c:uu,x:ii, forsome(y:ii,x<y) implies deriv(lambda(x:ii,c),x)=v0)"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises characterization-of-derivative)
direct-and-antecedent-inference-strategy
beta-reduce-repeatedly
simplify
(instantiate-existential ("y"))
)))
```

```
(def-theorem homogeneity-of-deriv
"forall(f:[ii,uu],a:rr,x:ii,
#(deriv(f,x))
implies
deriv(lambda(x:ii,a*f(x)),x)=a*deriv(f,x))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(

(unfold-single-defined-constant-globally deriv)
(force-substitution "(z_\$0-x)^[-1]*(a*f(z_\$0)-a*f(x))"
"a*lambda(z_\$0:ii,(z_\$0-x)^[-1]*(f(z_\$0)-f(x)))(z_\$0)"
(0))
(move-to-sibling 1)
simplify
(apply-macete-with-minor-premises rlim-homogeneity)
simplify
)))
```

```
(def-theorem ns-sum-of-continuous-is-continuous
"forall(f,g:[ii,uu], x:ii,
continuous%at%point(f,x) and continuous%at%point(g,x)
implies
continuous%at%point(lambda(x:ii,f(x)+g(x)),x))"
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("eps_\$0/2"))
(simplify-antecedent "with(p:prop, not(p))")
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("eps_\$0/2"))
(simplify-antecedent "with(p:prop, not(p))")
(cut-with-single-formula "min(delta,delta_\$0)<=delta and min(delta,delta_\$0)<=delta_\$0")
(instantiate-existential ("min(delta,delta_\$0)"))
unfold-defined-constants
(case-split ("delta<=delta_\$0"))
simplify
simplify
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("norm(f(x)-f(y_\$1))+norm(g(x)-g(y_\$1))"))
(force-substitution "(f(x)+g(x))-(f(y_\$1)+g(y_\$1))" "(f(x)-f(y_\$1))+(g(x)-g(y_\$1))" (0))
(apply-macete-with-minor-premises norm-triangle-inequality)
(cut-with-single-formula "norm(g(x)-g(y_\$1))<=eps_\$0/2")
simplify
(backchain "with(eps_\$0:rr,g:[ii,uu],delta:rr,x:ii,
forall(y:ii,
abs(x-y)<=delta implies norm(g(x)-g(y))<=eps_\$0/2));")
simplify
(cut-with-single-formula "norm(f(x)-f(y_\$1))<=eps_\$0/2")
simplify
(backchain "with(eps_\$0:rr,f:[ii,uu],delta_\$0:rr,x:ii,
forall(y:ii,
abs(x-y)<=delta_\$0 implies norm(f(x)-f(y))<=eps_\$0/2));")
simplify
simplify
(cut-with-single-formula "norm(g(x)-g(y_\$1))<=eps_\$0/2 and norm(f(x)-f(y_\$1))<=eps_\$0/2")
simplify
direct-inference
direct-and-antecedent-inference-strategy
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises minimum-2nd-arg)
)
)
(usages transportable-macete)
(theory mappings-from-an-interval-to-a-normed-space))
```

```
(def-theorem ns-multiple-of-continuous-is-continuous
"forall(f:[ii,uu], x:ii, a:rr,
continuous%at%point(f,x)
implies
continuous%at%point(lambda(x:ii,a*f(x)),x))"
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(case-split ("a=0"))
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
(simplify-antecedent "not(0<1);")
(instantiate-existential ("delta"))
simplify
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))"
("eps_\$0/abs(a)"))
(contrapose "with(a,eps_\$0:rr,not(0<eps_\$0/abs(a)));")
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(weaken (0 2))
(unfold-single-defined-constant (0) abs)
(case-split ("0<=a"))
simplify
simplify
(instantiate-existential ("delta"))
(force-substitution "a*f(x)-a*f(y_\$0)" "a*(f(x)-f(y_\$0))" (0))
(apply-macete-with-minor-premises norm-scalar-multiplication)
(instantiate-universal-antecedent "with(a,eps_\$0:rr,f:[ii,uu],delta:rr,x:ii,
forall(y:ii,
abs(x-y)<=delta implies norm(f(x)-f(y))<=eps_\$0/abs(a)));" ("y_\$0"))
(incorporate-antecedent "with(a,eps_\$0:rr,y_\$0,x:ii,f:[ii,uu],
norm(f(x)-f(y_\$0))<=eps_\$0/abs(a));")
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(weaken (0 1 3))
simplify
(weaken (1 2))
simplify
))
(usages transportable-macete)
(theory mappings-from-an-interval-to-a-normed-space))

```

```
(def-theorem mean-value-theorem-corollary-1
"forall(f,g:[ii,uu],
total_q{f,[ii,uu]}
and
total_q{g,[ii,uu]}
and
continuous(f)
and
continuous(g)
and
forall(x:ii,forsome(y:ii,x<y) implies deriv(f,x)=deriv(g,x))
and
forsome(x,y:ii,f(x)=g(x) and x<y)
implies
forall(x:ii,f(x)=g(x)))"
(theory mappings-from-an-interval-to-a-normed-space)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula
"forall(x,y:ii,lambda(x:ii,f(x)-g(x))(x)=lambda(x:ii,f(x)-g(x))(y))")
(incorporate-antecedent "with(g,f:[ii,uu],
forall(x,y:ii,
lambda(x:ii,f(x)-g(x))(x)=lambda(x:ii,f(x)-g(x))(y)));")
simplify
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(g,f:[ii,uu],forall(x,y:ii,f(x)+g(y)=f(y)+g(x)));"
("x_\$0" "x"))
(incorporate-antecedent "with(x:ii,g:[ii,uu],x_\$0:ii,f:[ii,uu],
f(x_\$0)+g(x)=f(x)+g(x_\$0));")
simplify
(apply-macete-with-minor-premises mean-value-theorem-corollary-0)
simplify
insistent-direct-inference-strategy
beta-reduce-repeatedly
simplify
(force-substitution "[-1]*g(x)" "lambda(x:ii,[-1]*g(x))(x)" (0))
(apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity)
(apply-macete-with-minor-premises ns-sum-of-continuous-is-continuous)
(apply-macete-with-minor-premises ns-multiple-of-continuous-is-continuous)
(incorporate-antecedent "with(f:[ii,uu],continuous(f));")
(incorporate-antecedent "with(g:[ii,uu],continuous(g));")
(apply-macete-with-minor-premises tr%eps-delta-characterization-of-continuity)
direct-and-antecedent-inference-strategy
(weaken (7 6 5 3 2 1 0))
beta-reduce-repeatedly
(force-substitution "[-1]*g(x)" "lambda(x:ii,[-1]*g(x))(x)" (0))
(apply-macete-with-minor-premises homogeneity-of-deriv)
simplify
simplify
simplify
simplify
(weaken (0 1 2 3 4 6 7 8))
)))
```

```
(def-theorem locality-of-derivative
"forall(f,g:[ii,uu],x:ii,
forsome(y:ii, x<y and forall(t:ii, x<=t and t<y implies f(t)=g(t)))
implies deriv(f,x)==deriv(g,x))"
(theory mappings-from-an-interval-to-a-normed-space)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference-strategy
(antecedent-inference "with(p,q:prop, p or q)")
(cut-with-single-formula "forsome(v:uu, deriv(f,x)=v)")
(antecedent-inference "with(x:ii,f:[ii,uu],forsome(v:uu,deriv(f,x)=v));")
(backchain "with(v:uu,x:ii,f:[ii,uu],deriv(f,x)=v);")
(force-substitution "v=deriv(g,x)" "deriv(g,x)=v" (0))
(incorporate-antecedent "with(v:uu,x:ii,f:[ii,uu],deriv(f,x)=v);")
(apply-macete-with-minor-premises characterization-of-derivative)
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))")
(cut-with-single-formula "forsome(z:ii,x<z and z<=z_0 and z<y)")
(antecedent-inference-strategy (0))
(instantiate-existential ("z"))
(backchain-backwards "with(g,f:[ii,uu],y,x:ii,
forall(t:ii,x<=t and t<y implies f(t)=g(t)));")
(backchain-backwards "with(g,f:[ii,uu],y,x:ii,
forall(t:ii,x<=t and t<y implies f(t)=g(t)));")
direct-and-antecedent-inference-strategy
simplify
simplify
simplify
(backchain "with(eps:rr,v:uu,f:[ii,uu],z_0,x:ii,
forall(z:ii,
x<z and z<=z_0
implies
norm((z-x)^[-1]*(f(z)-f(x))-v)<=eps));")
simplify
(cut-with-single-formula "forsome(z:ii,x<z and z<y)")
(antecedent-inference "with(y,x:ii,forsome(z:ii,x<z and z<y));")
(instantiate-existential ("min(z,z_0)"))
(unfold-single-defined-constant (0) min)
(case-split ("z<=z_0"))
simplify
simplify
(apply-macete-with-minor-premises minimum-2nd-arg)
(cut-with-single-formula "min(z,z_0)<=z")
simplify
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises interval-characterization)
(instantiate-existential ("z_0" "x"))
simplify
(instantiate-existential ("(x+y)/2"))
simplify
simplify
(apply-macete-with-minor-premises interval-characterization)
(instantiate-existential ("y" "x"))
simplify
simplify
simplify
(instantiate-existential ("deriv(f,x)"))
(cut-with-single-formula "forall(f,g:[ii,uu], #(deriv(f,x)) and forall(t:ii,x<=t and t<y implies f(t)=g(t)) and x<y implies deriv(f,x)=deriv(g,x) )")
(force-substitution "deriv(f,x)=deriv(g,x)" "deriv(g,x)=deriv(f,x)" (0))
(backchain "with(y,x:ii,
forall(f,g:[ii,uu],
#(deriv(f,x))
and
forall(t:ii,x<=t and t<y implies f(t)=g(t))
and
x<y
implies
deriv(f,x)=deriv(g,x)));")
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(g,f:[ii,uu],y,x:ii,
forall(t:ii,x<=t and t<y implies f(t)=g(t)));" ("t"))
simplify
(weaken (1 2 0))
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem derivative-of-a-linear-map
"forall(a,b:uu,x:ii,
forsome(y:ii,x<y) implies deriv(lambda(t:ii,t*a+b),x)=a)"
(theory mappings-from-an-interval-to-a-normed-space)
(proof
(
(force-substitution "t*a+b" "lambda(t:ii,t*a)(t)+lambda(t:ii,b)(t)" (0))
(apply-macete-with-minor-premises deriv-of-constant)
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises characterization-of-derivative)
beta-reduce-repeatedly
(force-substitution "(z*a-x*a)" "(z-x)*a" (0))
simplify
direct-and-antecedent-inference-strategy
auto-instantiate-existential
simplify
(apply-macete-with-minor-premises deriv-of-constant)
simplify
simplify
)))
```