A1: 1105 = (5 * 13) * 17 ;
5,13,17 are_mutually_coprime by PEPIN:59, PEPIN:60, NAT_4:28, INT_2:30;
hence 1105 divides (2 |^ 1105) - 2 by A1, Th45, Th46, Th47, Th12; :: thesis: verum