let p be odd Prime; :: thesis: for k being non zero Nat st k + 1 < p holds
p divides (p + 1) choose (k + 1)
let k be non zero Nat; :: thesis: ( k + 1 < p implies p divides (p + 1) choose (k + 1) )
assume A1: k + 1 < p ; :: thesis: p divides (p + 1) choose (k + 1)
( 0 < k + 0 & k + 0 < k + 1 & k + 1 < p ) by A1, XREAL_1:6;
then ( p divides p choose k & p divides p choose (k + 1) ) by NEWTON02:119;
then p divides (p choose k) + (p choose (k + 1)) by WSIERP_1:4;
hence p divides (p + 1) choose (k + 1) by NEWTON:22; :: thesis: verum