A1: ((83 * 3) * 83) * 3 = (241 * 257) + 64 ;
(3 |^ 32) mod (Fermat 3) = (3 |^ (16 + 16)) mod (Fermat 3)
.= ((3 |^ 16) * (3 |^ 16)) mod (Fermat 3) by NEWTON:8
.= ((83 * 3) * (83 * 3)) mod (Fermat 3) by Lm28, NAT_D:67
.= 64 by A1, Th53, NAT_D:def 2 ;
hence (3 |^ 32) mod (Fermat 3) = 64 ; :: thesis: verum