Theory PerfectBasics

section‹Basics needed›

theory PerfectBasics
imports Main "HOL-Computational_Algebra.Primes" "HOL-Algebra.Exponent"
begin

lemma exp_is_max_div:
   assumes m0: "m ≠ 0" and p: "prime p"
   shows "~ p dvd (m div (p^(multiplicity p m)))"
proof (rule ccontr)
  assume "~ ~ p dvd (m div (p^(multiplicity p m)))"
  hence a:"p dvd (m div (p^(multiplicity p m)))" by auto
  from m0 have "p^(multiplicity p m) dvd m" by (auto simp add: multiplicity_dvd)
  with a have "p^Suc (multiplicity p m) dvd m"
    by (subst (asm) dvd_div_iff_mult) auto
  with m0 p show False
    by (subst (asm) power_dvd_iff_le_multiplicity) auto
qed

lemma coprime_multiplicity:
  assumes "prime (p::nat)" and "m > 0"
  shows "coprime p (m div (p ^ multiplicity p m))"
proof (rule ccontr)
  assume "¬ coprime p (m div p ^ multiplicity p m)"
  with ‹prime p› have "∃q. prime q ∧ q dvd p ∧ q dvd m div p ^ multiplicity p m"
    by (metis dvd_refl prime_imp_coprime)
  with ‹prime p› have "∃q. q = p ∧ q dvd m div p ^ multiplicity p m"
    by (metis not_prime_1 prime_nat_iff)
  then have "p dvd m div p ^ multiplicity p m"
    by auto
  with assms show False
    by (auto simp add: exp_is_max_div)
qed

theorem simplify_sum_of_powers: "(x - 1::nat) * (∑i=0 .. n . x^i)  = x^(n + 1) - 1" (is "?l = ?r")
proof (cases)
  assume "n = 0"
  thus "?l = x^(n+1) - 1" by auto
next
  assume "n≠0"
  hence n0: "n>0" by auto 
  have "?l  = (x::nat)*(∑i=0 .. n . x^i) - (∑i=0 .. n . x^i)"
    by (metis diff_mult_distrib nat_mult_1)
  also have "... = (∑i=0 .. n . x^(Suc i))    - (∑i=0 .. n . x^i)"
    by (simp add: sum_distrib_left)
  also have "... = (∑i=Suc 0 .. Suc n . x^i)  - (∑i=0 .. n . x^i)"
    by (metis sum.shift_bounds_cl_Suc_ivl)
  also have "... = ((∑i=Suc 0 .. n. x^i)+x^(Suc n)) - (x^0 + (∑i=Suc 0 .. n. x^i))"
    by (simp add: sum.union_disjoint diff_add_inverse sum.atLeast_Suc_atMost)
  finally show "?thesis" by auto
qed

end