let a, n be Nat; ( (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
; 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; ( 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 )
; ( not (2 * n) + 1 divides (a |^ n) - k & not (2 * n) + 1 divides (a |^ n) + k )
A1c:
k - 1 > 1 - 1
by A1b, XREAL_1:9;
A1d:
( (k - 1) + 2 > (k - 1) + 1 & (k - 1) + 1 > (k - 1) + 0 )
by XREAL_1:6;
(2 * n) + 1 > k + 1
by A1b, XREAL_1:6;
then
( (2 * n) + 1 > k + 1 & (2 * n) + 1 > k )
by A1d, XXREAL_0:2;
then A2:
( (2 * n) + 1 > k + 1 & (2 * n) + 1 > k & (2 * n) + 1 > k - 1 )
by A1d, XXREAL_0:2;
A3:
( (2 * n) + 1 divides a or (2 * n) + 1 divides (a |^ n) - 1 or (2 * n) + 1 divides (a |^ n) + 1 )
by A1, Th70;
a divides a |^ n
by A1a, NAT_3:3;
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 A3, INT_2:2;
assume
( (2 * n) + 1 divides (a |^ n) - k or (2 * n) + 1 divides (a |^ n) + k )
; 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 A4, WSIERP_1:4;
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; verum