(*  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