let a, b, c be Nat; :: thesis: for n being odd Nat holds
( 3 divides (a + b) - c iff 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) )
let n be odd Nat; :: thesis: ( 3 divides (a + b) - c iff 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) )
thus ( 3 divides (a + b) - c implies 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) ) :: thesis: ( 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) implies 3 divides (a + b) - c )
proof
assume 3 divides (a + b) - c ; :: thesis: 3 divides ((a |^ n) + (b |^ n)) - (c |^ n)
then ((a + b) - c) mod 3 = 0 by INT_1:62;
then (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3 = 0 by Th89;
hence 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) by INT_1:62; :: thesis: verum
end;
assume 3 divides ((a |^ n) + (b |^ n)) - (c |^ n) ; :: thesis: 3 divides (a + b) - c
then (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3 = 0 by INT_1:62;
then ((a + b) - c) mod 3 = 0 by Th89;
hence 3 divides (a + b) - c by INT_1:62; :: thesis: verum