(def-theorem ()"forall(x,y:pp,#(dist(x,y)))"(theory metric-spaces) (usages d-r-convergence transportable-macete) (proof (insistent-direct-inference-strategy (instantiate-theorem positivity-of-distance ("x""y")))))

(def-theorem ()"forall(x,y:pp,dist(x,y)<=dist(y,x))"(theory metric-spaces) (proof ((instantiate-theorem symmetry-of-distance ("x""y")) simplify)))

(def-theorem ()"forall(x:pp,dist(x,x)<=0)"(theory metric-spaces) (proof ((instantiate-theorem point-separation-for-distance ("x""x")) simplify)))

(def-theorem triangle-inequality-alternate-form"forall(x,y,z:pp,r:rr, dist(x,z)+dist(z,y)<=r implies dist(x,y)<=r)"(theory metric-spaces) (usages transportable-macete) (proof (direct-inference-strategy (cut-with-single-formula"dist(x,y)<=dist(x,z)+dist(z,y)") simplify (apply-macete-with-minor-premises triangle-inequality-for-distance) )))

(def-theorem zero-self-distance"forall(x,y:pp,dist(x,x)=0)"(theory metric-spaces) (usages transportable-macete) (proof ( direct-inference (instantiate-theorem point-separation-for-distance ("x""x")) ) ))

(def-theorem metric-separation"forall(x,y:pp,x=y iff forall(r:rr,0<r implies forsome(z:pp, dist(z,x)<=r and dist(z,y)<=r)))"(theory metric-spaces) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("x")) simplify simplify (apply-macete-with-minor-premises point-separation-for-distance) (instantiate-universal-antecedent"with(p:prop, forall(r:rr, 0<r implies p))"("dist(x,y)/3")) simplify (cut-with-single-formula"dist(x,y)<=dist(z_$0,x)+dist(z_$0,y)") simplify (cut-with-single-formula"dist(x,y)<=dist(x,z_$0)+dist(z_$0,y)") simplify (apply-macete-with-minor-premises triangle-inequality-for-distance) )))

(def-theorem ball-definedness"forall(a:pp,r:rr,#(ball(a,r)))"(theory metric-spaces) (usages transportable-macete) (proof (unfold-defined-constants insistent-direct-inference-strategy simplify)))

(def-theorem open-ball-definedness"forall(a:pp,r:rr,#(open%ball(a,r)))"(theory metric-spaces) (usages transportable-macete) (proof (unfold-defined-constants insistent-direct-inference-strategy simplify)))

(def-theorem ball-membership-condition"forall(a,x:pp,r:rr,x in ball(a,r) iff dist(a,x)<=r)"(theory metric-spaces) (usages transportable-macete) (proof (unfold-defined-constants direct-inference simplify-insistently)))

(def-theorem open-ball-membership-condition"forall(a,x:pp,r:rr,x in open%ball(a,r) iff dist(a,x)<r)"(theory metric-spaces) (usages transportable-macete) (proof (unfold-defined-constants direct-inference simplify-insistently)))

(def-theorem open-balls-are-open"forall(a:pp,r:rr,open(open%ball(a,r)))"(theory metric-spaces) (usages transportable-macete) (proof ( unfold-defined-constants-repeatedly simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("(r-dist(a,x_$2))/2")) simplify (cut-with-single-formula"dist(a,x_$0)<=dist(a,x_$2)+dist(x_$2,x_$0)") simplify (apply-macete-with-minor-premises triangle-inequality-for-distance) )))

(def-constant lim"lambda(s:[zz,pp],iota(x:pp, forall(eps:rr,0<eps implies forsome(n:zz, forall(p:zz, n<=p implies dist(x,s(p))<=eps)))))"(theory metric-spaces))

