let n be Nat; :: thesis: ( n is prime iff ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) )
thus ( n is prime implies ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) ) :: thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 implies n is prime )

proof

assume A1: n is prime ; :: thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 )

per cases ( n < 2 or n >= 2 ) ;

suppose n < 2 ; :: thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 )

then n < 1 + 1 ;
then n <= 1 by NAT_1:13;
hence ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) by A1, INT_2:def 4; :: thesis: verum

end;

suppose n >= 2 ; :: thesis: ( (((n -' 1) !) + 1) mod n = 0 & n > 1 )

then A2: n - 2 >= 2 - 2 by XREAL_1:9;
then A3: (n - 2) + 1 >= 0 + 1 by XREAL_1:6;
set l = n -' 2;
A4: 2 + (n -' 2) > 1 + (n -' 2) by XREAL_1:6;
set f = Sgm (Seg (n -' 2));
A5: (n * 1) mod n = 0 by NAT_D:13;
A6: n -' 2 = n - 2 by A2, XREAL_0:def 2;
then A7: (n -' 2) + 1 = n - 1
.= n -' 1 by A3, XREAL_0:def 2 ;
A8: for l9 being Nat st l9 in rng (Sgm (Seg (n -' 2))) & l9 <> 1 holds
ex k9 being Nat st
( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 )

proof

let l9 be Nat; :: thesis: ( l9 in rng (Sgm (Seg (n -' 2))) & l9 <> 1 implies ex k9 being Nat st
( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) )
assume l9 in rng (Sgm (Seg (n -' 2))) ; :: thesis: ( not l9 <> 1 or ex k9 being Nat st
( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) )
then A9: l9 in Seg (n -' 2) by FINSEQ_1:def 14;
assume l9 <> 1 ; :: thesis: ex k9 being Nat st
( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 )
then consider k9 being Nat such that
A10: ( k9 in Seg (n -' 2) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) by A1, A6, A9, Lm9;
take k9 ; :: thesis: ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 )
thus ( k9 in rng (Sgm (Seg (n -' 2))) & k9 <> 1 & k9 <> l9 & (l9 * k9) mod ((n -' 2) + 2) = 1 ) by A10, FINSEQ_1:def 14; :: thesis: verum

end;

( (n -' 2) ! = Product (Sgm (Seg (n -' 2))) & rng (Sgm (Seg (n -' 2))) c= Seg (n -' 2) ) by FINSEQ_1:def 14, FINSEQ_3:48;
then A11: ((n -' 2) !) mod ((n -' 2) + 2) = 1 by A1, A6, A8, Lm10, FINSEQ_3:92;
(((n -' 2) + 1) !) mod ((n -' 2) + 2) = (((n -' 2) + 1) * ((n -' 2) !)) mod ((n -' 2) + 2) by NEWTON:15
.= (((n -' 2) + 1) * 1) mod ((n -' 2) + 2) by A11, EULER_2:7
.= (n -' 2) + 1 by A4, NAT_D:24 ;
then (((((n -' 2) + 1) !) mod ((n -' 2) + 2)) + 1) mod ((n -' 2) + 2) = 0 by A6, A5;
hence ( (((n -' 1) !) + 1) mod n = 0 & n > 1 ) by A1, A6, A7, INT_2:def 4, NAT_D:22; :: thesis: verum

end;

end;

end;

thus ( (((n -' 1) !) + 1) mod n = 0 & n > 1 implies n is prime ) :: thesis: verum

proof

assume that
A12: (((n -' 1) !) + 1) mod n = 0 and
A13: n > 1 ; :: thesis: n is prime
n >= 1 + 1 by A13, NAT_1:13;
then consider k being Element of NAT such that
A14: k is prime and
A15: k divides n by INT_2:31;
consider i being Nat such that
A16: n = k * i by A15, NAT_D:def 3;
A17: k <> 1 by A14, INT_2:def 4;
(((n -' 1) !) + 1) mod n = (((n -' 1) !) + 1) mod k by A12, A13, A14, A16, PEPIN:9;
then k divides ((n -' 1) !) + 1 by A12, A14, PEPIN:6;
then k > n -' 1 by A14, A17, NEWTON:42;
then k > n - 1 by XREAL_0:def 2;
then k + 1 > (n - 1) + 1 by XREAL_1:6;
then k >= n by NAT_1:13;
then k / k >= (k * i) / k by A16, XREAL_1:72;
then 1 >= (k * i) / k by A14, XCMPLX_1:60;
then 1 >= i * (k / k) by XCMPLX_1:74;
then A18: 1 >= i * 1 by A14, XCMPLX_1:60;
assume A19: not n is prime ; :: thesis: contradiction
i <> 0 by A13, A16;
then i >= 0 + 1 by NAT_1:13;
then i = 1 by A18, XXREAL_0:1;
hence contradiction by A19, A14, A16; :: thesis: verum

end;