let n, f, d, n1, a, q be Element of NAT ; :: thesis: ( n - 1 = (q |^ n1) * d & q |^ n1 > d & d > 0 & q is prime & (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 implies n is prime )
assume that
A1: ( n - 1 = (q |^ n1) * d & q |^ n1 > d & d > 0 ) and
A2: q is prime ; :: thesis: ( not (a |^ (n -' 1)) mod n = 1 or not ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 or n is prime )
set f = q |^ n1;
assume A3: (a |^ (n -' 1)) mod n = 1 ; :: thesis: ( not ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 or n is prime )
assume A4: ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 ; :: thesis: n is prime
for q1 being Element of NAT st q1 divides q |^ n1 & q1 is prime holds
ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 )

proof

let q1 be Element of NAT ; :: thesis: ( q1 divides q |^ n1 & q1 is prime implies ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 ) )
assume A5: q1 divides q |^ n1 ; :: thesis: ( not q1 is prime or ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 ) )
assume A6: q1 is prime ; :: thesis: ex a being Element of NAT st
( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 )
consider a being Element of NAT such that
A7: ( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 ) by A3, A4;
take a ; :: thesis: ( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 )
thus ( (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q1)) -' 1) gcd n = 1 ) by A2, A5, A6, A7, Th18; :: thesis: verum

end;

hence n is prime by A1, Th24; :: thesis: verum