let p be odd Prime; :: thesis: p divides (p + 1) choose ((p + 1) / 2)
reconsider k = (p - 1) / 2 as Nat ;
p + p > p + 1 by XREAL_1:6, INT_2:def 4;
then (2 * p) / 2 > (p + 1) / 2 by XREAL_1:74;
then p divides p choose ((p + 1) / 2) by NEWTON02:119;
then A1: p divides ((2 * k) + 1) choose k by NP0;
((2 * k) + 1) choose k divides 2 * (((2 * k) + 1) choose k) ;
then p divides 2 * (((2 * k) + 1) choose k) by A1, INT_2:9;
then p divides (2 * (k + 1)) choose (k + 1) by NP1;
hence p divides (p + 1) choose ((p + 1) / 2) ; :: thesis: verum