(def-theorem characterization-of-limit"forall(s:[zz,pp],x:pp,lim(s)=x iff forall(eps:rr,0<eps implies forsome(n:zz, forall(p:zz, n<=p implies dist(x,s(p))<=eps))))"(theory metric-spaces) (usages transportable-macete) (proof ( (unfold-single-defined-constant (0) lim) direct-and-antecedent-inference-strategy (contrapose"with(a:pp,p:prop, iota(x:pp, p)=a)") (eliminate-defined-iota-expression 0 w) (contrapose"with(eps:rr,s:[zz,pp],x:pp, forall(n:zz, forsome(p:zz,n<=p and not(dist(x,s(p))<=eps))));") (backchain-backwards"with(x,w:pp,w=x);") (backchain"with(p:prop,forall(eps:rr,0<eps implies p))") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises metric-separation) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(s:[zz,pp],b_$0:pp, forall(eps:rr, 0<eps implies forsome(n:zz, forall(p:zz,n<=p implies dist(b_$0,s(p))<=eps))));"("r")) (instantiate-universal-antecedent"with(s:[zz,pp],x:pp, forall(eps:rr, 0<eps implies forsome(n:zz, forall(p:zz,n<=p implies dist(x,s(p))<=eps))));"("r")) (instantiate-existential ("s(max(n,n_$0))")) (apply-macete-with-minor-premises symmetry-of-distance) (backchain"with(r:rr,s:[zz,pp],b_$0:pp,n:zz, forall(p:zz,n<=p implies dist(b_$0,s(p))<=r));") (apply-macete-with-minor-premises maximum-1st-arg) (apply-macete-with-minor-premises symmetry-of-distance) (backchain"with(r:rr,s:[zz,pp],x:pp,n_$0:zz, forall(p:zz,n_$0<=p implies dist(x,s(p))<=r));") (apply-macete-with-minor-premises maximum-2nd-arg) (instantiate-universal-antecedent"with(r:rr,s:[zz,pp],x:pp,n_$0:zz, forall(p:zz,n_$0<=p implies dist(x,s(p))<=r));"("max(n,n_$0)")) )))

(def-theorem existence-of-limit"forall(s:[zz,pp], #(lim(s)) iff forsome(x:pp,forall(eps:rr,0<eps implies forsome(n:zz,forall(p:zz, n<=p implies dist(x,s(p))<=eps)))))"(theory metric-spaces) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"lim(s)=lim(s)") (incorporate-antecedent"with(s:[zz,pp],lim(s)=lim(s));") (apply-macete-with-minor-premises characterization-of-limit) direct-inference (instantiate-existential ("lim(s)")) (cut-with-single-formula"lim(s)=x") (apply-macete-with-minor-premises characterization-of-limit) ) ))

(def-constant cauchy"lambda(s:[zz,pp],forall(eps:rr,0<eps implies forsome(p:zz,forall(q:zz,p<q implies dist(s(p),s(q))<=eps))))"(theory metric-spaces))

(def-constant complete"forall(s:[zz,pp],cauchy(s) implies #(lim(s)))"(theory metric-spaces))

(def-theorem cauchy-double-index-characterization"forall(s:[zz,pp], cauchy(s) iff forall(eps:rr,0<eps implies forsome(n:zz,forall(p,q:zz,n<=p and n<=q implies dist(s(p),s(q))<=eps))))"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("eps/2")) (contrapose"with(p:prop,not(p))") simplify (instantiate-existential ("p_$0+1")) (apply-macete-with-minor-premises triangle-inequality-alternate-form) (instantiate-existential ("s(p_$0)")) (cut-with-single-formula"dist(s(p_$0),s(p))<=eps/2 and dist(s(p_$0),s(q))<=eps/2") simplify direct-and-antecedent-inference-strategy (backchain"with(r:prop, forall(q_$0:zz,p_$0<q_$0 implies r))") simplify (backchain"with(r:prop, forall(q_$0:zz,p_$0<q_$0 implies r))") simplify (instantiate-universal-antecedent"with(r:prop, forall(q_$0:zz,p_$0<q_$0 implies r))"("q")) (instantiate-universal-antecedent"with(r:prop, forall(q_$0:zz,p_$0<q_$0 implies r))"("q")) (instantiate-universal-antecedent"with(r:prop, forall(q_$0:zz,p_$0<q_$0 implies r))"("q")) (auto-instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))") (instantiate-existential ("n")) (backchain"with(eps:rr,s:[zz,pp],n:zz,forall(p,q:zz,n<=p and n<=q implies dist(s(p),s(q))<=eps))") simplify ) ) (usages transportable-macete) (theory metric-spaces))

