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 )

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

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

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

end;

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;then n <= 1 by NAT_1:13;

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

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 )

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;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

( (n -' 2) ! = Product (Sgm (Seg (n -' 2))) & rng (Sgm (Seg (n -' 2))) c= Seg (n -' 2) )
by FINSEQ_1:def 13, FINSEQ_3:48;
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 13;

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 13; :: thesis: verum

end;( 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 13;

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 13; :: thesis: verum

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

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;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