let n be Nat; :: thesis: ( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff not 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 )
not not n mod (3 + 1) = 0 & ... & not n mod (3 + 1) = 3 by Th11;
hence ( 5 divides ((2 |^ ((2 * n) + 1)) - (2 |^ (n + 1))) + 1 iff not 5 divides ((2 |^ ((2 * n) + 1)) + (2 |^ (n + 1))) + 1 ) by Th39, Th40; :: thesis: verum