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, INT_2:10;
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 D3; :: thesis: verum