let k be Nat; :: thesis: for n being odd Prime st n = (2 * k) + 1 holds
( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 )
let n be odd Prime; :: thesis: ( n = (2 * k) + 1 implies ( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 ) )
assume A1: n = (2 * k) + 1 ; :: thesis: ( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 )
not 2 divides n ;
then A2: not n divides 2 by INT_2:28, INT_2:30, PYTHTRIP:def 2;
A3: ( n divides (2 |^ k) - 1 or n divides (2 |^ k) + 1 )

proof

n divides (2 |^ ((2 * k) + 1)) - 2 by A1, Th40;
then n divides ((2 |^ (2 * k)) * 2) - 2 by NEWTON:6;
then n divides 2 * ((2 |^ (2 * k)) - (1 |^ 2)) ;
then n divides (2 |^ (2 * k)) - 1 by A2, INT_5:7;
then n divides ((2 |^ k) |^ 2) - (1 |^ 2) by NEWTON:9;
then n divides ((2 |^ k) - 1) * ((2 |^ k) + 1) by NEWTON01:1;
hence ( n divides (2 |^ k) - 1 or n divides (2 |^ k) + 1 ) by INT_5:7; :: thesis: verum

end;

((2 |^ k) + 1) - ((2 |^ k) - 1) = 2 ;
hence ( n divides (2 |^ k) - 1 iff not n divides (2 |^ k) + 1 ) by A2, INT_5:1, A3; :: thesis: verum