(def-theorem sup-minus-epsilon"forall(s:sets[rr],eps:rr,0<eps implies not(sup(s)-eps majorizes s))"(theory h-o-real-arithmetic) (proof (direct-and-antecedent-inference-strategy (cut-with-single-formula"#(sup(s)) or not(#(sup(s)))") (antecedent-inference"with(s:sets[rr],#(sup(s)) or not(#(sup(s))));") (cut-with-single-formula"not(sup(s)<=sup(s)-eps)") (contrapose"with(eps:rr,s:sets[rr],not(sup(s)<=sup(s)-eps));") (apply-macete-with-minor-premises tr%lub-property-of-prec%sup) direct-and-antecedent-inference-strategy simplify simplify simplify)))

(def-theorem sup-minus-epsilon-corollary"forall(s:sets[rr],eps:rr, 0<eps and #(sup(s)) implies forsome(x:rr, x in s and sup(s)-eps<x))"(proof (direct-and-antecedent-inference-strategy (cut-with-single-formula"not(sup(s)-eps majorizes s)") (contrapose"with(eps:rr,s:sets[rr],not(sup(s)-eps majorizes s));") (unfold-single-defined-constant (0) majorizes) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p,q:prop,forall(x:rr,p or q))"("x_$0")) simplify (apply-macete-with-minor-premises sup-minus-epsilon))) (theory h-o-real-arithmetic))

(def-theorem nondecreasing-sequences-converge"forall(f:[zz,rr],nondecreasing(f) and forsome(n:zz,forall(k:zz,n<=k implies #(f(k)))) and #(sup(ran{f})) implies forall(eps:rr, 0<eps implies forsome(k:zz, forall(j:zz, k<=j implies sup(ran{f})-f(j)<=eps))))"(proof ( (unfold-single-defined-constant (0) nondecreasing) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(x:rr , x in ran{f} and sup(ran{f})-eps<x)") (antecedent-inference"with(eps:rr,f:[zz,rr], forsome(x:rr,x in ran{f} and sup(ran{f})-eps<x))") (antecedent-inference"with(eps,x:rr,f:[zz,rr],x in ran{f} and sup(ran{f})-eps<x)") (incorporate-antecedent"with(x:rr,f:[zz,rr],x in ran{f})") (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("max(x_$0,n)")) (cut-with-single-formula"f(x_$0)<=f(j_$0)") simplify (backchain"with(f:[zz,rr], forall(n,p:zz, n<=p and #(f(n)) and #(f(p)) implies f(n)<=f(p)))") (cut-with-single-formula"n<=max(x_$0,n) and x_$0<=max(x_$0,n)") direct-and-antecedent-inference-strategy simplify (backchain"with(f:[zz,rr],n:zz,forall(k:zz,n<=k implies #(f(k))))") simplify (apply-macete-with-minor-premises maximum-1st-arg) (apply-macete-with-minor-premises maximum-2nd-arg) (apply-macete-with-minor-premises sup-minus-epsilon-corollary) direct-and-antecedent-inference-strategy )) (theory h-o-real-arithmetic))

(def-theorem nondecreasing-sequences-converge-corollary"forall(f:[zz,rr],nondecreasing(f) and forsome(n:zz,forall(k:zz,n<=k implies #(f(k)))) and #(sup(ran{f})) implies forall(eps:rr, 0<eps implies forsome(k:zz, forall(j,j_1:zz, k<=j and j<=j_1 implies f(j_1)-f(j)<=eps))))"(proof ( direct-and-antecedent-inference-strategy (instantiate-theorem nondecreasing-sequences-converge ("f")) (contrapose"with(f:[zz,rr],forall(n:zz,forsome(k:zz,n<=k and not(#(f(k))))))") (instantiate-existential ("n")) (instantiate-universal-antecedent"with(p:prop,forall(eps:rr,0<eps implies p))"("eps")) (instantiate-existential ("k")) (cut-with-single-formula"f(j_1)<=sup(ran{f}) and sup(ran{f})-f(j)<=eps") simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy (instantiate-existential ("f(max(j_1,n))")) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (instantiate-existential ("max(j_1,n)")) (incorporate-antecedent"with(f:[zz,rr],nondecreasing(f));") (unfold-single-defined-constant (0) nondecreasing) direct-and-antecedent-inference-strategy (backchain"with(f:[zz,rr], forall(n,p:zz, n<=p and #(f(n)) and #(f(p)) implies f(n)<=f(p)));") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises maximum-1st-arg) (instantiate-universal-antecedent"with(eps:rr,f:[zz,rr],k:zz, forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));"("j_1")) (contrapose"with(j_1,k:zz,not(k<=j_1));") simplify (instantiate-universal-antecedent"with(eps:rr,f:[zz,rr],k:zz, forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));"("j_1")) (backchain"with(eps:rr,f:[zz,rr],k:zz, forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));") )) (theory h-o-real-arithmetic))

(def-theorem sum-interval-additivity"forall(m,n,p:zz, f:[zz,rr], m<=n and n<=p implies sum(m,n,f)+sum(n+1,p,f)==sum(m,p,f))"(proof ( (induction integer-inductor ("p")) direct-inference (backchain-backwards"with(p,q:prop, p implies q)") direct-and-antecedent-inference-strategy simplify ) ) (theory h-o-real-arithmetic))

(def-theorem sum-nonnegativityRemark: This entry is multiply defined. See: [1] [2]"forall(f:[zz,rr], a,b:zz, forall(z:zz,a<=z and z<=b implies 0<=f(z)) implies 0<=sum(a,b,f))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (case-split ("a<=b")) (induction integer-inductor ()) direct-and-antecedent-inference-strategy (cut-with-single-formula"0<=sum(a,t,f) and 0<=f(1+t)") simplify (prove-by-logic-and-simplification 3) (unfold-single-defined-constant (0) sum) simplify ) ))

(def-theorem nondecreasing%sums"forall(s:[zz,rr], k:zz, forall(n:zz,k<=n implies 0<=s(n)) implies nondecreasing(lambda(p:zz,sum(k,p,s))))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant (0) nondecreasing) direct-and-antecedent-inference-strategy (case-split ("k<=n_$0")) (force-substitution"sum(k,p_$0,s)""sum(k,n_$0,s)+sum(n_$0+1,p_$0,s)"(0)) simplify (apply-macete-with-minor-premises sum-nonnegativity) (prove-by-logic-and-simplification 3) (apply-macete-with-minor-premises sum-interval-additivity) (unfold-single-defined-constant (0) sum) simplify (case-split ("k<=p_$0")) (apply-macete-with-minor-premises sum-nonnegativity) (prove-by-logic-and-simplification 3) (unfold-single-defined-constant (0) sum) simplify ) ) )

(def-constant summable%nonnegative"lambda(s:[zz,rr], forsome(k:zz, forall(n:zz,k<=n implies 0<=s(n) and #(sup(ran{lambda(p:zz,sum(k,p,s))})))))"(theory h-o-real-arithmetic))

(def-theorem small%tails%of%summable%nonnegative%sequence"forall(s:[zz,rr], summable%nonnegative(s) implies forall(eps:rr,0<eps implies forsome(p:zz, forall(j,j_1:zz, p<=j and j<=j_1 implies sum(j,j_1,s)<=eps))))"(proof ( (unfold-single-defined-constant (0) summable%nonnegative) direct-and-antecedent-inference-strategy (instantiate-theorem nondecreasing-sequences-converge-corollary ("lambda(j:zz, sum(k,j,s))")) (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises nondecreasing%sums) direct-and-antecedent-inference-strategy (backchain"with(p:prop, k:zz, forall(n:zz, k<=n implies p))") (contrapose"with(s:[zz,rr],k:zz, forall(n_$0:zz, forsome(k_$0:zz, n_$0<=k_$0 and not(#(lambda(j:zz,sum(k,j,s))(k_$0))))));") beta-reduce-repeatedly (instantiate-existential ("k")) (cut-with-single-formula"0<=sum(k,k_$1,s)") (apply-macete-with-minor-premises sum-nonnegativity) (prove-by-logic-and-simplification 3) (contrapose"with(p:prop, not(p))") (backchain"with(s:[zz,rr],k:zz, forall(n:zz, k<=n implies 0<=s(n) and #(sup(ran{lambda(p:zz,sum(k,p,s))}))));") (instantiate-existential ("k")) simplify (beta-reduce-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))") (auto-instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))") (instantiate-existential ("max(k,k_$0)+1")) (instantiate-universal-antecedent"with(eps:rr,s:[zz,rr],k,k_$0:zz, forall(j_$0,j_$1:zz, k_$0<=j_$0 and j_$0<=j_$1 implies sum(k,j_$1,s)-sum(k,j_$0,s)<=eps));"("j-1""j_1")) (contrapose"with(p:prop, not(p))") (cut-with-single-formula"k_$0<=max(k,k_$0)") simplify (apply-macete-with-minor-premises maximum-2nd-arg) (simplify-antecedent"with(j_1,j:zz,not(j-1<=j_1));") (cut-with-single-formula"sum(k,j_1,s)==sum(k,j-1,s)+ sum((j-1)+1,j_1,s)") simplify (apply-macete-with-minor-premises sum-interval-additivity) (cut-with-single-formula"k<=max(k,k_$0)") simplify (apply-macete-with-minor-premises maximum-1st-arg) ) ) (theory h-o-real-arithmetic))