(3 |^ 4) |^ 276,1 |^ 276 are_congruent_mod 5 by Lm1142, GR_CY_3:34;
then (3 |^ 1104) * (3 |^ 1),1 * 3 are_congruent_mod 5 by Lm1138, INT_4:11;
hence 5 divides (3 |^ 1105) - 3 by Lm1139; :: thesis: verum