(def-theorem convergent-implies-cauchy"forall(s:[zz,pp], #(lim(s)) implies cauchy(s))"(theory metric-spaces) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises existence-of-limit) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) cauchy) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(eps:rr,0<eps implies p))"("eps/2")) (simplify-antecedent"with(p:prop, not(p))") (instantiate-existential ("n_$0")) (cut-with-single-formula"dist(s(n_$0),s(q))<=dist(s(n_$0),x)+dist(x,s(q)) and dist(s(n_$0),x)<=eps/2 and dist(x,s(q))<=eps/2") (antecedent-inference"with(p,q,r:prop, p and q and r)") simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises triangle-inequality-for-distance) (instantiate-universal-antecedent"with(q:prop,n:zz,forall(p:zz,n<=p implies q))"("q")) (simplify-antecedent"with(q,n_$0:zz,not(n_$0<=q));") (instantiate-universal-antecedent"with(q:prop,n:zz,forall(p:zz,n<=p implies q))"("n_$0")) (simplify-antecedent"with(n_$0:zz,not(n_$0<=n_$0));") (apply-macete-with-minor-premises symmetry-of-distance) (backchain"with(q:prop,n:zz,forall(p:zz,n<=p implies q))") simplify (backchain"with(q:prop,n:zz,forall(p:zz,n<=p implies q))") simplify )) (usages transportable-macete))

(def-theorem closed-balls-are-closed"forall(x:pp,r:rr,s:[zz,pp], ran{s} subseteq ball(x,r) and #(lim(s)) implies lim(s) in ball(x,r))"(theory metric-spaces) (usages transportable-macete) (proof ((force-substitution"#(lim(s))""#(lim(s)) and lim(s)=lim(s)"(0)) (apply-macete-with-minor-premises characterization-of-limit) simplify-insistently (unfold-single-defined-constant (0 1) ball) simplify-insistently direct-and-antecedent-inference-strategy (cut-with-single-formula"dist(x_$1,lim(s))<=r or r<dist(x_$1,lim(s))") (antecedent-inference"with(p,q:prop, p or q)") (instantiate-universal-antecedent"with(s:[zz,pp], forall(eps:rr, 0<eps implies forsome(n:zz, forall(p:zz,n<=p implies dist(lim(s),s(p))<=eps))));"("(dist(x_$1,lim(s))-r)/3")) (contrapose"with(p:prop, not(p))") simplify (instantiate-universal-antecedent"with(p:prop,n:zz,forall(q:zz,n<=q implies p))"("n_$0")) (contrapose"with(p:prop, not(p))") simplify (instantiate-universal-antecedent"with(p:prop, forall(x:pp,p))"("s(n_$0)")) (contrapose"with(p:prop, forall(x:zz, not(p)))") (instantiate-existential ("n_$0")) (apply-macete-with-minor-premises transitivity-of-<=) (apply-macete-with-minor-premises symmetry-of-distance) (instantiate-existential ("dist(lim(s),s(n_$0))+dist(s(n_$0),x_$1)")) (apply-macete-with-minor-premises triangle-inequality-for-distance) (incorporate-antecedent"with(a,b:pp,dist(a,b)<=(dist(b,a)-r)/3);") (force-substitution"dist(x_$1,lim(s))""dist(lim(s),x_$1)"(0)) simplify simplify simplify)))

(def-theorem ball-subset-larger-radius-open-ball"forall(a:pp,r,r_1:rr,r<r_1 implies ball(a,r) subseteq open%ball(a,r_1))"(theory metric-spaces) (usages transportable-macete) (proof (unfold-defined-constants simplify-insistently)))

