(def-constant monotone%between"lambda(a,b:rr, f:[rr,rr], forall(x,y:rr, a <= x and x <= b and a <= y and y <= b and x <= y implies f(x) <= f(y)))"(theory h-o-real-arithmetic))

(def-theorem monotone-fixed-point-theorem"forall(b,a:rr,f:[rr,rr], a <= b and a <= f(a) and f(b) <= b and monotone%between(a,b,f) implies forsome(z:rr,(a <= z and z <= b) and f(z)=z))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant (0) monotone%between) (apply-macete-with-minor-premises tr%knaster-fixed-point-theorem-corollary) )))

(def-constant weakly%lipschitz%between"lambda(a,b:rr,f:[rr,rr], forsome(k:rr, forall(x,y:rr, x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x))))"(theory h-o-real-arithmetic))

(def-theorem weak-lipschitz-constant-positive"forall(a,b:rr,f:[rr,rr], weakly%lipschitz%between(a,b,f) iff forsome(k:rr, 0<k and forall(x,y:rr, x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x))))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant-globally weakly%lipschitz%between) direct-and-antecedent-inference-strategy (case-split ("0<k")) auto-instantiate-existential (instantiate-existential ("1")) simplify (apply-macete-with-minor-premises transitivity-of-<=) (instantiate-existential ("0")) (case-split ("k=0")) (incorporate-antecedent"with(p:prop,forall(x,y:rr,p));") simplify (cut-with-single-formula"k*(y-x)<=0") (auto-instantiate-universal-antecedent"with(k:rr,f:[rr,rr],b,a:rr, forall(x,y:rr, x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x)));") simplify (force-substitution"k*(y-x)<=0""(-k)*0<=(-k)*(y-x)"(0)) (apply-macete-with-minor-premises monotonicity-for-multiplication) simplify simplify simplify simplify auto-instantiate-existential)))

(def-theorem weak-intermediate-value-thm"forall(a,b:rr, f:[rr,rr], f(a)<=0 and 0<=f(b) and a<=b and weakly%lipschitz%between(a,b,f) implies forsome(x:rr, a<=x and x<=b and f(x)=0))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises weak-lipschitz-constant-positive) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(x:rr, (a<=x and x<=b) and lambda(z:rr,z-f(z)/k)(x)=x)") (block (script-comment"first use the assertion.") (instantiate-existential ("x")) (incorporate-antecedent"with(p:prop,p and p);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify) (block (script-comment"now prove the assertion useing the knaster fp theorem.") (apply-macete-with-minor-premises tr%knaster-fixed-point-theorem-corollary) (incorporate-antecedent"with(p:prop,forall(x,y:rr,p));") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify direct-and-antecedent-inference-strategy-with-simplification (instantiate-universal-antecedent"with(p:prop,forall(x,y:rr,p));"("x_$0""y_$0") ) simplify) )))

(def-theorem power-fn-is-monotone"forall(n:zz, x,y:rr, 1<=n and 0<=x and x<=y implies x^n <= y^n)"(theory h-o-real-arithmetic) lemma (proof ( (induction integer-inductor ("n")) (apply-macete-with-minor-premises exp-out) (apply-macete-with-minor-premises monotone-product-lemma) simplify (case-split ("x=0")) simplify (cut-with-single-formula"0<x^t") simplify (apply-macete-with-minor-premises positivity-for-r^n) simplify )))

(def-theorem power-fn-is-weakly%lipschitz"forall(r:rr, n:zz, 1<=n implies weakly%lipschitz%between(0,r, lambda(x:rr,x^n)))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) weakly%lipschitz%between) (case-split ("r=0")) (instantiate-existential ("1")) (cut-with-single-formula"x_$0=y_$0") simplify simplify (instantiate-existential ("n*r^(n-1)")) (induction trivial-integer-inductor ("n")) simplify (cut-with-single-formula"y_$1*(y_$1^t-x_$1^t)<=t*r^t*(y_$1-x_$1) and x_$1^t*(y_$1-x_$1)<=r^t*(y_$1-x_$1)") simplify (force-substitution"t*r^t*(y_$1-x_$1)""r*(t*r^(t-1)*(y_$1-x_$1))"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify (force-substitution"0""0^t"(0)) (move-to-sibling 1) simplify (apply-macete-with-minor-premises power-fn-is-monotone) simplify simplify )))

(def-theorem nth-roots-exist"forall(x:rr, n:zz, 1<=n and 0<=x implies forsome(y:rr, 0<=y and y^n=x))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(a:rr, forsome(y:rr, 0<=y and y<=a and lambda(theta:rr, theta^n-x)(y)=0))") (antecedent-inference"with(p:prop,forsome(a:rr,p));") (instantiate-existential ("y")) (simplify-antecedent"with(p:prop,p and p and p);") (apply-macete-with-minor-premises weak-intermediate-value-thm) beta-reduce-repeatedly (force-substitution"weakly%lipschitz%between(0,a,lambda(theta:rr,theta^n-x))""weakly%lipschitz%between(0,a,lambda(theta:rr,theta^n))"(0)) (move-to-sibling 1) (unfold-single-defined-constant-globally weakly%lipschitz%between) simplify (apply-macete-with-minor-premises power-fn-is-weakly%lipschitz) simplify (case-split ("x<=1")) (instantiate-existential ("1")) simplify simplify (instantiate-existential ("x")) (induction integer-inductor ("n")) (apply-macete-with-minor-premises exp-out) (force-substitution"x""1*x"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify simplify )))

(def-theorem nth-roots-are-unique"forall(x,y:rr, n:zz, 1<=n and 0<=x and 0<=y and x^n=y^n implies x=y)"(theory h-o-real-arithmetic) (proof ( (cut-with-single-formula"forall(x,y:rr, n:zz, 1<=n and 0<=x and x<y implies x^n<y^n)") (move-to-sibling 1) direct-and-antecedent-inference-strategy (case-split ("x=0")) simplify (apply-macete-with-minor-premises positivity-for-r^n) (cut-with-single-formula"forall(t:rr, 1<t implies 1<t^n)") (instantiate-universal-antecedent"with(p:prop,forall(t:rr,p));"("y/x")) (contrapose"with(r:rr,not(1<r));") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify (incorporate-antecedent"with(r:rr,1<r);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify (apply-macete-with-minor-premises positivity-for-r^n) simplify direct-and-antecedent-inference-strategy (cut-with-single-formula"1+n*(t-1)<=t^n and 0<n*(t-1)") simplify (force-substitution"t""1+(t-1)"(1)) (apply-macete-with-minor-premises bernoullis-inequality) simplify simplify direct-and-antecedent-inference-strategy (cut-with-single-formula"x<y or x=y or y<x") (antecedent-inference"with(p:prop,p or p or p);") (instantiate-universal-antecedent"with(p:prop,forall(x,y:rr,n:zz,p));"("x""y""n")) simplify (instantiate-universal-antecedent"with(p:prop,forall(x,y:rr,n:zz,p));"("y""x""n")) simplify simplify )))

(def-constant nth%root"lambda(n:zz,x:rr, iota(y:rr, 1<=n and 0<=y and y^n=x))"(theory h-o-real-arithmetic))

(def-theorem iota-free-characterization-of-nth%root"forall(n:zz,x,y:rr, 1<=n implies (nth%root(n,x)=y iff (0<=y and y^n=x)))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant (0) nth%root) direct-and-antecedent-inference-strategy (contrapose"with(y,r:rr,r=y);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,not(p));") (contrapose"with(y,r:rr,r=y);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises nth-roots-are-unique) (instantiate-existential ("n")) )))

(def-theorem nth%root%existence"forall(n:zz, x:rr, 0 <=x and 1<=n implies #(nth%root(n,x)))"(theory h-o-real-arithmetic) (usages d-r-convergence) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(y:rr, 0<=y and nth%root(n,x)=y)") (antecedent-inference"with(p:prop,forsome(y:rr,p));") (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) simplify (apply-macete-with-minor-premises nth-roots-exist) direct-and-antecedent-inference-strategy )))

(def-theorem nth%root-power"forall(a,b:rr,n:zz,0<=a and 1<=n implies nth%root(n,a)^n=a)"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(s:rr, nth%root(n,a)=s)") (move-to-sibling 1) (instantiate-existential ("nth%root(n,a)")) simplify (antecedent-inference"with(p:prop,forsome(s:rr,p));") (backchain"with(s,r:rr,r=s);") (incorporate-antecedent"with(s,r:rr,r=s);") (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) direct-and-antecedent-inference-strategy )))

(def-theorem strict-monotonicity-of-nth%root"forall(a,b:rr, n:zz, 0<=a and a<b and 1<=n implies nth%root(n,a)<nth%root(n,b))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (case-split ("nth%root(n,b)<=nth%root(n,a)")) (move-to-sibling 2) simplify (cut-with-single-formula"not(b<=a)") (move-to-sibling 1) simplify (contrapose"with(p:prop,not(p));") (cut-with-single-formula"(nth%root(n,b))^n<=(nth%root(n,a))^n") (move-to-sibling 1) (apply-macete-with-minor-premises power-fn-is-monotone) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(s:rr, nth%root(n,b)=s)") (antecedent-inference"with(p:prop,forsome(s:rr,p));") (backchain"with(s,r:rr,r=s);") (incorporate-antecedent"with(s,r:rr,r=s);") (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) direct-and-antecedent-inference-strategy (instantiate-existential ("nth%root(n,b)")) (contrapose"with(n:zz,r:rr,r^n<=r^n);") (apply-macete-with-minor-premises nth%root-power) )))

(def-theorem monotonicity-of-nth%root"forall(a,b:rr, n:zz, 0<=a and a<=b and 1<=n implies nth%root(n,a)<=nth%root(n,b))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (case-split ("a=b")) simplify (cut-with-single-formula"nth%root(n,a)<nth%root(n,b)") simplify (apply-macete-with-minor-premises strict-monotonicity-of-nth%root) simplify)))

(def-theorem nth-root-is-multiplicative"forall(a,b:rr, n:zz, 0<=a and 0<=b and 1<=n implies nth%root(n,a*b)=nth%root(n,a)*nth%root(n,b))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(s,t:rr, nth%root(n,a)=s and nth%root(n,b)=t)") (move-to-sibling 1) (instantiate-existential ("nth%root(n,a)""nth%root(n,b)")) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(s,t:rr,p));") (backchain"with(p:prop,p and p);") (backchain"with(p:prop,p and p);") (incorporate-antecedent"with(p:prop,p and p);") (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) simplify direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)") (apply-macete-with-minor-premises positivity-for-products) simplify ) simplify ))))

