let m be non zero Nat; :: thesis: (2 |^ m) - 1,(((2 |^ m) - 1) |^ m) - 1 are_coprime
1 <= m by NAT_1:14;
then ((2 |^ m) - 1) |^ 1 divides ((2 |^ m) - 1) |^ m by NEWTON03:16;
hence (2 |^ m) - 1,(((2 |^ m) - 1) |^ m) - 1 are_coprime by NUMBER07:6; :: thesis: verum