A1: 257 = (257 * 1) + 0 ;
1 = (257 * 0) + 1 ;
then 1 mod (Fermat 3) = 1 by Th53, NAT_D:def 2;
then ((3 |^ ((32 * 0) + 128)) + 1) mod (Fermat 3) = (256 + 1) mod (Fermat 3) by Lm31, EULER_2:6
.= 0 by A1, Th53, NAT_D:def 2 ;
hence Fermat 3 divides (3 |^ ((32 * 0) + 128)) + 1 by Th7, NAT_D:6; :: thesis: verum