```
(def-theorem convergence-test-for-complete-spaces
"complete
implies
forall(f:[zz,pp],
forsome(s:[zz,rr],k:zz,
summable%nonnegative(s)
and
forall(j:zz,k<=j implies dist(f(j),f(j+1))<=s(j)))
implies
#(lim(f)))"

(proof
(
(unfold-single-defined-constant (0) complete)
direct-and-antecedent-inference-strategy
(backchain "forall(s:[zz,pp],cauchy(s) implies #(lim(s)));")
(unfold-single-defined-constant (0) cauchy)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(p:zz, forall(j,j_1:zz, p<=j and j<=j_1 implies sum(j,j_1,s)<=eps))")
(instantiate-existential ("max(k,p)"))
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("sum(max(k,p),q_\$0-1,lambda(j:zz,dist(f(j),f(j+1))))"))
(force-substitution "q_\$0" "q_\$0-1+1" (0))
(apply-macete-with-minor-premises generalized-triangle-inequality)
direct-and-antecedent-inference-strategy

simplify
(cut-with-single-formula "dist(f(j),f(j+1))<=s(j)")
(backchain "with(s:[zz,rr],f:[zz,pp],k:zz,
forall(j:zz,k<=j implies dist(f(j),f(j+1))<=s(j)));")
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("max(k,p)"))
(apply-macete-with-minor-premises maximum-1st-arg)
simplify
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("sum(max(k,p),q_\$0-1,s)"))
(apply-macete-with-minor-premises monotonicity-for-sum)
direct-and-antecedent-inference-strategy
beta-reduce-repeatedly
(backchain "with(s:[zz,rr],f:[zz,pp],k:zz,
forall(j:zz,k<=j implies dist(f(j),f(j+1))<=s(j)));")
(cut-with-single-formula "k<=max(k,p)")
simplify
(apply-macete-with-minor-premises maximum-1st-arg)
(backchain "with(eps:rr,s:[zz,rr],p:zz,
forall(j,j_1:zz,
p<=j and j<=j_1 implies sum(j,j_1,s)<=eps));")
(apply-macete-with-minor-premises maximum-2nd-arg)
(cut-with-single-formula "sum(max(k,p),[-1]+q_\$0,s)<=eps")
(backchain "with(eps:rr,s:[zz,rr],p:zz,
forall(j,j_1:zz,
p<=j and j<=j_1 implies sum(j,j_1,s)<=eps));")
(apply-macete-with-minor-premises maximum-2nd-arg)
simplify
(apply-macete-with-minor-premises sum-definedness)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "dist(f(k_\$0),f(1+k_\$0))<=s(k_\$0)")
(backchain "with(s:[zz,rr],f:[zz,pp],k:zz,
forall(j:zz,k<=j implies dist(f(j),f(j+1))<=s(j)));")
(cut-with-single-formula "k<=max(k,p)")
simplify
(apply-macete-with-minor-premises maximum-1st-arg)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises small%tails%of%summable%nonnegative%sequence)
direct-and-antecedent-inference-strategy

)
)
(usages transportable-macete)
(theory metric-spaces))
```

```
(def-theorem geometric-series-formula
"forall(a,r:rr,p,q:zz,
0<=p and p<=q and not(r=0) and not(r=1)
implies
sum(p,q,lambda(j:zz,r^j*a))=a*r^p/(1-r)*(1-r^(q-p+1)))"
lemma
(theory h-o-real-arithmetic)

(proof
(
(apply-macete-with-minor-premises fractional-expression-manipulation)
(induction integer-inductor ("q"))

)))
```

```
(def-theorem geometric-series-upper-estimate-lemma
"forall(a,r:rr,p,q:zz,
1<=p and p<=q and 0<r and r<1 and 0<=a
implies
a*r^p/(1-r)*(1-r^(q-p+1)) <= a*r^p/(1-r))"
lemma
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises positivity-for-products)
direct-and-antecedent-inference-strategy
(force-substitution "0<=r^(1+q)" "0<r^(1+q)" (0))
(apply-macete-with-minor-premises positivity-for-r^n)
simplify

)))
```

```
(def-theorem  geometric-series-upper-estimate
"forall(a,r:rr,p,q:zz,
1<=p and p<=q and 0<r and r<1 and 0<=a
implies
sum(p,q,lambda(j:zz,r^j*a))<=a*r^p/(1-r))"
(theory h-o-real-arithmetic)

(proof
(
(apply-macete-with-minor-premises geometric-series-formula)
(apply-macete-with-minor-premises  geometric-series-upper-estimate-lemma)
)))
```

```
(def-theorem  geometric-series-is-summable%nonnegative
"forall(a,r:rr,p,q:zz, 0<r and r<1 and 0<=a
implies
summable%nonnegative(lambda(j:zz,r^j*a)))"

(proof
(
(unfold-single-defined-constant (0) summable%nonnegative)
direct-and-antecedent-inference-strategy
(instantiate-existential ("1"))
(apply-macete-with-minor-premises positivity-for-products)
(cut-with-single-formula "0<r^n")
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
(instantiate-existential ("1"))
(apply-macete-with-minor-premises sum-definedness)
beta-reduce-repeatedly
simplify
(instantiate-existential ("a*r^1/(1-r)"))
(unfold-single-defined-constant (0) majorizes)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(backchain "with(a,r:rr,x_\$1:zz,x:rr,x=sum(1,x_\$1,lambda(j_\$0:zz,r^j_\$0*a)));")
(case-split ("1<=x_\$1"))
(apply-macete-with-minor-premises geometric-series-upper-estimate)
direct-and-antecedent-inference-strategy
simplify
(unfold-single-defined-constant (0) sum)
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
))
(theory h-o-real-arithmetic))

```