Theory Productdivides

(*  Title:      RSAPSS/Productdivides.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - Technische Universität Darmstadt 
*)

section "Lemmata for modular arithmetic with primes"

theory Productdivides
imports Pdifference
begin

lemma productdivides: "x mod a = (0::nat); x mod b = 0; prime a; prime b; a  b  x mod (a*b) = 0"
  by (simp add: mod_eq_0_iff_dvd primes_coprime divides_mult)

lemma specializedtoprimes1: 
  fixes p::nat 
  shows "prime p; prime q; p  q; a mod p = b mod p ; a mod q = b mod q
          a mod (p*q) = b mod (p*q)"
by (metis equalmodstrick1 equalmodstrick2 productdivides) 

lemma specializedtoprimes1a:
  fixes p::nat 
  shows "prime p; prime q; p  q; a mod p = b mod p; a mod q = b mod q; b < p*q 
     a mod (p*q) = b"
  by (simp add: specializedtoprimes1)
  
end