30 = 3 * 10 ;
then A1: 32,2 are_congruent_mod 3 ;
1023 = 3 * 341 ;
then 2 |^ 10,1 are_congruent_mod 3 by Lm10;
then (2 |^ 10) |^ 64,1 |^ 64 are_congruent_mod 3 by GR_CY_3:34;
then (2 |^ 640) * (2 |^ 5),1 * (2 |^ 5) are_congruent_mod 3 by Lm1122, INT_4:11;
then 2 |^ 645,2 are_congruent_mod 3 by Lm5, Lm1123, A1, INT_1:15;
hence 3 divides (2 |^ 645) - 2 ; :: thesis: verum