(def-theorem weak-positivity-for-r^n"forall(x:rr, n:zz, 1<=n and 0<=x implies 0<=x^n)"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (case-split ("x=0")) simplify (cut-with-single-formula"0<x^n") simplify (apply-macete-with-minor-premises positivity-for-r^n) simplify direct-and-antecedent-inference-strategy )))

(def-theorem positive-rational-characterization"forall(s:qq, 0<s implies forsome(m,n:zz, 1<=m and 1<=n and s=m/n))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, s=m/n)") (move-to-sibling 1) (apply-macete-with-minor-premises zz-quotient-field) (antecedent-inference"with(p:prop,forsome(m,n:zz,p));") (cut-with-single-formula"0=m or 0<m or m<0") (move-to-sibling 1) simplify (antecedent-inference"with(p:prop,p or p or p);") (simplify-antecedent"with(n,m:zz,s:qq,s=m/n);") (instantiate-existential ("m""n")) simplify (contrapose"with(r:rr,s:qq,s=r);") (cut-with-single-formula"n<0 or n=0") (antecedent-inference"with(p:prop,p or p);") (apply-macete-with-minor-premises fractional-expression-manipulation) (cut-with-single-formula"0<(-s)*n") simplify simplify simplify simplify (instantiate-existential ("-m""-n")) (incorporate-antecedent"with(r:rr,s:qq,s=r);") simplify (contrapose"with(r:rr,s:qq,s=r);") (cut-with-single-formula"n=0 or 0<n") (move-to-sibling 1) simplify (antecedent-inference"with(p:prop,p or p);") simplify (apply-macete-with-minor-premises fractional-expression-manipulation) (cut-with-single-formula"0<s*n") simplify simplify (incorporate-antecedent"with(r:rr,s:qq,s=r);") simplify )))

(def-theorem rational-power-lemma-1"forall(x:rr, m,n,p:zz, 1<=n and 1<=m and 1<=p and 0<=x implies nth%root(p*n,x^(p*m))= nth%root(n,x^m))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises nth%root-non-negative) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(s:rr, nth%root(n,x^m)=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 (cut-with-single-formula"(s^n)^p=(x^m)^p") (move-to-sibling 1) (backchain"with(r:rr,r=r);") simplify simplify (instantiate-existential ("nth%root(n,x^m)")) (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify simplify )))

(def-theorem rational-power-lemma-2"forall(x:rr, m,n,p,q:zz, 1<=n and 1<=m and 1<=p and 1<=q and 0<=x and m/n=p/q implies nth%root(n,x^m)=nth%root(q,x^p))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises fractional-expression-manipulation) direct-and-antecedent-inference-strategy (cut-with-single-formula"nth%root(n,x^m)=nth%root(q*n,x^(q*m)) and nth%root(n*q,x^(n*p))=nth%root(q,x^p)") (move-to-sibling 1) (apply-macete-with-minor-premises rational-power-lemma-1) simplify (apply-macete-with-minor-premises nth%root%existence) (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (backchain"with(p:prop,p and p);") (antecedent-inference"with(p:prop,p and p);") (force-substitution"q*m""n*p"(0)) (move-to-sibling 1) simplify (force-substitution"q*n""n*q"(0)) simplify)))

(def-theorem rational-power-lemma-3"forall(x:rr, m,n,p:zz, 1<=n and 1<=m and 0<=x implies nth%root(n,x^m)= nth%root(n,x)^m)"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises iota-free-characterization-of-nth%root) (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises nth%root-non-negative) simplify (force-substitution"(nth%root(n,x)^m)^n""(nth%root(n,x)^n)^m"(0)) (apply-macete-with-minor-premises nth%root-power) simplify simplify )))

(def-constant posrat%exp"lambda(x:rr, s:qq, if(s<=0 or x<0,?rr, iota(r:rr, forall(m,n:zz,1<=m and 1<=n and s=m/n implies r=nth%root(n,x^m)))))"(theory h-o-real-arithmetic))

(def-theorem posrat%exp-characterization"forall(x:rr, m,n:zz,1<=m and 1<=n and 0<=x implies posrat%exp(x,m/n)=nth%root(n,x^m))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant (0) posrat%exp) (raise-conditional (0)) direct-and-antecedent-inference-strategy (contrapose"with(r:rr,r<=0);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify (simplify-antecedent"with(x:rr,x<0);") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises rational-power-lemma-2) direct-and-antecedent-inference-strategy simplify (apply-macete-with-minor-premises nth%root%existence) (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy )))

(def-theorem posrat%exp-definedness"forall(x:rr, s:qq,0<s and 0<=x implies #(posrat%exp(x,s)))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, s=m/n and 1<=m and 1<=n)") (antecedent-inference"with(p:prop,forsome(m,n:zz,p));") (backchain"with(p:prop,p and p and p);") (apply-macete-with-minor-premises posrat%exp-characterization) (apply-macete-with-minor-premises nth%root%existence) (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (instantiate-theorem positive-rational-characterization ("s")) auto-instantiate-existential )))