(def-theorem nth%root-of-zero"forall(n:zz, 1<=n implies nth%root(n,0)=0)"(theory h-o-real-arithmetic) (proof ( direct-inference (instantiate-theorem nth%root%existence ("n""0")) (simplify-antecedent"with(p:prop,p);") direct-inference (incorporate-antecedent"with(p:prop,p);") (unfold-single-defined-constant-globally nth%root) (eliminate-defined-iota-expression 1 zero) simplify)))

(def-theorem nth%root-non-negative"forall(x:rr,n:zz, 0<=x and 1<=n implies 0<= nth%root(n,x))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem strict-monotonicity-of-nth%root ("0""x""n")) (simplify-antecedent"with(p:prop,not(p));") (cut-with-single-formula"x=0") simplify (apply-macete-with-minor-premises nth%root-of-zero) simplify (contrapose"with(r:rr,r<r);") (apply-macete-with-minor-premises nth%root-of-zero) simplify)))

(def-theorem nth%root-positive-for-positive"forall(x:rr,n:zz, 0<x and 1<=n implies 0<nth%root(n,x))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem strict-monotonicity-of-nth%root ("0""x""n")) (simplify-antecedent"with(p:prop,not(p));") (contrapose"with(x:rr,n:zz,nth%root(n,0)<nth%root(n,x));") (apply-macete-with-minor-premises nth%root-of-zero))))

(def-theorem iterated-nth%root"forall(x:rr,n,m:zz, 0<=x and 1<=n and 1<=m implies nth%root(n*m,x)=nth%root(n,nth%root(m,x)))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) (apply-macete-with-minor-premises nth%root-non-negative) (apply-macete-with-minor-premises nth%root-non-negative) (force-substitution"nth%root(n,nth%root(m,x))^(n*m)""(nth%root(n,nth%root(m,x))^(n))^m"(0)) (apply-macete-with-minor-premises nth%root-power) (apply-macete-with-minor-premises nth%root-power) simplify (apply-macete-with-minor-premises nth%root-non-negative) simplify (apply-macete-with-minor-premises product-power-is-iterated-power) (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify simplify )))