let n be Nat; :: thesis: for t, z being Integer st 3 divides t - z holds
3 divides (t |^ n) - (z |^ n)
let t, z be Integer; :: thesis: ( 3 divides t - z implies 3 divides (t |^ n) - (z |^ n) )
( 3 divides t - z & t - z divides (t |^ n) - (z |^ n) implies 3 divides (t |^ n) - (z |^ n) ) by INT_2:9;
hence ( 3 divides t - z implies 3 divides (t |^ n) - (z |^ n) ) by Th18; :: thesis: verum