(def-theorem posrat%exp-nonnegative"forall(x:rr, s:qq, 0<s and 0<=x implies 0<=posrat%exp(x,s))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, 1<=m and 1<=n and s=m/n) ") (move-to-sibling 1) (apply-macete-with-minor-premises positive-rational-characterization) (antecedent-inference"with(p:prop,forsome(m,n:zz,p));") (backchain"with(p:prop,p and p and p);") (apply-macete-with-minor-premises posrat%exp-characterization) (apply-macete-with-minor-premises nth%root-non-negative) (apply-macete-with-minor-premises weak-positivity-for-r^n) simplify )))

(def-theorem posrat%exp-additive-property"forall(x:rr, s,t:qq,0<s and 0<t and 0<=x implies posrat%exp(x,s+t)=posrat%exp(x,s)*posrat%exp(x,t))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, 1<=m and 1<=n and s=m/n) and forsome(m,n:zz, 1<=m and 1<=n and t=m/n)") (move-to-sibling 1) (apply-macete-with-minor-premises positive-rational-characterization) direct-and-antecedent-inference-strategy (antecedent-inference-strategy (0)) (backchain-repeatedly ("with(n_$0,m_$0:zz,s:qq,s=m_$0/n_$0);")) (backchain-repeatedly ("with(n,m:zz,t:qq,t=m/n);")) (apply-macete-with-minor-premises fractional-expression-manipulation) (apply-macete-with-minor-premises posrat%exp-characterization) (move-to-sibling 1) (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify simplify (move-to-sibling 2) (cut-with-single-formula"1<=m_$0*n and 0<=n_$0*m") simplify (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify (force-substitution"x^(n_$0*m+n*m_$0)""x^(n_$0*m)*x^(n*m_$0)"(0)) (move-to-sibling 1) simplify (apply-macete-with-minor-premises nth-root-is-multiplicative) (force-substitution"n*n_$0""n_$0*n"(0)) (move-to-sibling 1) simplify (apply-macete-with-minor-premises rational-power-lemma-1) simplify (apply-macete-with-minor-premises nth%root%existence) (apply-macete-with-minor-premises weak-positivity-for-r^n) simplify (apply-macete-with-minor-premises weak-positivity-for-r^n) simplify (apply-macete-with-minor-premises weak-positivity-for-r^n) simplify )))

(def-theorem posrat%exp-multiplicative-property"forall(x,y:rr, s,t:qq,0<s and 0<=x and 0<=y implies posrat%exp(x*y,s)=posrat%exp(x,s)*posrat%exp(y,s))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, 1<=m and 1<=n and s=m/n) ") (move-to-sibling 1) (apply-macete-with-minor-premises positive-rational-characterization) (antecedent-inference-strategy (0)) (backchain-repeatedly ("with(n_$0,m_$0:zz,s:qq,s=m_$0/n_$0);")) (apply-macete-with-minor-premises posrat%exp-characterization) simplify (apply-macete-with-minor-premises nth-root-is-multiplicative) simplify (apply-macete-with-minor-premises nth%root%existence) (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises weak-positivity-for-r^n) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises weak-positivity-for-r^n) (apply-macete-with-minor-premises positivity-for-products) direct-and-antecedent-inference-strategy )))

(def-theorem posrat%exp-iterated-exponent-property"forall(x,y:rr, s,t:qq,0<s and 0<t and 0<=x implies posrat%exp(x,s*t)=posrat%exp(posrat%exp(x,s),t))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m,n:zz, 1<=m and 1<=n and s=m/n) and forsome(m,n:zz, 1<=m and 1<=n and t=m/n)") (move-to-sibling 1) (apply-macete-with-minor-premises positive-rational-characterization) direct-and-antecedent-inference-strategy (antecedent-inference-strategy (0)) (backchain-repeatedly ("with(n_$0,m_$0:zz,s:qq,s=m_$0/n_$0);")) (backchain-repeatedly ("with(n,m:zz,t:qq,t=m/n);")) (apply-macete-with-minor-premises fractional-expression-manipulation) (apply-macete-with-minor-premises posrat%exp-characterization) (move-to-sibling 1) (apply-macete-with-minor-premises posrat%exp-nonnegative) direct-and-antecedent-inference-strategy (move-to-sibling 2) (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify simplify (apply-macete-with-minor-premises posrat%exp-characterization) (apply-macete-with-minor-premises iterated-nth%root) (move-to-sibling 1) (apply-macete-with-minor-premises weak-positivity-for-r^n) (force-substitution"1""1*1"(0)) (apply-macete-with-minor-premises monotone-product-lemma) simplify (apply-macete-with-minor-premises rational-power-lemma-3) (move-to-sibling 1) (apply-macete-with-minor-premises nth%root-non-negative) (apply-macete-with-minor-premises weak-positivity-for-r^n) simplify (apply-macete-with-minor-premises rational-power-lemma-3) (move-to-sibling 1) (apply-macete-with-minor-premises nth%root-non-negative) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises rational-power-lemma-3) simplify (force-substitution"1""1*1"(0)) )))