(def-theorem exponential-monotonicity-lemma
*"forall(n:zz,2<=n implies (1+1/(n-1))^(n-1)<=(1+1/n)^n)"*
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula *"1-1/n<=(1-1/n^2)^n"*)
(cut-with-single-formula *"n^(2*n)*(n-1)<=n*(n^2-1)^n"*)
(weaken (1))
(cut-with-single-formula *"n*(n^2-1)^n=n*(n+1)^n*(n-1)^(n-1)*(n-1)"*)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(contrapose *"with(n:zz,n^(2*n)*(n-1)<=n*(n^2-1)^n);"*)
(backchain *"with(n:zz,n*(n^2-1)^n=n*(n+1)^n*(n-1)^(n-1)*(n-1));"*)
(force-substitution *"n^(2*n)"* *"n^(2*n-1)*n"* (0))
simplify
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
(apply-macete-with-minor-premises positivity-for-r^n)
simplify
(cut-with-single-formula *"forall(x,y:rr,m:zz,1<=m implies x^m*y^m=(x*y)^m)"*)
(backchain *"forall(x,y:rr,m:zz,1<=m implies x^m*y^m=(x*y)^m);"*)
simplify
simplify
(incorporate-antecedent *"with(n:zz,1-1/n<=(1-1/n^2)^n);"*)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
(cut-with-single-formula *"1+n*(-1/n^2)<=(1+(-1/n^2))^n"*)
simplify
(apply-macete-with-minor-premises bernoullis-inequality)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(force-substitution *"1<n^2"* *"0<(n-1)*(n+1)"* (0))
(apply-macete-with-minor-premises strict-positivity-for-products)
simplify
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
simplify
)))

(def-theorem sum-lte-product
*"forall(x,y:rr, 2<=x and 2<=y implies x+y<=x*y)"*
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula *"1/x+1/y<=1"*)
(incorporate-antecedent *"with(r:rr,r<=1);"*)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(cut-with-single-formula *"1/x<=1/2 and 1/y<=1/2"*)
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
)))