let p be Prime; :: thesis: for n being Nat st n + 2 < p holds
((p + 1) choose (n + 2)) mod p = 0
let n be Nat; :: thesis: ( n + 2 < p implies ((p + 1) choose (n + 2)) mod p = 0 )
assume A1: n + 2 < p ; :: thesis: ((p + 1) choose (n + 2)) mod p = 0
(n + 1) + 1 < p by A1;
hence ((p + 1) choose (n + 2)) mod p = 0 by PC0; :: thesis: verum