(def-theorem limit-of-subsequence"forall(s:[zz,pp],phi:[zz,zz],#(lim(s)) and convergent%to%infinity(phi) implies lim(s)=lim(s oo phi))"(theory metric-spaces) (usages transportable-macete) (proof ( (unfold-single-defined-constant (0) convergent%to%infinity) (force-substitution"lim(s)=lim(s oo phi)""lim(s oo phi)=lim(s)"(0)) direct-inference-strategy (antecedent-inference"with(p,q:prop, p and q)") (cut-with-single-formula"lim(s)=lim(s)") (incorporate-antecedent"with(s:[zz,pp],lim(s)=lim(s));") (apply-macete-with-minor-premises characterization-of-limit) direct-inference-strategy (auto-instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))") (instantiate-universal-antecedent"with(p:prop,forall(m:rr,forsome(x:zz,p)))"("n")) (instantiate-existential ("x")) beta-reduce-insistently (backchain"with(eps:rr,s:[zz,pp],n:zz, forall(p:zz,n<=p implies dist(lim(s),s(p))<=eps));") simplify simplify simplify )))

(def-theorem limit-of-subsequence-corollary"forall(s:[zz,pp],n:zz, #(lim(s)) implies lim(s)=lim(s oo lambda(i:zz,(if (n<=i,i,?zz)))))"(theory metric-spaces) (usages transportable-macete) (proof ((apply-macete-with-minor-premises limit-of-subsequence) (unfold-single-defined-constant (0) convergent%to%infinity) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m_1:zz,max(n,m)<m_1)") (instantiate-existential ("m_1")) (cut-with-single-formula"n<=max(n,m) and m<=max(n,m)") simplify (apply-macete-with-minor-premises maximum-1st-arg) (apply-macete-with-minor-premises maximum-2nd-arg) (apply-macete-with-minor-premises archimedean)) ))

(def-theorem limit-depends-on-tail"forall(s,s_1:[zz,pp],n:zz, forsome(m:zz,forall(p:zz,m<=p implies s_1(p)=s(p))) and #(lim(s)) implies lim(s_1)=lim(s))"(theory metric-spaces) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises characterization-of-limit) direct-and-antecedent-inference-strategy (cut-with-single-formula"lim(s)=lim(s)") (incorporate-antecedent"with(s:[zz,pp],lim(s)=lim(s))") (apply-macete-with-minor-premises characterization-of-limit) direct-and-antecedent-inference-strategy (auto-instantiate-universal-antecedent"with(s:[zz,pp],forall(eps:rr, 0<eps implies forsome(n:zz, forall(p:zz,n<=p implies dist(lim(s),s(p))<=eps))))") (instantiate-existential ("max(n,m)")) (backchain"with(s,s_1:[zz,pp],m:zz,forall(p:zz,m<=p implies s_1(p)=s(p)))") direct-inference (cut-with-single-formula"m<=max(n,m)") simplify (apply-macete-with-minor-premises maximum-2nd-arg) (backchain"with(eps:rr,s:[zz,pp],n:zz, forall(p:zz,n<=p implies dist(lim(s),s(p))<=eps))") (cut-with-single-formula"n<=max(n,m)") simplify (apply-macete-with-minor-premises maximum-1st-arg) )))

(def-theorem limit-translation-invariance"forall(s:[zz,pp],a,b:zz,#(lim(s)) and 0<a implies lim(s)=lim(lambda(j:zz,s(a*j+b))))"(theory metric-spaces) (proof ( (force-substitution"lambda(j:zz,s(a*j+b))""s oo lambda(j:zz,a*j+b)"(0)) (apply-macete-with-minor-premises limit-of-subsequence) simplify (force-substitution"b+j*a""a*j+b"(0)) (apply-macete-with-minor-premises convergent%to%infinity-linear-form) sort-definedness simplify simplify-insistently )))

(def-constant closure"lambda(a:sets[pp],indic{y:pp,forall(r:rr,0<r implies nonempty_indic_q{open%ball(y,r) inters a})})"(theory metric-spaces))

(def-theorem characterization-of-closure-lemma-1"forall(x:pp,a:sets[pp], forsome(s:[zz,pp],ran{s} subseteq a and lim(s)=x) implies x in closure(a))"lemma (proof ((force-substitution"ran{s} subseteq a ""forall(x:zz, #(s(x)) implies s(x) in a)"(0)) (apply-macete-with-minor-premises characterization-of-limit) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) closure) simplify-insistently (apply-macete-with-minor-premises open-ball-membership-condition) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("r_$0/2")) (contrapose"with(p:prop, not(p))") simplify (instantiate-existential ("s(n)")) (instantiate-universal-antecedent"with(r_$0:rr,s:[zz,pp],x_$0:pp,n:zz, forall(p:zz,n<=p implies dist(x_$0,s(p))<=r_$0/2));"("n")) (contrapose"with(p:prop, not(p))") simplify simplify (backchain"with(a:sets[pp],s:[zz,pp],forall(x:zz,#(s(x)) implies s(x) in a));") simplify direct-and-antecedent-inference-strategy (backchain"with(a,b:sets[pp],s:[zz,pp],b subseteq a);") simplify-insistently (instantiate-existential ("x")))) (theory metric-spaces))

