let a, b be Nat; :: thesis: for n being odd Nat holds
( 3 divides (a |^ n) + (b |^ n) iff 3 divides a + b )
let n be odd Nat; :: thesis: ( 3 divides (a |^ n) + (b |^ n) iff 3 divides a + b )
consider k being Nat such that
A0: n = (2 * k) + 1 by ABIAN:9;
( 3 divides (a |^ n) + (b |^ n) implies 3 divides a + b )
proof
assume A1: 3 divides (a |^ n) + (b |^ n) ; :: thesis: 3 divides a + b
( 3 divides (a |^ n) - a & 3 divides (b |^ n) - b ) by A0, NEWTON02:173;
then 3 divides ((a |^ n) - a) + ((b |^ n) - b) by WSIERP_1:4;
then 3 divides ((a |^ n) + (b |^ n)) + (- (a + b)) ;
then 3 divides - (a + b) by A1, INT_2:1;
hence 3 divides a + b by INT_2:10; :: thesis: verum
end;
hence ( 3 divides (a |^ n) + (b |^ n) iff 3 divides a + b ) by A0, NEWTON02:196, PEPIN:41; :: thesis: verum