let n be natural odd number ; :: thesis: ( n > 1 implies ( n + 2 is prime iff not n + 2 divides (n -' 1) ! ) )
assume A1: n > 1 ; :: thesis: ( n + 2 is prime iff not n + 2 divides (n -' 1) ! )
A2: n -' 1 = n - 1 by A1, XREAL_1:233;
thus ( n + 2 is prime implies not n + 2 divides (n -' 1) ! ) :: thesis: ( not n + 2 divides (n -' 1) ! implies n + 2 is prime )

proof

assume A3: n + 2 is prime ; :: thesis: not n + 2 divides (n -' 1) !
A4: (n -' 1) + 1 = (n - 1) + 1 ;
n <= n + 2 by NAT_1:11;
hence not n + 2 divides (n -' 1) ! by A3, A4, NAT_1:13, NAT_4:19; :: thesis: verum

end;

assume A5: not n + 2 divides (n -' 1) ! ; :: thesis: n + 2 is prime
consider k being Nat such that
A6: n = (2 * k) + 1 by ABIAN:9;
k <> 0 by A1, A6;
then ( k = 1 or k >= 2 ) by NAT_1:23;

per cases then ( k = 1 or k = 2 or k > 2 ) by XXREAL_0:1;

suppose ( k = 1 or k = 2 ) ; :: thesis: n + 2 is prime

hence n + 2 is prime by A6, XPRIMES1:5, XPRIMES1:7; :: thesis: verum

end;

suppose k > 2 ; :: thesis: n + 2 is prime

then k >= 2 + 1 by NAT_1:13;
then k * 2 >= 3 * 2 by XREAL_1:64;
then A7: n >= 6 + 1 by A6, XREAL_1:6;
then A8: ( n > 1 & n + 2 >= 7 + 2 ) by XREAL_1:6, XXREAL_0:2;
assume not n + 2 is prime ; :: thesis: contradiction
then consider a being Nat such that
A9: ( a divides n + 2 & a <> 1 & a <> n + 2 ) by A8, XXREAL_0:2;
consider b being Nat such that
A10: n + 2 = a * b by A9, NAT_D:def 3;
A11: ( a <> 0 & b <> 0 ) by A10;
A12: b <> 1 by A10, A9;
( 1 <= a & 1 <= b ) by A11, NAT_1:14;
then ( 1 < a & 1 < b & 2 is even ) by A12, A9, XXREAL_0:1;
then ( 1 + 1 <= a & 1 + 1 <= b & a <> 2 & b <> 2 ) by A10, NAT_1:13;
then ( 2 < a & 2 < b ) by XXREAL_0:1;
then ( 2 + 1 <= a & 2 + 1 <= b ) by NAT_1:13;
then ( 3 * b <= n + 2 & 3 * a <= n + 2 ) by A10, XREAL_1:64;
then A13: ( a <= (n + 2) / 3 & b <= (n + 2) / 3 ) by XREAL_1:77;
7 + ((2 * n) - 3) <= n + ((2 * n) - 3) by A7, XREAL_1:6;
then (n + 2) * 2 <= (n - 1) * 3 ;
then (n + 2) / 3 <= (n - 1) / 2 by XREAL_1:102;
then ( a <= (n - 1) / 2 & b <= (n - 1) / 2 ) by A13, XXREAL_0:2;
then A14: ( 2 * a <= n - 1 & 2 * b <= n - 1 ) by XREAL_1:83;

per cases ( 2 * a < 2 * b or 2 * b < 2 * a or 2 * a = 2 * b ) by XXREAL_0:1;

suppose ( 2 * a < 2 * b or 2 * b < 2 * a ) ; :: thesis: contradiction

then A15: (2 * a) * (2 * b) divides (n -' 1) ! by A2, A11, A14, NUMBER16:37;
a * b divides (a * b) * 4 ;
hence contradiction by A10, A5, A15, INT_2:9; :: thesis: verum

end;

suppose 2 * a = 2 * b ; :: thesis: contradiction

then 1 * a < 2 * b by A11, XREAL_1:68;
then A16: a * (2 * b) divides (n -' 1) ! by A2, A11, A14, NUMBER16:37;
a * b divides (a * b) * 2 ;
hence contradiction by A10, A5, A16, INT_2:9; :: thesis: verum

end;

end;

end;

end;