let n, f, c be Element of NAT ; :: thesis: ( n - 1 = f * c & f > c & c > 0 & f gcd c = 1 & ( for q being Element of NAT st q divides f & q is prime holds
ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 ) ) implies n is prime )
assume A1: ( n - 1 = f * c & f > c & c > 0 & f gcd c = 1 ) ; :: thesis: ( ex q being Element of NAT st
( q divides f & q is prime & ( for a being Element of NAT holds
( not (a |^ (n -' 1)) mod n = 1 or not ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 ) ) ) or n is prime )
assume A2: for q being Element of NAT st q divides f & q is prime holds
ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 ) ; :: thesis: n is prime
assume A3: not n is prime ; :: thesis: contradiction
(n - 1) + 1 > 0 + 1 by A1, XREAL_1:8;
then consider p being Element of NAT such that
A4: ( p divides n & 1 < p & p * p <= n & p is prime ) by A3, Lm1;
A5: for q1 being Element of NAT st q1 in support (pfexp f) & q1 |-count f > 0 holds
p mod (q1 |^ (q1 |-count f)) = 1
proof
let q1 be Element of NAT ; :: thesis: ( q1 in support (pfexp f) & q1 |-count f > 0 implies p mod (q1 |^ (q1 |-count f)) = 1 )
assume A6: q1 in support (pfexp f) ; :: thesis: ( not q1 |-count f > 0 or p mod (q1 |^ (q1 |-count f)) = 1 )
assume A7: q1 |-count f > 0 ; :: thesis: p mod (q1 |^ (q1 |-count f)) = 1
A8: ( q1 is prime & q1 divides f ) by A6, NAT_3:34, NAT_3:36;
then consider a being Element of NAT such that
A9: ( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 ) by A2;
q1 <> 1 by A8, INT_2:def 5;
then A10: q1 |^ (q1 |-count f) divides f by A1, NAT_3:def 7;
set n1 = q1 |-count f;
consider d being Nat such that
A11: f = (q1 |^ (q1 |-count f)) * d by A10, NAT_D:def 3;
reconsider d = d as Element of NAT by ORDINAL1:def 13;
set k = d * c;
A12: n - 1 = (d * c) * (q1 |^ (q1 |-count f)) by A1, A11;
A13: d * c > 0
proof
assume d * c <= 0 ; :: thesis: contradiction
then d = 0 by A1;
hence contradiction by A1, A11; :: thesis: verum
end;
A14: q1 is prime by A6, NAT_3:34;
not p divides (a |^ ((n -' 1) div q1)) -' 1
proof
assume p divides (a |^ ((n -' 1) div q1)) -' 1 ; :: thesis: contradiction
then p divides n gcd ((a |^ ((n -' 1) div q1)) -' 1) by A4, NEWTON:63;
hence contradiction by A4, A9, NAT_D:7; :: thesis: verum
end;
hence p mod (q1 |^ (q1 |-count f)) = 1 by A4, A7, A9, A12, A13, A14, Th23; :: thesis: verum
end;
A15: p - 1 > 1 - 1 by A4, XREAL_1:11;
then A16: p -' 1 > 0 by A4, XREAL_1:235;
A17: p - 1 = p -' 1 by A4, XREAL_1:235;
for q1 being Element of NAT st q1 is prime holds
q1 |-count f <= q1 |-count (p -' 1)
proof
let q1 be Element of NAT ; :: thesis: ( q1 is prime implies q1 |-count f <= q1 |-count (p -' 1) )
assume A18: q1 is prime ; :: thesis: q1 |-count f <= q1 |-count (p -' 1)
per cases ( q1 in support (pfexp f) or not q1 in support (pfexp f) ) ;
end;
end;
then ex n2 being Element of NAT st p -' 1 = f * n2 by A1, A16, Th20;
then f divides p -' 1 by NAT_D:def 3;
then f <= p -' 1 by A16, NAT_D:7;
then (p - 1) + 1 >= f + 1 by A17, XREAL_1:8;
then p > f by NAT_1:13;
then B23: p ^2 > f ^2 by SQUARE_1:78;
f >= c + 1 by A1, NAT_1:13;
then f * f >= f * (c + 1) by XREAL_1:66;
then A24: p ^2 > f + (n - 1) by A1, B23, XXREAL_0:2;
A25: f >= c + 1 by A1, NAT_1:13;
c >= 0 + 1 by A1, NAT_1:13;
then c + 1 >= 1 + 1 by XREAL_1:8;
then f >= 2 by A25, XXREAL_0:2;
then f - 1 >= 2 - 1 by XREAL_1:11;
then n + (f - 1) >= n + 1 by XREAL_1:8;
then p ^2 >= n + 1 by A24, XXREAL_0:2;
hence contradiction by A4, NAT_1:13; :: thesis: verum