let a, b, c be Nat; :: thesis: for n being odd Nat holds ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3
let n be odd Nat; :: thesis: ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3
A1: ( (a |^ n) mod 3 = a mod 3 & (b |^ n) mod 3 = b mod 3 & (c |^ n) mod 3 = c mod 3 ) by Th87;
((a + b) - c) mod 3 = (((a mod 3) + (b mod 3)) + (2 * (c mod 3))) mod 3 by LmSum
.= (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3 by A1, LmSum ;
hence ((a + b) - c) mod 3 = (((a |^ n) + (b |^ n)) - (c |^ n)) mod 3 ; :: thesis: verum