A1: 561 = (3 * 11) * 17 ;
3,11,17 are_mutually_coprime by PEPIN:41, PEPIN:60, NAT_4:27, INT_2:30;
hence 561 divides (3 |^ 561) - 3 by A1, Th51, Th52, Th53, Th12; :: thesis: verum