theory Pr+
−
imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"+
−
begin+
−
+
−
lemma +
−
  fixes a b::nat+
−
  shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"+
−
apply(simp add: power2_sum)+
−
done+
−
+
−
lemma+
−
  fixes a b c::"real"+
−
  assumes eq: "a * c \<le> b * c" and ineq: "b < a"+
−
  shows "c \<le> 0"+
−
proof -+
−
  {+
−
    assume  "0 < c" +
−
    then have "b * c < a * c" using ineq by(auto)+
−
    then have "False" using eq by auto+
−
  } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) +
−
qed+
−
    +
−
+
−
+
−
+
−
lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"+
−
by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))+
−
+
−
+
−
+
−
lemma +
−
 fixes n::"nat"+
−
 assumes a: "n > 1"+
−
    and  b: "\<not>(prime n)"+
−
 shows "\<not>(prime ((2 ^ n) - 1))"   +
−
using a b+
−
apply(induct n)+
−
apply(simp)+
−
apply(simp)+
−
+
−
+
−
+
−
end+
−