let p be odd Prime; :: thesis: for n being Nat st (2 * n) + 1 < p holds
( ((p - 1) choose (2 * n)) mod p = 1 & ((p - 1) choose ((2 * n) + 1)) mod p = p - 1 )
defpred S₁[ Nat] means ( (2 * $1) + 1 < p implies ( ((p - 1) choose (2 * $1)) mod p = 1 & ((p - 1) choose ((2 * $1) + 1)) mod p = p - 1 ) );
A1: S₁[ 0 ]

proof

B1: ((p - 1) choose (2 * 0)) mod p = 1 mod p by NEWTON:19;
((p - 1) choose ((2 * 0) + 1)) mod p = (p - 1) mod ((p - 1) + 1) ;
hence S₁[ 0 ] by B1; :: thesis: verum

end;

A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume B1: ( (2 * m) + 1 < p implies ( ((p - 1) choose (2 * m)) mod p = 1 & ((p - 1) choose ((2 * m) + 1)) mod p = p - 1 ) ) ; :: thesis: S₁[m + 1]
( (2 * (m + 1)) + 1 < p implies ( ((p - 1) choose (2 * (m + 1))) mod p = 1 & ((p - 1) choose ((2 * (m + 1)) + 1)) mod p = p - 1 ) )

proof

assume C1: (2 * (m + 1)) + 1 < p ; :: thesis: ( ((p - 1) choose (2 * (m + 1))) mod p = 1 & ((p - 1) choose ((2 * (m + 1)) + 1)) mod p = p - 1 )
C3: ((2 * m) + 1) + 0 < ((2 * m) + 1) + 2 by XREAL_1:6;
((p - 1) + 1) choose (((2 * m) + 1) + 1) = ((p - 1) choose (((2 * m) + 1) + 1)) + ((p - 1) choose ((2 * m) + 1)) by NEWTON:22;
then C4: ((p - 1) choose ((2 * m) + 2)) mod p = ((p choose ((2 * m) + 2)) - ((p - 1) choose ((2 * m) + 1))) mod p
.= (((p choose ((2 * m) + 2)) mod p) - (((p - 1) choose ((2 * m) + 1)) mod p)) mod p by INT_6:7
.= (0 - (p - 1)) mod p by PCK, B1, C1, XXREAL_0:2, C3
.= (1 - p) mod p
.= ((1 mod p) - (p mod p)) mod p by INT_6:7
.= 1 mod (1 + (p - 1))
.= 1 ;
((p - 1) + 1) choose (((2 * m) + 2) + 1) = ((p - 1) choose (((2 * m) + 2) + 1)) + ((p - 1) choose ((2 * m) + 2)) by NEWTON:22;
then ((p - 1) choose (((2 * m) + 2) + 1)) mod p = ((((p - 1) + 1) choose (((2 * m) + 2) + 1)) - ((p - 1) choose ((2 * m) + 2))) mod p
.= (((p choose ((2 * (m + 1)) + 1)) mod p) - (((p - 1) choose (2 * (m + 1))) mod p)) mod p by INT_6:7
.= (0 - 1) mod p by C1, C4, PCK
.= ((- 1) + (1 * p)) mod ((p - 1) + 1) by NAT_D:61
.= p - 1 ;
hence ( ((p - 1) choose (2 * (m + 1))) mod p = 1 & ((p - 1) choose ((2 * (m + 1)) + 1)) mod p = p - 1 ) by C4; :: thesis: verum

end;

hence S₁[m + 1] ; :: thesis: verum

end;

for c being Nat holds S₁[c] from NAT_1:sch 2(A1, A2);
hence for n being Nat st (2 * n) + 1 < p holds
( ((p - 1) choose (2 * n)) mod p = 1 & ((p - 1) choose ((2 * n) + 1)) mod p = p - 1 ) ; :: thesis: verum