let a, n be Nat; :: thesis: ( (2 * n) + 1 is prime implies for k being Nat st 2 * n > k & k > 1 holds
( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k ) )

assume A1: (2 * n) + 1 is prime ; :: thesis: for k being Nat st 2 * n > k & k > 1 holds
( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )

set p = (2 * n) + 1;
2 * n <> 0 by A1;
then A1a: n > 0 ;
let k be Nat; :: thesis: ( 2 * n > k & k > 1 implies ( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k ) )
assume A1b: ( 2 * n > k & k > 1 ) ; :: thesis: ( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )
A1c: k - 1 > 1 - 1 by ;
A1d: ( (k - 1) + 2 > (k - 1) + 1 & (k - 1) + 1 > (k - 1) + 0 ) by XREAL_1:6;
(2 * n) + 1 > k + 1 by ;
then ( (2 * n) + 1 > k + 1 & (2 * n) + 1 > k ) by ;
then A2: ( (2 * n) + 1 > k + 1 & (2 * n) + 1 > k & (2 * n) + 1 > k - 1 ) by ;
A3: ( (2 * n) + 1 divides a or (2 * n) + 1 divides (a |^ n) - 1 or (2 * n) + 1 divides (a |^ n) + 1 ) by ;
a divides a |^ n by ;
then ( (2 * n) + 1 divides a implies (2 * n) + 1 divides a |^ n ) by INT_2:9;
then A4: ( (2 * n) + 1 divides (- 1) * (a |^ n) or (2 * n) + 1 divides (- 1) * ((a |^ n) - 1) or (2 * n) + 1 divides (- 1) * ((a |^ n) + 1) ) by ;
assume ( (2 * n) + 1 divides (a |^ n) - k or (2 * n) + 1 divides (a |^ n) + k ) ; :: thesis: contradiction
then ( (2 * n) + 1 divides (- (a |^ n)) + ((a |^ n) - k) or (2 * n) + 1 divides (- (a |^ n)) + ((a |^ n) + k) or (2 * n) + 1 divides ((- (a |^ n)) - 1) + ((a |^ n) - k) or (2 * n) + 1 divides ((- (a |^ n)) - 1) + ((a |^ n) + k) or (2 * n) + 1 divides ((- (a |^ n)) + 1) + ((a |^ n) - k) or (2 * n) + 1 divides ((- (a |^ n)) + 1) + ((a |^ n) + k) ) by ;
then ( (2 * n) + 1 divides - k or (2 * n) + 1 divides k or (2 * n) + 1 divides - (1 + k) or (2 * n) + 1 divides (- 1) + k or (2 * n) + 1 divides - (k - 1) or (2 * n) + 1 divides 1 + k ) ;
hence contradiction by A1b, A1c, A2, INT_2:27, INT_2:10; :: thesis: verum