let n be natural number ; :: 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 A2:
n - 2
>= 2
- 2
by XREAL_1:11;
A3:
(n - 2) + 1
>= 0 + 1
by A2, XREAL_1:8;
set l =
n -' 2;
A4:
n -' 2
= n - 2
by A2, XREAL_0:def 2;
A5:
(n -' 2) + 1 =
n - 1
by A4
.=
n -' 1
by A3, XREAL_0:def 2
;
A6:
2
+ (n -' 2) > 1
+ (n -' 2)
by XREAL_1:8;
A7:
(n -' 2) ! = Product (Sgm (Seg (n -' 2)))
by FINSEQ_3:54;
set f =
Sgm (Seg (n -' 2));
A8:
rng (Sgm (Seg (n -' 2))) c= Seg (n -' 2)
by FINSEQ_1:def 13;
A9:
for
l' being
natural number st
l' in rng (Sgm (Seg (n -' 2))) &
l' <> 1 holds
ex
k' being
natural number st
(
k' in rng (Sgm (Seg (n -' 2))) &
k' <> 1 &
k' <> l' &
(l' * k') mod ((n -' 2) + 2) = 1 )
A13:
((n -' 2) ! ) mod ((n -' 2) + 2) = 1
by A4, A1, A7, A8, FINSEQ_3:99, A9, Lm10;
A14:
(((n -' 2) + 1) ! ) mod ((n -' 2) + 2) =
(((n -' 2) + 1) * ((n -' 2) ! )) mod ((n -' 2) + 2)
by NEWTON:21
.=
(((n -' 2) + 1) * 1) mod ((n -' 2) + 2)
by A13, EULER_2:9
.=
(n -' 2) + 1
by A6, NAT_D:24
;
(n * 1) mod n = 0
by NAT_D:13;
then
(((((n -' 2) + 1) ! ) mod ((n -' 2) + 2)) + 1) mod ((n -' 2) + 2) = 0
by A4, A14;
hence
(
(((n -' 1) ! ) + 1) mod n = 0 &
n > 1 )
by A4, A5, NAT_D:22, A1, INT_2:def 5;
:: thesis: verum end;
end;
thus
( (((n -' 1) ! ) + 1) mod n = 0 & n > 1 implies n is prime )
:: thesis: verumproof
assume A15:
(
(((n -' 1) ! ) + 1) mod n = 0 &
n > 1 )
;
:: thesis: n is prime
assume A16:
not
n is
prime
;
:: thesis: contradiction
n >= 1
+ 1
by A15, NAT_1:13;
then consider k being
Element of
NAT such that A17:
(
k is
prime &
k divides n )
by INT_2:48;
consider i being
Nat such that A18:
n = k * i
by A17, NAT_D:def 3;
(((n -' 1) ! ) + 1) mod n = (((n -' 1) ! ) + 1) mod k
by A15, A17, A18, PEPIN:9;
then A19:
k divides ((n -' 1) ! ) + 1
by A15, A17, PEPIN:6;
(
k <> 1 &
k <> 0 )
by A17, INT_2:def 5;
then A20:
k > n -' 1
by A19, NEWTON:55;
k > n - 1
by A20, XREAL_0:def 2;
then
k + 1
> (n - 1) + 1
by XREAL_1:8;
then
k >= n
by NAT_1:13;
then
k / k >= (k * i) / k
by A18, XREAL_1:74;
then
1
>= (k * i) / k
by A17, XCMPLX_1:60;
then
1
>= i * (k / k)
by XCMPLX_1:75;
then A21:
1
>= i * 1
by A17, XCMPLX_1:60;
i <> 0
by A15, A18;
then
i >= 0 + 1
by NAT_1:13;
then
i = 1
by A21, XXREAL_0:1;
hence
contradiction
by A16, A17, A18;
:: thesis: verum
end;