A1: 4 -' 1 = 4 - 1 by XREAL_0:def 2
.= 3 + 0 ;
A2: 17 -' 1 = 17 - 1 by XREAL_0:def 2
.= 16 + 0 ;
16 div 2 = 8 by A1, POWER:61, POWER:62, NAT_2:16, Lm22;
then ((Fermat 2) -' 1) div 2 = (16 * 0) + 8 by A2, Th52;
then Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) + 1 by Lm24;
then Fermat 2 divides (3 |^ (((Fermat 2) -' 1) div 2)) - (- 1) ;
then 3 |^ (((Fermat 2) -' 1) div 2), - 1 are_congruent_mod Fermat 2 ;
hence 17 is prime by Th52, Th58; :: thesis: verum