let a, n be Nat; :: thesis: for p being prime Nat holds
( not p = (2 * n) + 1 or p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )
let p be prime Nat; :: thesis: ( not p = (2 * n) + 1 or p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )
assume A1: p = (2 * n) + 1 ; :: thesis: ( p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 )
(a |^ ((2 * n) + 1)) - a = ((a |^ (2 * n)) * a) - a by NEWTON:6
.= a * ((a |^ (2 * n)) - 1)
.= a * (((a |^ n) |^ 2) - (1 |^ 2)) by NEWTON:9
.= a * (((a |^ n) - 1) * ((a |^ n) + 1)) by NEWTON01:1 ;
then ( p divides a or p divides ((a |^ n) - 1) * ((a |^ n) + 1) ) by A1, Th58, INT_5:7;
hence ( p divides a or p divides (a |^ n) - 1 or p divides (a |^ n) + 1 ) by INT_5:7; :: thesis: verum