A1:
22 |^ 2 = 22 * 22
by WSIERP_1:1;
17 + 5,5 are_congruent_mod 17
;
then A2:
22 * 22,5 * 5 are_congruent_mod 17
by INT_1:18;
(1 * 17) + 8,8 are_congruent_mod 17
;
then
22 * 22,8 are_congruent_mod 17
by A2, INT_1:15;
then
(22 |^ 2) |^ 4,8 |^ 4 are_congruent_mod 17
by A1, GR_CY_3:34;
then A3:
((22 |^ 2) |^ 4) + 1,(8 |^ 4) + 1 are_congruent_mod 17
;
(8 |^ 4) + 1, 0 are_congruent_mod 17
by Lm32, Lm33;
then
((22 |^ 2) |^ 4) + 1, 0 are_congruent_mod 17
by A3, INT_1:15;
hence
17 divides (22 |^ (2 |^ 3)) + 1
by Lm3, NEWTON:9; verum