A1: 8 -' 1 = 8 - 1 by XREAL_0:def 2
.= 7 + 0 ;
A2: 257 -' 1 = 257 - 1 by XREAL_0:def 2
.= 256 + 0 ;
2 to_power 8 = 2 |^ (4 + 4)
.= 16 * 16 by NEWTON:8, POWER:62
.= 256 ;
then 256 div 2 = 2 to_power (8 -' 1) by Lm22, NAT_2:16
.= 2 |^ (4 + 3) by A1
.= 16 * 8 by NEWTON:8, POWER:61, POWER:62
.= 128 ;
then Fermat 3 divides (3 |^ (((Fermat 3) -' 1) div 2)) - (- 1) by A2, Lm47, Th53;
then 3 |^ (((Fermat 3) -' 1) div 2), - 1 are_congruent_mod Fermat 3 ;
hence 257 is prime by Th53, Th58; :: thesis: verum