A1:
(22 |^ 3) |^ 7 = 22 |^ (3 * 7)
by NEWTON:9;
A2:
(22 |^ 21) |^ 2 = 22 |^ (21 * 2)
by NEWTON:9;
A3: ((3 |^ 3) |^ 5) |^ 43 =
(3 |^ (3 * 5)) |^ 43
by NEWTON:9
.=
3 |^ ((3 * 5) * 43)
by NEWTON:9
;
27 |^ 5 = (((27 * 27) * 27) * 27) * 27
by NUMBER02:1;
then
(27 |^ 5) - 22 = 43 * ((3336 * 100) + 95)
;
then
27 |^ 5,22 are_congruent_mod 43
;
then A4:
((3 |^ 3) |^ 5) |^ 43,22 |^ 43 are_congruent_mod 43
by Lm1109, GR_CY_3:34;
22 |^ 3 = (22 * 22) * 22
by POLYEQ_5:2;
then
(22 |^ 3) - 27 = 43 * 247
;
then
22 |^ 3,27 are_congruent_mod 43
;
then A5:
(22 |^ 3) |^ 7,27 |^ 7 are_congruent_mod 43
by GR_CY_3:34;
27 |^ 7 = (((((27 * 27) * 27) * 27) * 27) * 27) * 27
by NUMBER02:3;
then
(27 |^ 7) - 42 = 43 * ((24326 * 10000) + 4027)
;
then
27 |^ 7,42 are_congruent_mod 43
;
then
(22 |^ 3) |^ 7,42 are_congruent_mod 43
by A5, INT_1:15;
then A6:
((22 |^ 3) |^ 7) |^ 2,42 |^ 2 are_congruent_mod 43
by GR_CY_3:34;
42 |^ 2 = 42 * 42
by WSIERP_1:1;
then
(42 |^ 2) - 1 = 43 * 41
;
then
42 |^ 2,1 are_congruent_mod 43
;
then
((22 |^ 3) |^ 7) |^ 2,1 are_congruent_mod 43
by A6, INT_1:15;
then
(22 |^ 42) * 22,1 * 22 are_congruent_mod 43
by A1, A2, INT_4:11;
then
22 |^ (42 + 1),22 are_congruent_mod 43
by NEWTON:6;
then
3 |^ 645,22 are_congruent_mod 43
by A3, A4, INT_1:15;
then
not 3 |^ 645,3 are_congruent_mod 43
by NAT_6:14;
hence
not 43 divides (3 |^ 645) - 3
; verum