A1: 16 -' 1 = 16 - 1 by XREAL_0:def 2
.= 15 + 0 ;
A2: ((256 * 256) + 1) -' 1 = ((256 * 256) + 1) - 1 by XREAL_0:def 2
.= (256 * 256) + 0 ;
2 to_power 16 = 2 |^ (8 + 8)
.= 256 * 256 by Lm7, NEWTON:8 ;
then (256 * 256) div 2 = 2 to_power (16 -' 1) by Lm22, NAT_2:16
.= 2 |^ (8 + 7) by A1
.= 256 * (2 |^ (4 + 3)) by Lm7, NEWTON:8
.= 256 * (16 * 8) by NEWTON:8, POWER:61, POWER:62
.= 256 * 128 ;
then 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