let n be 2 _greater Nat; for s being non trivial Divisor of n - 1 st s > sqrt n & ex a being Nat st
( a |^ (n - 1),1 are_congruent_mod n & ( for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1 ) ) holds
n is prime
let s be non trivial Divisor of n - 1; ( s > sqrt n & ex a being Nat st
( a |^ (n - 1),1 are_congruent_mod n & ( for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1 ) ) implies n is prime )
assume A1:
( s > sqrt n & ex a being Nat st
( a |^ (n - 1),1 are_congruent_mod n & ( for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1 ) ) )
; n is prime
reconsider m = n as Element of NAT by ORDINAL1:def 12;
reconsider f = s as Element of NAT by ORDINAL1:def 12;
m > 1 + 1
by Def1;
then A2:
m >= 1
by NAT_1:13;
consider c being Integer such that
A3:
m - 1 = f * c
by Def2, INT_1:def 3;
A4:
sqrt n >= 0
by SQUARE_1:def 2;
c > 0
by A3;
then reconsider c = c as Element of NAT by INT_1:3;
A6:
( m - 1 = f * c & f > c & c > 0 )
by A3, A5;
now for p being Element of NAT st p divides f & p is prime holds
ex a being Element of NAT st
( (a |^ (m -' 1)) mod m = 1 & ((a |^ ((m -' 1) div p)) -' 1) gcd m = 1 )let p be
Element of
NAT ;
( p divides f & p is prime implies ex a being Element of NAT st
( (a |^ (m -' 1)) mod m = 1 & ((a |^ ((m -' 1) div p)) -' 1) gcd m = 1 ) )assume A7:
(
p divides f &
p is
prime )
;
ex a being Element of NAT st
( (a |^ (m -' 1)) mod m = 1 & ((a |^ ((m -' 1) div p)) -' 1) gcd m = 1 )reconsider q =
p as
Nat ;
reconsider q =
q as
Divisor of
s by A7, Def2;
reconsider q =
q as
prime Divisor of
s by A7;
consider b being
Nat such that A8:
(
b |^ (n - 1),1
are_congruent_mod n & ( for
q being
prime Divisor of
s holds
((b |^ ((n - 1) / q)) - 1) gcd n = 1 ) )
by A1;
reconsider a =
b as
Element of
NAT by ORDINAL1:def 12;
consider k1 being
Integer such that A9:
q * k1 = s
by Def2, INT_1:def 3;
consider k2 being
Integer such that A10:
s * k2 = n - 1
by Def2, INT_1:def 3;
consider l1 being
Integer such that A11:
p * l1 = f
by A7;
A12:
k2 = c
by A3, A10, XCMPLX_1:5;
A13:
(m - 1) / p =
((p * l1) * c) * (p ")
by A3, A11, XCMPLX_0:def 9
.=
(l1 * c) * (p * (p "))
.=
(l1 * c) * 1
by A7, XCMPLX_0:def 7
;
A14:
n - 1
>= 2
- 1
by Def1, XREAL_1:9;
then
(a |^ ((m -' 1) div p)) + 1
> 0 + 1
by XREAL_1:6;
then A15:
a |^ ((m -' 1) div p) >= 1
by NAT_1:13;
(n - 1) / q =
((q * k1) * k2) * (q ")
by A9, A10, XCMPLX_0:def 9
.=
(k1 * k2) * (q * (q "))
.=
(k1 * k2) * 1
by XCMPLX_0:def 7
.=
(m - 1) / p
by A9, A11, A12, A13, XCMPLX_1:5
.=
[/((m - 1) / p)\]
by A13
.=
[\((m - 1) / p)/]
by A13
.=
(m -' 1) div p
by A2, XREAL_1:233
;
then
(a |^ ((m -' 1) div p)) -' 1
= (b |^ ((n - 1) / q)) - 1
by A15, XREAL_1:233;
then A16:
((a |^ ((m -' 1) div p)) -' 1) gcd m = 1
by A8;
consider x being
Integer such that A17:
n * x = (a |^ (n - 1)) - 1
by A8;
A18:
(a |^ (n - 1)) / n =
((n * x) + 1) * (n ")
by A17, XCMPLX_0:def 9
.=
(((n ") * n) * x) + (1 * (n "))
.=
(1 * x) + (n ")
by XCMPLX_0:def 7
;
A19:
x <= (a |^ (n - 1)) / n
by A18, XREAL_1:29;
A20:
((a |^ (n - 1)) / n) - 1
= x + ((n ") - 1)
by A18;
2
< n
by Def1;
then
2
- 1
< n - 0
by XREAL_1:15;
then
n " < 1
"
by XREAL_1:88;
then
(n ") - 1
< 0
by XREAL_1:49;
then
((a |^ (n - 1)) / n) - 1
< x
by A20, XREAL_1:30;
then
(a |^ (n - 1)) div n = x
by A19, INT_1:def 6;
then A21:
(a |^ (n - 1)) mod n =
(a |^ (n - 1)) - (n * x)
by INT_1:def 10
.=
1
by A17
;
(a |^ (m -' 1)) mod m = 1
by A21, A2, XREAL_1:233;
hence
ex
a being
Element of
NAT st
(
(a |^ (m -' 1)) mod m = 1 &
((a |^ ((m -' 1) div p)) -' 1) gcd m = 1 )
by A16;
verum end;
hence
n is prime
by A6, NAT_4:24; verum