;;; Proof of the Irrationality of the Square Root of a Non Perfect Square
;;;
;;; William M. Farmer
;;; 4-JAN-2002
;;;
;;; Outline of proof:
;;;
;;; 1. The notion of the "divisor power" of d in n is defined for
;;; natural numbers d and n. divisor%power(d,n) denotes the
;;; greatest m such that d^m divides n (provided such an m
;;; exists).
;;;
;;; 2. Some lemmas about divisor%power are proved.
;;;
;;; 3. The notion of a "non perfect square" is defined as a natural
;;; number k for which there is a prime p such divisor%power(p,k)
;;; is odd.
;;;
;;; 4. The main theorem, that the square root of a non perfect
;;; square is irrational, is then proved as follows. Let k be a
;;; natural number for which there is a prime p such
;;; divisor%power(p,k) is odd. Assume that sqrt(k) is rational.
;;; Then, for some natural numbers m and n, k*n*n = m*m. It
;;; follows that divisor%power(p,k*n*n) is odd and
;;; divisor%power(p,m*m) is even, which is a contradiction.
;;;
;;; 5. The irrationality of the square root of 2 is proved as a
;;; corollary of the main theorem.
(include-files
(files (imps theories/reals/mutual-interp)
(imps theories/reals/primes)
(imps theories/reals/polynomials)))
(def-constant divisor%power
"lambda(d,n:nn,
iota(m:nn, forsome(w:nn, n = d^m * w and not(d divides w))))"
(theory h-o-real-arithmetic))
(def-theorem ho-exponent-non-zero-lemma-1
exponent-non-zero-lemma-1
;; "forall(n:zz,x:rr, not(x=0) implies not(x^n = 0))"
(theory h-o-real-arithmetic)
(translation complete-ordered-field-interpretable)
(proof existing-theorem))
(def-theorem divisor%power-of-d-in-0-is-undefined
"forall(d:nn, not(#(divisor%power(d,0))))"
(theory h-o-real-arithmetic)
(proof
(
direct-inference
(unfold-single-defined-constant (0) divisor%power)
simplify
(apply-macete-with-minor-premises eliminate-iota-macete)
(cut-with-single-formula "0=d or 0m")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(apply-macete-with-minor-premises
divisor%power-characterization-lemma)
auto-instantiate-existential
)
(block
(script-comment "`antecedent-inference' at (2)")
(force-substitution "b=m" "m=b" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises
divisor%power-characterization-lemma)
auto-instantiate-existential
(incorporate-antecedent "with(m,b:nn,b>m);")
(unfold-single-defined-constant (0) >)
)
simplify
) )
simplify
)))
(def-theorem divisor%power-is-almost-total-aux
"forall(d:nn,
2<=d
implies
forall(n:zz, 1<=n implies lambda(n1:zz, #(divisor%power(d,n1)))(n)))"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises complete-induction-schema)
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula "d divides m or not(d divides m)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(incorporate-antecedent "with(m:zz,d:nn,d divides m);")
(apply-macete-with-minor-premises divisibility-lemma)
direct-and-antecedent-inference-strategy
(backchain "with(r:rr,m:zz,m=r);")
(cut-with-single-formula "1<=k and k