let n be Nat; :: thesis: 5 divides (2 |^ (4 * n)) - 1
(3 * 5) + 1,1 are_congruent_mod 5 ;
then (2 |^ 4) |^ n,1 |^ n are_congruent_mod 5 by Lm3, GR_CY_3:34;
hence 5 divides (2 |^ (4 * n)) - 1 by NEWTON:9; :: thesis: verum