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