# Theory Primes

Up to index of Isabelle/ZF/ex

theory Primes
imports Main
begin

    (*  Title:      ZF/ex/Primes.thy
        ID:         $Id: Primes.thy,v 1.10 2005/06/17 14:15:11 haftmann Exp $
        Author:     Christophe Tabacznyj and Lawrence C Paulson
        Copyright   1996  University of Cambridge
    *)

    header{*The Divides Relation and Euclid's algorithm for the GCD*}

    theory Primes imports Main begin
    constdefs
      divides :: "[i,i]=>o"              (infixl "dvd" 50)
        "m dvd n == m ∈ nat & n ∈ nat & (∃k ∈ nat. n = m#*k)"

      is_gcd  :: "[i,i,i]=>o"     --{*definition of great common divisor*}
        "is_gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
                           (∀d∈nat. (d dvd m) & (d dvd n) --> d dvd p)"

      gcd     :: "[i,i]=>i"       --{*Euclid's algorithm for the gcd*}
        "gcd(m,n) == transrec(natify(n),
                            %n f. λm ∈ nat.
                                    if n=0 then m else f`(m mod n)`n) ` natify(m)"

      coprime :: "[i,i]=>o"       --{*the coprime relation*}
        "coprime(m,n) == gcd(m,n) = 1"

      prime   :: i                --{*the set of prime numbers*}
       "prime == {p ∈ nat. 1<p & (∀m ∈ nat. m dvd p --> m=1 | m=p)}"

    subsection{*The Divides Relation*}

    lemma dvdD: "m dvd n ==> m ∈ nat & n ∈ nat & (∃k ∈ nat. n = m#*k)"
    by (unfold divides_def, assumption)

    lemma dvdE:
         "[|m dvd n;  !!k. [|m ∈ nat; n ∈ nat; k ∈ nat; n = m#*k|] ==> P|] ==> P"
    by (blast dest!: dvdD)

    lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard]
    lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard]

    lemma dvd_0_right [simp]: "m ∈ nat ==> m dvd 0"
    apply (simp add: divides_def)
    apply (fast intro: nat_0I mult_0_right [symmetric])
    done

    lemma dvd_0_left: "0 dvd m ==> m = 0"
    by (simp add: divides_def)

    lemma dvd_refl [simp]: "m ∈ nat ==> m dvd m"
    apply (simp add: divides_def)
    apply (fast intro: nat_1I mult_1_right [symmetric])
    done

    lemma dvd_trans: "[| m dvd n; n dvd p |] ==> m dvd p"
    by (auto simp add: divides_def intro: mult_assoc mult_type)

    lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m=n"
    apply (simp add: divides_def)
    apply (force dest: mult_eq_self_implies_10
                 simp add: mult_assoc mult_eq_1_iff)
    done

    lemma dvd_mult_left: "[|(i#*j) dvd k; i ∈ nat|] ==> i dvd k"
    by (auto simp add: divides_def mult_assoc)

    lemma dvd_mult_right: "[|(i#*j) dvd k; j ∈ nat|] ==> j dvd k"
    apply (simp add: divides_def, clarify)
    apply (rule_tac x = "i#*k" in bexI)
    apply (simp add: mult_ac)
    apply (rule mult_type)
    done

    subsection{*Euclid's Algorithm for the GCD*}

    lemma gcd_0 [simp]: "gcd(m,0) = natify(m)"
    apply (simp add: gcd_def)
    apply (subst transrec, simp)
    done

    lemma gcd_natify1 [simp]: "gcd(natify(m),n) = gcd(m,n)"
    by (simp add: gcd_def)

    lemma gcd_natify2 [simp]: "gcd(m, natify(n)) = gcd(m,n)"
    by (simp add: gcd_def)

    lemma gcd_non_0_raw:
        "[| 0<n;  n ∈ nat |] ==> gcd(m,n) = gcd(n, m mod n)"
    apply (simp add: gcd_def)
    apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
    apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
                     mod_less_divisor [THEN ltD])
    done

    lemma gcd_non_0: "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)"
    apply (cut_tac m = m and n = "natify (n) " in gcd_non_0_raw)
    apply auto
    done

    lemma gcd_1 [simp]: "gcd(m,1) = 1"
    by (simp (no_asm_simp) add: gcd_non_0)

    lemma dvd_add: "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)"
    apply (simp add: divides_def)
    apply (fast intro: add_mult_distrib_left [symmetric] add_type)
    done

    lemma dvd_mult: "k dvd n ==> k dvd (m #* n)"
    apply (simp add: divides_def)
    apply (fast intro: mult_left_commute mult_type)
    done

    lemma dvd_mult2: "k dvd m ==> k dvd (m #* n)"
    apply (subst mult_commute)
    apply (blast intro: dvd_mult)
    done

    (* k dvd (m*k) *)
    lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard]
    lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard]

    lemma dvd_mod_imp_dvd_raw:
         "[| a ∈ nat; b ∈ nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
    apply (case_tac "b=0")
     apply (simp add: DIVISION_BY_ZERO_MOD)
    apply (blast intro: mod_div_equality [THEN subst]
                 elim: dvdE
                 intro!: dvd_add dvd_mult mult_type mod_type div_type)
    done

    lemma dvd_mod_imp_dvd: "[| k dvd (a mod b); k dvd b; a ∈ nat |] ==> k dvd a"
    apply (cut_tac b = "natify (b)" in dvd_mod_imp_dvd_raw)
    apply auto
    apply (simp add: divides_def)
    done

    (*Imitating TFL*)
    lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n ∈ nat;
             ∀m ∈ nat. P(m,0);
             ∀m ∈ nat. ∀n ∈ nat. 0<n --> P(n, m mod n) --> P(m,n) |]
          ==> ∀m ∈ nat. P (m,n)"
    apply (erule_tac i = n in complete_induct)
    apply (case_tac "x=0")
    apply (simp (no_asm_simp))
    apply clarify
    apply (drule_tac x1 = m and x = x in bspec [THEN bspec])
    apply (simp_all add: Ord_0_lt_iff)
    apply (blast intro: mod_less_divisor [THEN ltD])
    done

    lemma gcd_induct: "!!P. [| m ∈ nat; n ∈ nat;
             !!m. m ∈ nat ==> P(m,0);
             !!m n. [|m ∈ nat; n ∈ nat; 0<n; P(n, m mod n)|] ==> P(m,n) |]
          ==> P (m,n)"
    by (blast intro: gcd_induct_lemma)

    subsection{*Basic Properties of @{term gcd}*}

    text{*type of gcd*}
    lemma gcd_type [simp,TC]: "gcd(m, n) ∈ nat"
    apply (subgoal_tac "gcd (natify (m), natify (n)) ∈ nat")
    apply simp
    apply (rule_tac m = "natify (m)" and n = "natify (n)" in gcd_induct)
    apply auto
    apply (simp add: gcd_non_0)
    done

    text{* Property 1: gcd(a,b) divides a and b *}

    lemma gcd_dvd_both:
         "[| m ∈ nat; n ∈ nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n"
    apply (rule_tac m = m and n = n in gcd_induct)
    apply (simp_all add: gcd_non_0)
    apply (blast intro: dvd_mod_imp_dvd_raw nat_into_Ord [THEN Ord_0_lt])
    done

    lemma gcd_dvd1 [simp]: "m ∈ nat ==> gcd(m,n) dvd m"
    apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
    apply auto
    done

    lemma gcd_dvd2 [simp]: "n ∈ nat ==> gcd(m,n) dvd n"
    apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_dvd_both)
    apply auto
    done

    text{* if f divides a and b then f divides gcd(a,b) *}

    lemma dvd_mod: "[| f dvd a; f dvd b |] ==> f dvd (a mod b)"
    apply (simp add: divides_def)
    apply (case_tac "b=0")
     apply (simp add: DIVISION_BY_ZERO_MOD, auto)
    apply (blast intro: mod_mult_distrib2 [symmetric])
    done

    text{* Property 2: for all a,b,f naturals,
                   if f divides a and f divides b then f divides gcd(a,b)*}

    lemma gcd_greatest_raw [rule_format]:
         "[| m ∈ nat; n ∈ nat; f ∈ nat |]
          ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
    apply (rule_tac m = m and n = n in gcd_induct)
    apply (simp_all add: gcd_non_0 dvd_mod)
    done

    lemma gcd_greatest: "[| f dvd m;  f dvd n;  f ∈ nat |] ==> f dvd gcd(m,n)"
    apply (rule gcd_greatest_raw)
    apply (auto simp add: divides_def)
    done

    lemma gcd_greatest_iff [simp]: "[| k ∈ nat; m ∈ nat; n ∈ nat |]
          ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)"
    by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)

    subsection{*The Greatest Common Divisor*}

    text{*The GCD exists and function gcd computes it.*}

    lemma is_gcd: "[| m ∈ nat; n ∈ nat |] ==> is_gcd(gcd(m,n), m, n)"
    by (simp add: is_gcd_def)

    text{*The GCD is unique*}

    lemma is_gcd_unique: "[|is_gcd(m,a,b); is_gcd(n,a,b); m∈nat; n∈nat|] ==> m=n"
    apply (simp add: is_gcd_def)
    apply (blast intro: dvd_anti_sym)
    done

    lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
    by (simp add: is_gcd_def, blast)

    lemma gcd_commute_raw: "[| m ∈ nat; n ∈ nat |] ==> gcd(m,n) = gcd(n,m)"
    apply (rule is_gcd_unique)
    apply (rule is_gcd)
    apply (rule_tac [3] is_gcd_commute [THEN iffD1])
    apply (rule_tac [3] is_gcd, auto)
    done

    lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
    apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_commute_raw)
    apply auto
    done

    lemma gcd_assoc_raw: "[| k ∈ nat; m ∈ nat; n ∈ nat |]
          ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
    apply (rule is_gcd_unique)
    apply (rule is_gcd)
    apply (simp_all add: is_gcd_def)
    apply (blast intro: gcd_dvd1 gcd_dvd2 gcd_type intro: dvd_trans)
    done

    lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
    apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
           in gcd_assoc_raw)
    apply auto
    done

    lemma gcd_0_left [simp]: "gcd (0, m) = natify(m)"
    by (simp add: gcd_commute [of 0])

    lemma gcd_1_left [simp]: "gcd (1, m) = 1"
    by (simp add: gcd_commute [of 1])

    subsection{*Addition laws*}

    lemma gcd_add1 [simp]: "gcd (m #+ n, n) = gcd (m, n)"
    apply (subgoal_tac "gcd (m #+ natify (n), natify (n)) = gcd (m, natify (n))")
    apply simp
    apply (case_tac "natify (n) = 0")
    apply (auto simp add: Ord_0_lt_iff gcd_non_0)
    done

    lemma gcd_add2 [simp]: "gcd (m, m #+ n) = gcd (m, n)"
    apply (rule gcd_commute [THEN trans])
    apply (subst add_commute, simp)
    apply (rule gcd_commute)
    done

    lemma gcd_add2' [simp]: "gcd (m, n #+ m) = gcd (m, n)"
    by (subst add_commute, rule gcd_add2)

    lemma gcd_add_mult_raw: "k ∈ nat ==> gcd (m, k #* m #+ n) = gcd (m, n)"
    apply (erule nat_induct)
    apply (auto simp add: gcd_add2 add_assoc)
    done

    lemma gcd_add_mult: "gcd (m, k #* m #+ n) = gcd (m, n)"
    apply (cut_tac k = "natify (k)" in gcd_add_mult_raw)
    apply auto
    done

    subsection{* Multiplication Laws*}

    lemma gcd_mult_distrib2_raw:
         "[| k ∈ nat; m ∈ nat; n ∈ nat |]
          ==> k #* gcd (m, n) = gcd (k #* m, k #* n)"
    apply (erule_tac m = m and n = n in gcd_induct, assumption)
    apply simp
    apply (case_tac "k = 0", simp)
    apply (simp add: mod_geq gcd_non_0 mod_mult_distrib2 Ord_0_lt_iff)
    done

    lemma gcd_mult_distrib2: "k #* gcd (m, n) = gcd (k #* m, k #* n)"
    apply (cut_tac k = "natify (k)" and m = "natify (m)" and n = "natify (n) "
           in gcd_mult_distrib2_raw)
    apply auto
    done

    lemma gcd_mult [simp]: "gcd (k, k #* n) = natify(k)"
    by (cut_tac k = k and m = 1 and n = n in gcd_mult_distrib2, auto)

    lemma gcd_self [simp]: "gcd (k, k) = natify(k)"
    by (cut_tac k = k and n = 1 in gcd_mult, auto)

    lemma relprime_dvd_mult:
         "[| gcd (k,n) = 1;  k dvd (m #* n);  m ∈ nat |] ==> k dvd m"
    apply (cut_tac k = m and m = k and n = n in gcd_mult_distrib2, auto)
    apply (erule_tac b = m in ssubst)
    apply (simp add: dvd_imp_nat1)
    done

    lemma relprime_dvd_mult_iff:
         "[| gcd (k,n) = 1;  m ∈ nat |] ==> k dvd (m #* n) <-> k dvd m"
    by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)

    lemma prime_imp_relprime:
         "[| p ∈ prime;  ~ (p dvd n);  n ∈ nat |] ==> gcd (p, n) = 1"
    apply (simp add: prime_def, clarify)
    apply (drule_tac x = "gcd (p,n)" in bspec)
    apply auto
    apply (cut_tac m = p and n = n in gcd_dvd2, auto)
    done

    lemma prime_into_nat: "p ∈ prime ==> p ∈ nat"
    by (simp add: prime_def)

    lemma prime_nonzero: "p ∈ prime ==> p≠0"
    by (auto simp add: prime_def)

    text{*This theorem leads immediately to a proof of the uniqueness of
      factorization.  If @{term p} divides a product of primes then it is
      one of those primes.*}

    lemma prime_dvd_mult:
         "[|p dvd m #* n; p ∈ prime; m ∈ nat; n ∈ nat |] ==> p dvd m ∨ p dvd n"
    by (blast intro: relprime_dvd_mult prime_imp_relprime prime_into_nat)

    lemma gcd_mult_cancel_raw:
         "[|gcd (k,n) = 1; m ∈ nat; n ∈ nat|] ==> gcd (k #* m, n) = gcd (m, n)"
    apply (rule dvd_anti_sym)
     apply (rule gcd_greatest)
      apply (rule relprime_dvd_mult [of _ k])
    apply (simp add: gcd_assoc)
    apply (simp add: gcd_commute)
    apply (simp_all add: mult_commute)
    apply (blast intro: dvdI1 gcd_dvd1 dvd_trans)
    done

    lemma gcd_mult_cancel: "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)"
    apply (cut_tac m = "natify (m)" and n = "natify (n)" in gcd_mult_cancel_raw)
    apply auto
    done

    subsection{*The Square Root of a Prime is Irrational: Key Lemma*}

    lemma prime_dvd_other_side:
         "[|n#*n = p#*(k#*k); p ∈ prime; n ∈ nat|] ==> p dvd n"
    apply (subgoal_tac "p dvd n#*n")
     apply (blast dest: prime_dvd_mult)
    apply (rule_tac j = "k#*k" in dvd_mult_left)
     apply (auto simp add: prime_def)
    done

    lemma reduction:
         "[|k#*k = p#*(j#*j); p ∈ prime; 0 < k; j ∈ nat; k ∈ nat|]
          ==> k < p#*j & 0 < j"
    apply (rule ccontr)
    apply (simp add: not_lt_iff_le prime_into_nat)
    apply (erule disjE)
     apply (frule mult_le_mono, assumption+)
    apply (simp add: mult_ac)
    apply (auto dest!: natify_eqE
                simp add: not_lt_iff_le prime_into_nat mult_le_cancel_le1)
    apply (simp add: prime_def)
    apply (blast dest: lt_trans1)
    done

    lemma rearrange: "j #* (p#*j) = k#*k ==> k#*k = p#*(j#*j)"
    by (simp add: mult_ac)

    lemma prime_not_square:
         "[|m ∈ nat; p ∈ prime|] ==> ∀k ∈ nat. 0<k --> m#*m ≠ p#*(k#*k)"
    apply (erule complete_induct, clarify)
    apply (frule prime_dvd_other_side, assumption)
    apply assumption
    apply (erule dvdE)
    apply (simp add: mult_assoc mult_cancel1 prime_nonzero prime_into_nat)
    apply (blast dest: rearrange reduction ltD)
    done

    end

### The Divides Relation

lemma dvdD:

      m dvd n ==> m ∈ nat ∧ n ∈ nat ∧ (∃k∈nat. n = m #× k)

lemma dvdE:

      [| m dvd n; !!k. [| m ∈ nat; n ∈ nat; k ∈ nat; n = m #× k |] ==> P |] ==> P

lemmas dvd_imp_nat1:

      m dvd n ==> m ∈ nat

lemmas dvd_imp_nat1:

      m dvd n ==> m ∈ nat

lemmas dvd_imp_nat2:

      m dvd n ==> n ∈ nat

lemmas dvd_imp_nat2:

      m dvd n ==> n ∈ nat

lemma dvd_0_right:

      m ∈ nat ==> m dvd 0

lemma dvd_0_left:

      0 dvd m ==> m = 0

lemma dvd_refl:

      m ∈ nat ==> m dvd m

lemma dvd_trans:

      [| m dvd n; n dvd p |] ==> m dvd p

lemma dvd_anti_sym:

      [| m dvd n; n dvd m |] ==> m = n

lemma dvd_mult_left:

      [| i #× j dvd k; i ∈ nat |] ==> i dvd k

lemma dvd_mult_right:

      [| i #× j dvd k; j ∈ nat |] ==> j dvd k

### Euclid's Algorithm for the GCD

lemma gcd_0:

      gcd(m, 0) = natify(m)

lemma gcd_natify1:

      gcd(natify(m), n) = gcd(m, n)

lemma gcd_natify2:

      gcd(m, natify(n)) = gcd(m, n)

lemma gcd_non_0_raw:

      [| 0 < n; n ∈ nat |] ==> gcd(m, n) = gcd(n, m mod n)

lemma gcd_non_0:

      0 < natify(n) ==> gcd(m, n) = gcd(n, m mod n)

lemma gcd_1:

      gcd(m, 1) = 1

lemma dvd_add:

      [| k dvd a; k dvd b |] ==> k dvd a #+ b

lemma dvd_mult:

      k dvd n ==> k dvd m #× n

lemma dvd_mult2:

      k dvd m ==> k dvd m #× n

lemmas dvdI1:

      k ∈ nat ==> k dvd m #× k

lemmas dvdI1:

      k ∈ nat ==> k dvd m #× k

lemmas dvdI2:

      k ∈ nat ==> k dvd k #× n

lemmas dvdI2:

      k ∈ nat ==> k dvd k #× n

lemma dvd_mod_imp_dvd_raw:

      [| a ∈ nat; b ∈ nat; k dvd b; k dvd a mod b |] ==> k dvd a

lemma dvd_mod_imp_dvd:

      [| k dvd a mod b; k dvd b; a ∈ nat |] ==> k dvd a

lemma gcd_induct_lemma:

      [| n ∈ nat; ∀m∈nat. P(m, 0);
         ∀m∈nat. ∀n∈nat. 0 < n --> P(n, m mod n) --> P(m, n); m ∈ nat |]
      ==> P(m, n)

lemma gcd_induct:

      [| m ∈ nat; n ∈ nat; !!m. m ∈ nat ==> P(m, 0);
         !!m n. [| m ∈ nat; n ∈ nat; 0 < n; P(n, m mod n) |] ==> P(m, n) |]
      ==> P(m, n)

### Basic Properties of @{term gcd}

lemma gcd_type:

      gcd(m, n) ∈ nat

lemma gcd_dvd_both:

      [| m ∈ nat; n ∈ nat |] ==> gcd(m, n) dvd m ∧ gcd(m, n) dvd n

lemma gcd_dvd1:

      m ∈ nat ==> gcd(m, n) dvd m

lemma gcd_dvd2:

      n ∈ nat ==> gcd(m, n) dvd n

lemma dvd_mod:

      [| f dvd a; f dvd b |] ==> f dvd a mod b

lemma gcd_greatest_raw:

      [| m ∈ nat; n ∈ nat; f ∈ nat; f dvd m; f dvd n |] ==> f dvd gcd(m, n)

lemma gcd_greatest:

      [| f dvd m; f dvd n; f ∈ nat |] ==> f dvd gcd(m, n)

lemma gcd_greatest_iff:

      [| k ∈ nat; m ∈ nat; n ∈ nat |] ==> k dvd gcd(m, n) <-> k dvd m ∧ k dvd n

### The Greatest Common Divisor

lemma is_gcd:

      [| m ∈ nat; n ∈ nat |] ==> is_gcd(gcd(m, n), m, n)

lemma is_gcd_unique:

      [| is_gcd(m, a, b); is_gcd(n, a, b); m ∈ nat; n ∈ nat |] ==> m = n

lemma is_gcd_commute:

      is_gcd(k, m, n) <-> is_gcd(k, n, m)

lemma gcd_commute_raw:

      [| m ∈ nat; n ∈ nat |] ==> gcd(m, n) = gcd(n, m)

lemma gcd_commute:

      gcd(m, n) = gcd(n, m)

lemma gcd_assoc_raw:

      [| k ∈ nat; m ∈ nat; n ∈ nat |] ==> gcd(gcd(k, m), n) = gcd(k, gcd(m, n))

lemma gcd_assoc:

      gcd(gcd(k, m), n) = gcd(k, gcd(m, n))

lemma gcd_0_left:

      gcd(0, m) = natify(m)

lemma gcd_1_left:

      gcd(1, m) = 1

### Addition laws

lemma gcd_add1:

      gcd(m #+ n, n) = gcd(m, n)

lemma gcd_add2:

      gcd(m, m #+ n) = gcd(m, n)

lemma gcd_add2':

      gcd(m, n #+ m) = gcd(m, n)

lemma gcd_add_mult_raw:

      k ∈ nat ==> gcd(m, k #× m #+ n) = gcd(m, n)

lemma gcd_add_mult:

      gcd(m, k #× m #+ n) = gcd(m, n)

### Multiplication Laws

lemma gcd_mult_distrib2_raw:

      [| k ∈ nat; m ∈ nat; n ∈ nat |] ==> k #× gcd(m, n) = gcd(k #× m, k #× n)

lemma gcd_mult_distrib2:

      k #× gcd(m, n) = gcd(k #× m, k #× n)

lemma gcd_mult:

      gcd(k, k #× n) = natify(k)

lemma gcd_self:

      gcd(k, k) = natify(k)

lemma relprime_dvd_mult:

      [| gcd(k, n) = 1; k dvd m #× n; m ∈ nat |] ==> k dvd m

lemma relprime_dvd_mult_iff:

      [| gcd(k, n) = 1; m ∈ nat |] ==> k dvd m #× n <-> k dvd m

lemma prime_imp_relprime:

      [| p ∈ prime; ¬ p dvd n; n ∈ nat |] ==> gcd(p, n) = 1

lemma prime_into_nat:

      p ∈ prime ==> p ∈ nat

lemma prime_nonzero:

      p ∈ prime ==> p ≠ 0

lemma prime_dvd_mult:

      [| p dvd m #× n; p ∈ prime; m ∈ nat; n ∈ nat |] ==> p dvd m ∨ p dvd n

lemma gcd_mult_cancel_raw:

      [| gcd(k, n) = 1; m ∈ nat; n ∈ nat |] ==> gcd(k #× m, n) = gcd(m, n)

lemma gcd_mult_cancel:

      gcd(k, n) = 1 ==> gcd(k #× m, n) = gcd(m, n)

### The Square Root of a Prime is Irrational: Key Lemma

lemma prime_dvd_other_side:

      [| n #× n = p #× k #× k; p ∈ prime; n ∈ nat |] ==> p dvd n

lemma reduction:

      [| k #× k = p #× j #× j; p ∈ prime; 0 < k; j ∈ nat; k ∈ nat |]
      ==> k < p #× j ∧ 0 < j

lemma rearrange:

      j #× p #× j = k #× k ==> k #× k = p #× j #× j

lemma prime_not_square:

      [| m ∈ nat; p ∈ prime |] ==> ∀k∈nat. 0 < k --> m #× m ≠ p #× k #× k