Quellcodebibliothek fermats_little_theorem.pvs

fermats_little_theorem: THEORY
%------------------------------------------------------------------------------
%   Fermat's Little Theorem
%
%   Anthony Narkawicz
%   December 2012
%------------------------------------------------------------------------------
BEGIN

    IMPORTING ints@mod_lems, ints@primes, eq_mod,
              reals@factorial, reals@binomial_identities,
       reals@polynomials

    n,m,p,l: VAR nat
    a,b: VAR nat
    k: VAR int
    np: VAR posnat

    prime_divides_choose: LEMMA
      prime?(p) AND np < p IMPLIES
      divides(p,C(p,np))


    Fermats_Little: THEOREM prime?(p) AND a<p %just for nats
                            IMPLIES 
                               eq_mod(p)(a^p,a)

    fermats_little_theorem: THEOREM prime?(p) %just for nats
                            IMPLIES 
                               eq_mod(p)(k^p,k)


END fermats_little_theorem