```
(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
)))
```

```
"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))
)))
```