let k, n be prime Nat; :: thesis: n * k divides ((2 |^ n) - 2) * ((2 |^ k) - 2)
( n divides (2 |^ n) - 2 & k divides (2 |^ k) - 2 ) by Th40;
hence n * k divides ((2 |^ n) - 2) * ((2 |^ k) - 2) by NAT_3:1; :: thesis: verum