let p be Prime; :: thesis: for n being even Nat st n < p holds
((p - 1) choose n) mod p = 1
let n be even Nat; :: thesis: ( n < p implies ((p - 1) choose n) mod p = 1 )
assume A1: n < p ; :: thesis: ((p - 1) choose n) mod p = 1

per cases ( p is even or p is odd ) ;

suppose p is even ; :: thesis: ((p - 1) choose n) mod p = 1

then B1: p = 2 by LAGRA4SQ:13;
(2 * 0) + 1 is odd ;
then n = 0 by A1, B1, NAT_1:23;
then ((p - 1) choose n) mod p = 1 mod (1 + (p - 1)) by NEWTON:19;
hence ((p - 1) choose n) mod p = 1 ; :: thesis: verum

end;

suppose p is odd ; :: thesis: ((p - 1) choose n) mod p = 1

then reconsider p = p as odd Nat ;
reconsider m = n / 2 as Nat ;
(2 * m) + 1 <= p by A1, INT_1:7;

per cases then ( (2 * m) + 1 < p or (2 * m) + 1 = p ) by XXREAL_0:1;

suppose (2 * m) + 1 < p ; :: thesis: ((p - 1) choose n) mod p = 1

then 1 = ((p - 1) choose (((2 * m) + 1) - 1)) mod p by PCZ;
hence ((p - 1) choose n) mod p = 1 ; :: thesis: verum

end;

suppose (2 * m) + 1 = p ; :: thesis: ((p - 1) choose n) mod p = 1

then ((p - 1) choose n) mod p = 1 mod (1 + (p - 1)) by NEWTON:21;
hence ((p - 1) choose n) mod p = 1 ; :: thesis: verum

end;

end;

end;

end;