A1:
(256 * 16) * (256 * 16) = (255 * ((256 * 256) + 1)) + (673 * 97)
;
(3 |^ (256 * 32)) * (3 |^ (256 * 32)) =
3 |^ ((256 * 32) + (256 * 32))
by NEWTON:8
.=
3 |^ (256 * (32 + 32))
;
then (3 |^ (256 * 64)) mod (Fermat 4) =
((256 * 16) * (256 * 16)) mod (Fermat 4)
by Lm44, NAT_D:67
.=
673 * 97
by A1, Th54, NAT_D:def 2
;
hence
(3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97
; verum