let n be natural odd number ; :: thesis: ( n > 1 implies ( n is prime iff not n divides (n -' 1) ! ) )
assume A1: n > 1 ; :: thesis: ( n is prime iff not n divides (n -' 1) ! )
A2: (n -' 1) + 1 = (n - 1) + 1 ;
thus ( n is prime implies not n divides (n -' 1) ! ) :: thesis: ( not n divides (n -' 1) ! implies n is prime )
proof
assume A3: n is prime ; :: thesis: not n divides (n -' 1) !
(n -' 1) + 1 = (n - 1) + 1 ;
then n -' 1 < n by NAT_1:13;
hence not n divides (n -' 1) ! by A3, NAT_4:19; :: thesis: verum
end;
assume A4: not n divides (n -' 1) ! ; :: thesis: n is prime
consider k being Nat such that
A5: n = (2 * k) + 1 by ABIAN:9;
k <> 0 by A1, A5;
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 is prime
hence n is prime by A5, XPRIMES1:3, XPRIMES1:5; :: thesis: verum
end;
suppose k > 2 ; :: thesis: n is prime
then k >= 2 + 1 by NAT_1:13;
then k * 2 >= 3 * 2 by XREAL_1:64;
then A6: n >= 6 + 1 by A5, XREAL_1:6;
assume not n is prime ; :: thesis: contradiction
then consider a being Nat such that
A7: ( a divides n & a <> 1 & a <> n ) by A6, XXREAL_0:2;
consider b being Nat such that
A8: n = a * b by A7, NAT_D:def 3;
A9: ( a <> 0 & b <> 0 ) by A8;
then A10: ( a <= n & b <= n ) by A8, NAT_1:24;
b <> n
proof
assume b = n ; :: thesis: contradiction
then n * 1 = n * a by A8;
hence contradiction by A7, XCMPLX_1:5; :: thesis: verum
end;
then A11: ( a < n & b < n ) by A10, A7, XXREAL_0:1;
per cases ( a <> b or a = b ) ;
suppose a <> b ; :: thesis: contradiction
then A12: ( a < b or b < a ) by XXREAL_0:1;
( a <= n -' 1 & b <= n -' 1 ) by A11, A2, NAT_1:13;
hence contradiction by A4, A8, A12, A9, NUMBER16:37; :: thesis: verum
end;
end;
end;
end;