A2: ((256 * 256) + 1) -' 1 = ((256 * 256) + 1) - 1 by XREAL_0:def 2
.= (256 * 256) + 0 ;
Fermat 4 divides (3 |^ (((Fermat 4) -' 1) div 2)) - (- 1) by A2, Lm48, Th54;
then 3 |^ (((Fermat 4) -' 1) div 2), - 1 are_congruent_mod Fermat 4 ;
hence (256 * 256) + 1 is prime by Th54, Th58; :: thesis: verum