A1: 24 |^ 2 = 24 * 24 by WSIERP_1:1;
A2: 49 |^ 4 = ((49 * 49) * 49) * 49 by POLYEQ_5:3;
17 + 7,7 are_congruent_mod 17 ;
then 24 * 24,7 * 7 are_congruent_mod 17 by INT_1:18;
then (24 |^ 2) |^ 4,49 |^ 4 are_congruent_mod 17 by A1, GR_CY_3:34;
then A3: ((24 |^ 2) |^ 4) + 1,(49 |^ 4) + 1 are_congruent_mod 17 ;
17 * 339106, 0 are_congruent_mod 17 ;
then ((24 |^ 2) |^ 4) + 1, 0 are_congruent_mod 17 by A3, A2, INT_1:15;
hence 17 divides (24 |^ (2 |^ 3)) + 1 by Lm3, NEWTON:9; :: thesis: verum