let n be Nat; :: thesis: for a, b being odd Nat st 4 divides (a |^ n) + (b |^ n) holds
not 4 divides (a |^ (2 * n)) + (b |^ (2 * n))
let a, b be odd Nat; :: thesis: ( 4 divides (a |^ n) + (b |^ n) implies not 4 divides (a |^ (2 * n)) + (b |^ (2 * n)) )
A0: ( (a |^ n) |^ 2 = a |^ (2 * n) & (b |^ n) |^ 2 = b |^ (2 * n) ) by NEWTON:9;
assume 4 divides (a |^ n) + (b |^ n) ; :: thesis: not 4 divides (a |^ (2 * n)) + (b |^ (2 * n))
then 4 divides ((a |^ n) + (b |^ n)) * ((a |^ n) - (b |^ n)) by INT_2:2;
then 4 divides (a |^ (2 * n)) - (b |^ (2 * n)) by A0, NEWTON01:1;
hence not 4 divides (a |^ (2 * n)) + (b |^ (2 * n)) by NEWTON02:58; :: thesis: verum