(def-theorem characterization-of-closure-lemma-2"forall(x:pp,a:sets[pp], x in closure(a) implies forsome(s:[zz,pp], forall(n:zz,1<=n implies s(n) in a and dist(s(n),x)<=1/n)))"lemma (theory metric-spaces) (proof ( (unfold-single-defined-constant (0) closure) simplify-insistently (apply-macete-with-minor-premises open-ball-membership-condition) direct-and-antecedent-inference-strategy choice-principle direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,p);"("max(1,n)^[-1]")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 0)") (contrapose"with(p:prop,p);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify) (block (script-comment"`instantiate-universal-antecedent' at (0 0 1 0 0)") (cut-with-single-formula"forsome(z:pp, z in a and dist(x,z)<max(1,n)^[-1])") (move-to-sibling 1) auto-instantiate-existential (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(z:pp,p));") (instantiate-existential ("z")) (force-substitution"n""max(1,n)"(0)) simplify (block (script-comment"`force-substitution' at (1)") (unfold-single-defined-constant (0) max) simplify))) )))

(def-theorem characterization-of-closure"forall(x:pp,a:sets[pp], x in closure(a) iff forsome(s:[zz,pp],ran{s} subseteq a and lim(s)=x))"(theory metric-spaces) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0 0)") (cut-with-single-formula"forsome(s:[zz,pp], forall(n:zz,1<=n implies s(n) in a and dist(s(n),x_$1)<=1/n))") (block (script-comment"node added by `cut-with-single-formula' at (0)") (instantiate-existential ("lambda(n:zz, if(1<=n,s(n),?pp))")) (block (script-comment"node added by `instantiate-existential' at (0 0 0)") simplify-insistently direct-and-antecedent-inference-strategy (backchain"with(p,x_$3:pp,x_$3=p);") (backchain"with(p:prop,forall(n:zz,p));")) (block (script-comment"node added by `instantiate-existential' at (0 0 1)") (apply-macete-with-minor-premises characterization-of-limit) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(n:zz,1<=n and 1/n<=eps)") (block (script-comment"node added by `cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(n:zz,p));") (instantiate-existential ("n")) simplify (instantiate-universal-antecedent"with(p:prop,forall(n:zz,p));"("p")) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 0)") (contrapose"with(p:prop,not(p));") simplify) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 1 0)") (cut-with-single-formula"1/p<=1/n") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify))) (block (script-comment"node added by `cut-with-single-formula' at (1)") (force-substitution"1/n<=eps""eps^[-1]<=n"(0)) (block (script-comment"node added by `force-substitution' at (0)") (cut-with-single-formula"forsome(n:zz, eps^[-1]+1<=n)") (block (script-comment"node added by `cut-with-single-formula' at (0)") (instantiate-existential ("n")) (block (script-comment"node added by `instantiate-existential' at (0 0 0)") (cut-with-single-formula"0<eps^[-1]") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify)) simplify) (block (script-comment"node added by `cut-with-single-formula' at (1)") (cut-with-single-formula"forsome(n:zz,eps^[-1]+1<n)") (block (script-comment"node added by `cut-with-single-formula' at (0)") (instantiate-existential ("n")) simplify) (apply-macete-with-minor-premises archimedean))) (block (script-comment"node added by `force-substitution' at (1)") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify)))) (apply-macete-with-minor-premises characterization-of-closure-lemma-2)) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0 1 0 0)") (apply-macete-with-minor-premises characterization-of-closure-lemma-1) (instantiate-existential ("s"))) ) ))

(def-theorem closure-contains-set"forall(s:sets[pp], s subseteq closure(s))"(theory metric-spaces) (proof ( (unfold-single-defined-constant (0) closure) insistent-direct-inference-strategy (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy simplify-insistently (apply-macete-with-minor-premises open-ball-membership-condition) (instantiate-existential ("x")) simplify )) (usages transportable-macete))

(def-theorem generalized-triangle-inequality"forall(s:[zz,pp],p,q:zz, p<=q and forall(j:zz,p<=j and j<=q+1 implies #(s(j))) implies dist(s(p),s(q+1))<=sum(p,q,lambda(j:zz,dist(s(j),s(j+1)))))"(theory metric-spaces) (proof ( (induction integer-inductor ()) (prove-by-logic-and-simplification 3) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises triangle-inequality-alternate-form) (instantiate-existential ("s(1+t)")) simplify-with-minor-premises (backchain"with(p:prop,a,b:rr, p implies a<=b)") direct-and-antecedent-inference-strategy (backchain"with(q:prop,a:pp, forall(j:zz, q implies #(a)))") simplify (backchain"with(q:prop,a:pp, forall(j:zz, q implies #(a)))") simplify direct-and-antecedent-inference-strategy (backchain"with(q:prop,a:pp, forall(j:zz, q implies #(a)))") simplify ) ) )

(def-theorem dist-continuity-lemma"forall(x,y,z:pp, abs(dist(x,z)-dist(y,z))<=dist(x,y))"(theory metric-spaces) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) abs) (cut-with-single-formula"dist(x,z)<=dist(x,y)+dist(y,z) and dist(y,z)<=dist(y,x)+dist(x,z)") (prove-by-logic-and-simplification 3) (apply-macete-with-minor-premises triangle-inequality-for-distance) )))