A1:
28 |^ (2 |^ 3) = (28 |^ 2) |^ 4
by Lm3, NEWTON:9;
A2:
28 |^ 2 = 28 * 28
by WSIERP_1:1;
17 + 11,11 are_congruent_mod 17
;
then A3:
28 * 28,11 * 11 are_congruent_mod 17
by INT_1:18;
(7 * 17) + 2,2 are_congruent_mod 17
;
then
28 * 28,2 are_congruent_mod 17
by A3, INT_1:15;
then
(28 |^ 2) |^ 4,2 |^ 4 are_congruent_mod 17
by A2, GR_CY_3:34;
then
((28 |^ 2) |^ 4) + 1,(2 |^ 4) + 1 are_congruent_mod 17
;
hence
17 divides (28 |^ (2 |^ 3)) + 1
by A1, Lm4, Th32; verum