A1: 645 = (3 * 5) * 43 ;
3,5,43 are_mutually_coprime by PEPIN:41, PEPIN:59, NAT_4:32, INT_2:30;
hence 645 divides (2 |^ 645) - 2 by A1, Th41, Th42, Th43, Th12; :: thesis: verum