let t be Integer; :: thesis: for a, b, c being odd Nat holds 3 divides ((t |^ a) + (t |^ b)) + (t |^ c)
let a, b, c be odd Nat; :: thesis: 3 divides ((t |^ a) + (t |^ b)) + (t |^ c)
A1: ( (t |^ a) mod 3 = t mod 3 & (t |^ b) mod 3 = t mod 3 & (t |^ c) mod 3 = t mod 3 ) by Th87;
(((t |^ a) + (t |^ b)) + (t |^ c)) mod 3 = (((t |^ a) + (t |^ b)) + ((t |^ c) mod 3)) mod 3 by Th88
.= ((((t |^ c) mod 3) + (t |^ a)) + (t |^ b)) mod 3
.= ((((t |^ c) mod 3) + (t |^ a)) + ((t |^ b) mod 3)) mod 3 by Th88
.= ((((t |^ c) mod 3) + ((t |^ b) mod 3)) + (t |^ a)) mod 3
.= ((((t |^ c) mod 3) + ((t |^ b) mod 3)) + ((t |^ a) mod 3)) mod 3 by Th88
.= (0 + (3 * (t mod 3))) mod 3 by A1
.= 0 ;
hence 3 divides ((t |^ a) + (t |^ b)) + (t |^ c) by INT_1:62; :: thesis: verum