let n be Nat; :: thesis: for u, v being Integer st u - v is even holds
( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
let u, v be Integer; :: thesis: ( u - v is even implies ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even ) )
assume A1: u - v is even ; :: thesis: ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
per cases ( ( u is even & v is even ) or ( u is odd & v is odd ) or ( u is odd & v is even ) or ( u is even & v is odd ) ) ;
suppose A2: ( u is even & v is even ) ; :: thesis: ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
then ( ( u |^ n is even & v |^ n is even ) or n = 0 ) ;
then A3a: ( ( u |^ n is even & v |^ n is even ) or ( u |^ n = 1 & v |^ n = 1 ) ) by NEWTON:4;
then ( (u |^ n) - (v |^ n) is even or (u |^ n) - (v |^ n) = 0 ) ;
hence ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even ) by A2, A3a; :: thesis: verum
end;
suppose ( u is odd & v is odd ) ; :: thesis: ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
hence ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even ) ; :: thesis: verum
end;
suppose ( u is odd & v is even ) ; :: thesis: ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
hence ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even ) by A1; :: thesis: verum
end;
suppose ( u is even & v is odd ) ; :: thesis: ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even )
hence ( u + v is even & (u |^ n) - (v |^ n) is even & (u |^ n) + (v |^ n) is even ) by A1; :: thesis: verum
end;
end;