let n be Nat; :: thesis: for a, b being odd Nat st 4 divides a - b holds
not 4 divides (a |^ n) + (b |^ n)
let a, b be odd Nat; :: thesis: ( 4 divides a - b implies not 4 divides (a |^ n) + (b |^ n) )
assume A1: 4 divides a - b ; :: thesis: not 4 divides (a |^ n) + (b |^ n)
per cases ( n is odd or n is even ) ;
suppose n is odd ; :: thesis: not 4 divides (a |^ n) + (b |^ n)
hence not 4 divides (a |^ n) + (b |^ n) by A1, NEWTON02:69; :: thesis: verum
end;
suppose n is even ; :: thesis: not 4 divides (a |^ n) + (b |^ n)
then 4 divides (a |^ n) - (b |^ n) by NEWTON02:65;
hence not 4 divides (a |^ n) + (b |^ n) by NEWTON02:58; :: thesis: verum
end;
end;