let n, f, c be Element of NAT ; :: thesis: ( n - 1 = f * c & f > c & c > 0 & ( 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 that
A1: n - 1 = f * c and
A2: f > c and
A3: c > 0 ; :: 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 )
A4: (n - 1) + 1 > 0 + 1 by A1, A2, A3, XREAL_1:6;
assume A5: 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 not n is prime ; :: thesis: contradiction
then consider p being Element of NAT such that
A6: p divides n and
A7: 1 < p and
A8: p * p <= n and
A9: p is prime by A4, Lm1;
A10: p - 1 = p -' 1 by A7, XREAL_1:233;
A11: p - 1 > 1 - 1 by A7, XREAL_1:9;
then A12: p -' 1 > 0 by A7, XREAL_1:233;
A13: 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 )
set n1 = q1 |-count f;
assume A14: q1 in support (pfexp f) ; :: thesis: ( not q1 |-count f > 0 or p mod (q1 |^ (q1 |-count f)) = 1 )
then A15: q1 is prime by NAT_3:34;
A16: q1 is prime by A14, NAT_3:34;
then consider a being Element of NAT such that
A17: (a |^ (n -' 1)) mod n = 1 and
A18: ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 by A5, A14, NAT_3:36;
assume A19: q1 |-count f > 0 ; :: thesis: p mod (q1 |^ (q1 |-count f)) = 1
A20: not p divides (a |^ ((n -' 1) div q1)) -' 1 by A6, NEWTON:50, A7, A18, NAT_D:7;
q1 <> 1 by A16, INT_2:def 4;
then q1 |^ (q1 |-count f) divides f by A2, NAT_3:def 7;
then consider d being Nat such that
A21: f = (q1 |^ (q1 |-count f)) * d by NAT_D:def 3;
reconsider d = d as Element of NAT by ORDINAL1:def 12;
set k = d * c;
A22: d * c > 0
proof
assume d * c <= 0 ; :: thesis: contradiction
then d = 0 by A3;
hence contradiction by A2, A21; :: thesis: verum
end;
n - 1 = (d * c) * (q1 |^ (q1 |-count f)) by A1, A21;
hence p mod (q1 |^ (q1 |-count f)) = 1 by A6, A9, A19, A17, A22, A15, A20, Th23; :: thesis: verum
end;
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 A23: 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 A2, A12, Th20;
then f divides p -' 1 by NAT_D:def 3;
then f <= p -' 1 by A12, NAT_D:7;
then (p - 1) + 1 >= f + 1 by A10, XREAL_1:6;
then p > f by NAT_1:13;
then A26: p ^2 > f ^2 by SQUARE_1:16;
c >= 0 + 1 by A3, NAT_1:13;
then A27: c + 1 >= 1 + 1 by XREAL_1:6;
f >= c + 1 by A2, NAT_1:13;
then f >= 2 by A27, XXREAL_0:2;
then f - 1 >= 2 - 1 by XREAL_1:9;
then A28: n + (f - 1) >= n + 1 by XREAL_1:6;
f >= c + 1 by A2, NAT_1:13;
then f * f >= f * (c + 1) by XREAL_1:64;
then p ^2 > f + (n - 1) by A1, A26, XXREAL_0:2;
then p ^2 >= n + 1 by A28, XXREAL_0:2;
hence contradiction by A8, NAT_1:13; :: thesis: verum