A1: 1 mod (Fermat 3) = 1

proof

1 = (257 * 0 ) + 1 ;
hence 1 mod (Fermat 3) = 1 by Th58, NAT_D:def 2; :: thesis: verum

end;

A2: 257 mod (Fermat 3) = 0

proof

257 = (257 * 1) + 0 ;
hence 257 mod (Fermat 3) = 0 by Th58, NAT_D:def 2; :: thesis: verum

end;

((3 |^ ((32 * 0 ) + 128)) + 1) mod (Fermat 3) = (256 + 1) mod (Fermat 3) by A1, Lm35, EULER_2:8
.= 0 by A2 ;
then Fermat 3 divides ((3 |^ ((32 * 0 ) + 128)) + 1) mod (Fermat 3) by NAT_D:6;
hence Fermat 3 divides (3 |^ ((32 * 0 ) + 128)) + 1 by Th7; :: thesis: verum