A1: 2 to_power 1 = 2 |^ 1
.= 2 by NEWTON:10 ;
A2: 16 -' 1 = 16 - 1 by XREAL_0:def 2
.= 15 + 0 ;
A3: ((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:13 ;
then (256 * 256) div 2 = 2 to_power (16 -' 1) by A1, NAT_2:18
.= 2 |^ (8 + 7) by A2
.= 256 * (2 |^ (4 + 3)) by Lm7, NEWTON:13
.= 256 * (16 * 8) by NEWTON:13, POWER:69, POWER:70
.= 256 * 128 ;
then Fermat 4 divides (3 |^ (((Fermat 4) -' 1) div 2)) - (- 1) by A3, Lm49, Th59;
then 3 |^ (((Fermat 4) -' 1) div 2), - 1 are_congruent_mod Fermat 4 by INT_2:19;
hence (256 * 256) + 1 is prime by Th59, Th63; :: thesis: verum