```
(def-theorem archimedean
"forall(a:rr,forsome(n:zz,a<n))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem completeness ("lambda(j:zz, truth)"))
(block (script-comment "node added by `instantiate-theorem' at (0 0 0)")
(instantiate-universal-antecedent "with(p:prop,p);" ("1"))
(contrapose "with(p:prop,p);")
simplify)
(block (script-comment "node added by `instantiate-theorem' at (0 0 1)")
(contrapose "with(p:prop,p);")
(instantiate-existential ("a"))
(instantiate-universal-antecedent "with(p:prop,forall(n:zz,p));"
("theta"))
simplify)
(block (script-comment "node added by `instantiate-theorem' at (0 1 0 0)")
(contrapose "with(gamma:rr,p:prop,
forall(gamma_1:rr,
forall(theta:rr,p) implies gamma<=gamma_1));")
(instantiate-existential ("gamma-1"))
(prove-by-logic-and-simplification 3)
simplify)
)))
```

```
(def-constant convergent%to%infinity
"lambda(s:[zz,rr],
forall(m:rr,forsome(x:zz, forall(j:zz, x<=j implies m<=s(j)))))"
(theory h-o-real-arithmetic))
```

```
(def-theorem convergent%to%infinity-linear-form
"forall(a,b:rr, 0<a implies convergent%to%infinity(lambda(j:zz,a*j+b)))"
(theory h-o-real-arithmetic)

(proof
(
(unfold-single-defined-constant (0) convergent%to%infinity)
direct-and-antecedent-inference-strategy
(force-substitution "forall(j_\$0:zz,x_\$0<=j_\$0 implies m_\$0<=a*j_\$0+b)" "a^[-1]*(m_\$0-b)<x_\$0" (0))
(apply-macete-with-minor-premises archimedean)
(force-substitution "m_\$0<=a*j_\$0+b" "a^[-1]*(m_\$0-b)<j_\$0" (0))
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
)))
```

```
(def-theorem bernoullis-inequality
"forall(h:rr,n:zz,-1<h and 1<=n implies 1+n*h<=(1+h)^n)"
(theory h-o-real-arithmetic)
(proof
(
(induction integer-inductor ("n"))
(cut-with-single-formula "0<=t*h^2 and (1+h)*(1+h*t)<=(1+h)*(1+h)^t")
simplify
simplify
)))
```

```
(def-theorem unbounded-heredity
"forall(s,t:[zz,rr],convergent%to%infinity(s) and forsome(m:zz,forall(n:zz,m<=n implies s(n)<=t(n))) implies convergent%to%infinity(t))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(m:rr,forsome(x:zz,p)));"
("m"))
(instantiate-existential ("max(m_\$0,x)"))
(apply-macete-with-minor-premises transitivity-of-<=)
(block (script-comment "node added by `apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("s(j_\$0)"))
(block (script-comment "node added by `instantiate-existential' at (0 0)")
(backchain "with(s:[zz,rr],m:rr,x:zz,forall(j:zz,x<=j implies m<=s(j)));")
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("max(m_\$0,x)"))
(apply-macete-with-minor-premises maximum-2nd-arg))
(block (script-comment "node added by `instantiate-existential' at (0 1)")
(backchain "with(t,s:[zz,rr],m_\$0:zz,
forall(n:zz,m_\$0<=n implies s(n)<=t(n)));")
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("max(m_\$0,x)"))
(apply-macete-with-minor-premises maximum-1st-arg))
(cut-with-single-formula "s(j_\$0)<=t(j_\$0)"))
(cut-with-single-formula "s(j_\$0)<=t(j_\$0)"))))
```

```
(def-theorem r^n-convergent-to-infinity
"forall(r:rr,1<r implies convergent%to%infinity(lambda(n:zz,r^n)))"
(theory h-o-real-arithmetic)
(proof
(

direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises unbounded-heredity)
(instantiate-existential ("lambda(k:zz, (r-1)*k+1)"))
(block (script-comment "node added by `instantiate-existential' at (0 0)")
(apply-macete-with-minor-premises convergent%to%infinity-linear-form)
simplify)
(block (script-comment "node added by `instantiate-existential' at (0 1)")
beta-reduce-repeatedly
(force-substitution "(r-1)*n_\$0+1<=r^n_\$0"
"1+n_\$0*(r-1)<=(1+(r-1))^n_\$0"
(0))
(block (script-comment "node added by `force-substitution' at (0)")
(apply-macete-with-minor-premises bernoullis-inequality)
(instantiate-existential ("1"))
simplify)
simplify)
)))
```

```
(def-theorem complete-induction
"forall(p:[zz,prop],n:zz,
forall(m:zz,
n<=m and forall(k:zz,n<=k and k<m implies p(k))
implies
p(m))
implies
forall(k:zz,n<=k implies p(k)))"
(theory h-o-real-arithmetic)
(proof
(

direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(k:zz,n<=k implies forall(s:zz, n<=s and s<= k implies p(s)))")
(block (script-comment "node added by `cut-with-single-formula' at (0)")
(backchain "with(p:prop,n:zz,forall(k:zz,n<=k implies forall(s:zz,p)));")
(instantiate-existential ("k"))
simplify)
(block (script-comment "node added by `cut-with-single-formula' at (1)")
(weaken (0))
(induction integer-inductor ())
(block (script-comment "node added by `induction' at (0 0 0)")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(m:zz,p));")
direct-and-antecedent-inference-strategy
(contrapose "with(n,s_\$0:zz,s_\$0<=n);")
simplify)
(prove-by-logic-and-simplification 3))
)))
```

```
(def-theorem complete-induction-schema
Remark: This entry is multiply defined. See:  [1] [2]
"forall(p:[zz,prop],n:zz,
forall(k:zz,n<=k implies p(k))
iff
(truth
and
forall(m:zz,
n<=m and forall(k:zz,n<=k and k<m implies p(k))
implies
p(m))))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(p:[zz,prop],n:zz,forall(k:zz,n<=k implies p(k)));")
(apply-macete-with-minor-premises complete-induction)
(instantiate-existential ("n"))
)))
```

```(def-inductor complete-inductor
complete-induction-schema
(theory h-o-real-arithmetic))
```

```
(def-theorem well-ordering-for-integers
"forall(s:[zz,prop],forsome(y:zz,s(y)) and
forsome(n:zz, forall(m:zz,m<=n implies not(s(m))))
implies
forsome(u:zz, s(u) and forall(v:zz,v<u implies not s(v))))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(y:zz,s:[zz,prop],s(y));")
(cut-with-single-formula "y<=n or n<=y")
(antecedent-inference "with(n,y:zz,y<=n or n<=y);")
(backchain "with(s:[zz,prop],n:zz,forall(m:zz,m<=n implies not(s(m))));")
(incorporate-antecedent "with(y,n:zz,n<=y);")
(force-substitution "not s(y)" "lambda (z:zz,not s(z))(y)" (0))
(apply-macete-with-minor-premises complete-induction)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("n"))
(backchain "with(s:[zz,prop],
forall(u:zz,not(s(u)) or forsome(v:zz,v<u and s(v))));")
direct-and-antecedent-inference-strategy
(case-split ("n<=v"))
(prove-by-logic-and-simplification 3)
simplify
beta-reduce-repeatedly
simplify
)))
```

```
(def-constant set%min
"lambda(s:sets[zz], iota(k:zz, k in s and forall(j:zz, j<k implies not(j in s))))"
(theory h-o-real-arithmetic))
```

```
(def-theorem iota-free-characterization-of-set%min
"forall(s:sets[zz],k:zz,  set%min(s)=k iff (k in s and forall(j:zz, j<k implies not(j in s))))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally set%min)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(contrapose "with(p:prop,p);")
(apply-macete-with-minor-premises eliminate-iota-macete)
(contrapose "with(p:prop,p);"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
(contrapose "with(k,z:zz,z=k);")
(apply-macete-with-minor-premises eliminate-iota-macete)
(contrapose "with(j:zz,s:sets[zz],j in s);")
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
(contrapose "with(b:zz,s:sets[zz],b in s);")
(backchain "with(s:sets[zz],k:zz,forall(j:zz,j<k implies not(j in s)));")
(contrapose "with(k:zz,s:sets[zz],k in s);")
(backchain "with(s:sets[zz],b:zz,forall(j:zz,j<b implies not(j in s)));")
simplify)
)))
```

```
(def-theorem definedness-of-set%min
"forall(s:sets[zz],
#(set%min(s)) iff
(forsome(k:zz, k in s) and forsome(k:zz, forall(j:zz, j<=k implies not(j in s)))))"
(theory h-o-real-arithmetic)
(proof
(
direct-inference
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(cut-with-single-formula "forsome(k:zz, set%min(s)=k)")
(move-to-sibling 1)
(instantiate-existential ("set%min(s)"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(k:zz,p));")
(incorporate-antecedent "with(k,z:zz,z=k);")
(apply-macete-with-minor-premises iota-free-characterization-of-set%min)
direct-and-antecedent-inference-strategy
(instantiate-existential ("k"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(instantiate-existential ("k-1"))
simplify)))
(block
(script-comment "`direct-inference' at (1)")
(cut-with-single-formula "forsome(k:zz, set%min(s)=k)")
(antecedent-inference "with(p:prop,forsome(k:zz,p));")
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises iota-free-characterization-of-set%min)
(instantiate-theorem well-ordering-for-integers
("lambda(k:zz, k in s)"))
(block
(script-comment "`instantiate-theorem' at (0 0 0)")
(contrapose "with(p:prop,forall(y:zz,p));")
simplify-insistently)
(block
(script-comment "`instantiate-theorem' at (0 0 1)")
(contrapose "with(p:prop,forall(n:zz,p));")
simplify)
(block
(script-comment "`instantiate-theorem' at (0 1 0 0)")
(beta-reduce-antecedent "with(s:sets[zz],u:zz,
forall(v:zz,v<u implies not(lambda(k:zz,k in s)(v))));")
(beta-reduce-antecedent "with(u:zz,s:sets[zz],lambda(k:zz,k in s)(u));")
(instantiate-existential ("u")))))
)))
```

```
(def-theorem well-ordering-for-natural-numbers
"forall(s:[nn,prop],
nonvacuous_q{s}
implies
forsome(u:nn, s(u) and forall(v:nn,v<u implies not s(v))))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem well-ordering-for-integers ("s"))
(instantiate-universal-antecedent "with(p:prop, forall(y:zz,p))" ("x_0"))
(instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("[-1]"))
(cut-with-single-formula "not(#(m,nn))")
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
auto-instantiate-existential
(backchain "with(p:prop, forall(v:zz,p))")
)))
```

```
(def-constant floor
"lambda(x:rr, iota(z:zz,z<=x and x<1+z))"
(theory h-o-real-arithmetic))
```

```
(def-theorem floor-definedness
"forall(x:rr, #(floor(x)))"
(usages d-r-convergence)
(proof
(
insistent-direct-inference
unfold-defined-constants
(eliminate-iota 0)
(cut-with-single-formula "forsome(y%iota:zz,y%iota<=x and x<1+y%iota)")
(instantiate-existential ("y%iota"))
simplify
(instantiate-theorem well-ordering-for-integers ("lambda(u:zz,x<u)"))
(contrapose 0)
beta-reduce-insistently
(apply-macete-with-minor-premises archimedean)
(contrapose 0)
(cut-with-single-formula "forsome(u:zz,-x<u)")
(instantiate-existential ("-u"))
simplify
(apply-macete-with-minor-premises archimedean)
(instantiate-existential ("u-1"))
(instantiate-universal-antecedent 0 ("u-1"))
simplify
(contrapose 0)
simplify
(simplify-antecedent 0)
simplify
))

(theory h-o-real-arithmetic))
```

```
(def-theorem floor-characterization
"forall(x:rr, n:zz, floor(x)=n iff (n<=x and x<n+1))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) floor)
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-and-antecedent-inference-strategy
simplify
simplify
simplify
)))
```

```
(def-theorem floor-below-arg
"forall(x:rr, floor(x)<=x)"
(theory h-o-real-arithmetic)
(proof
(
direct-inference
(instantiate-theorem floor-definedness ("x"))
(incorporate-antecedent "with(p:prop,p);")
(unfold-single-defined-constant-globally floor)
direct-and-antecedent-inference-strategy
(eliminate-defined-iota-expression 0 i))))
```

```
(def-theorem floor-plus-1-exceeds-arg
"forall(x:rr, x<1+floor(x))"
(theory h-o-real-arithmetic)
(proof
(
direct-inference
(instantiate-theorem floor-definedness ("x"))
(incorporate-antecedent "with(p:prop,p);")
(unfold-single-defined-constant-globally floor)
direct-and-antecedent-inference-strategy
(eliminate-defined-iota-expression 0 i))))
```

```
(def-theorem floor-not-much-below-arg
"forall(x:rr, n:zz, n<=x implies n<=floor(x))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem floor-definedness ("x"))
(incorporate-antecedent "with(z:zz,#(z));")
(unfold-single-defined-constant-globally floor)
direct-and-antecedent-inference-strategy
(eliminate-defined-iota-expression 0 f)
simplify)))
```

```
(def-theorem floor-inequality-characterization
"forall(x,y:rr, (floor(x)<=floor(y) iff floor(x)<=y))"
(theory h-o-real-arithmetic)
(proof
(direct-and-antecedent-inference-strategy-with-simplification)))
```

```
(def-theorem monotonicity-of-floor
"forall(x,y:rr, x<=y implies floor(x)<=floor(y))"
(theory h-o-real-arithmetic)
(proof
(simplify)))
```

```
(def-theorem integer-exponentiation-definedness
"forall(m,n:zz, 1<=n implies #(m^n,zz))"
(theory h-o-real-arithmetic)
(proof
(
(induction integer-inductor ())
(apply-macete-with-minor-premises exp-out)
sort-definedness
simplify)))
```

```
(def-theorem integer-exponentiation-definedness-dr
"forall(m,n:ind, #(m,zz) and #(n,zz) and 1<=n implies #(m^n,zz))"
(usages d-r-convergence)
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises integer-exponentiation-definedness)
simplify)))
```

```
(def-theorem product-power-is-iterated-power
"forall(z:rr, n,m:zz, 1<=n and 1<=m implies z^(n*m) ==(z^n)^m)"
(theory h-o-real-arithmetic)
(proof
(
simplify)))
```

```
(def-constant mod
"lambda(a,b:rr, a-b*floor(a/b))"
(theory h-o-real-arithmetic))
```

```
(def-theorem mod-of-negative
"forall(a,b:rr, mod(-b,-a)==-mod(b,a))"
(theory h-o-real-arithmetic)
(proof
(

(unfold-single-defined-constant-globally mod)
simplify
)))
```

```
(def-constant div
"lambda(x,y:rr, floor(x/y))"
(theory h-o-real-arithmetic))
```

```
(def-theorem mod-of-integer-is-integer
"forall(a,b:zz, not(b=0) implies #(a mod b,zz))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) mod)
sort-definedness
)))
```