(2 |^ 4) |^ 276,1 |^ 276 are_congruent_mod 5 by Lm1141, GR_CY_3:34;
then (2 |^ 1104) * (2 |^ 1),1 * 2 are_congruent_mod 5 by Lm1129, INT_4:11;
hence 5 divides (2 |^ 1105) - 2 by Lm1128; :: thesis: verum