A2: 17 -' 1 = 17 - 1 by XREAL_0:def 2
.= 16 + 0 ;
((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