(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)") (apply-macete-with-minor-premises commutative-law-for-addition) (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))