A1: 84 |^ (2 |^ 6) = (84 |^ 2) |^ 32 by Lm6, NEWTON:9;
A2: 84 |^ 2 = 84 * 84 by WSIERP_1:1;
(257 * 27) + 117,117 are_congruent_mod 257 ;
then A3: (84 |^ 2) |^ 32,117 |^ 32 are_congruent_mod 257 by A2, GR_CY_3:34;
A4: 117 |^ (2 * 16) = (117 |^ 2) |^ 16 by NEWTON:9;
A5: 117 |^ 2 = 117 * 117 by WSIERP_1:1;
(53 * 257) + 68,68 are_congruent_mod 257 ;
then (117 |^ 2) |^ 16,68 |^ 16 are_congruent_mod 257 by A5, GR_CY_3:34;
then A6: 84 |^ (2 |^ 6),68 |^ 16 are_congruent_mod 257 by A1, A3, A4, INT_1:15;
A7: 4 |^ 4 = ((4 * 4) * 4) * 4 by POLYEQ_5:3;
A8: 68 |^ 4 = ((68 * 68) * 68) * 68 by POLYEQ_5:3;
A9: 68 |^ (4 * 4) = (68 |^ 4) |^ 4 by NEWTON:9;
21381376 = (83196 * 257) + 4 ;
then 68 |^ 4,4 are_congruent_mod 257 by A8;
then (68 |^ 4) |^ 4,4 |^ 4 are_congruent_mod 257 by GR_CY_3:34;
then 84 |^ (2 |^ 6),4 |^ 4 are_congruent_mod 257 by A6, A9, INT_1:15;
then (84 |^ (2 |^ 6)) + 1,256 + 1 are_congruent_mod 257 by A7;
hence 257 divides (84 |^ (2 |^ 6)) + 1 by Th32; :: thesis: verum