let a, b, n be Nat; :: thesis: ( a,b are_coprime implies a * b,(a |^ (n + 1)) - (b |^ (n + 1)) are_coprime )
A1: b * (b |^ n) = |.(b |^ (n + 1)).| by NEWTON:6;
A2: a * (a |^ n) = |.(a |^ (n + 1)).| by NEWTON:6;
A3: |.((a |^ (n + 1)) - (b |^ (n + 1))).| = |.(- ((a |^ (n + 1)) - (b |^ (n + 1)))).| by COMPLEX1:52;
assume a,b are_coprime ; :: thesis: a * b,(a |^ (n + 1)) - (b |^ (n + 1)) are_coprime
then a |^ (n + 1),b |^ (n + 1) are_coprime by WSIERP_1:11;
then ( ((a |^ (n + 1)) - (1 * (b |^ (n + 1)))) gcd (b |^ (n + 1)) = 1 & ((b |^ (n + 1)) - (1 * (a |^ (n + 1)))) gcd (a |^ (n + 1)) = 1 ) by Th5;
then ( |.((a |^ (n + 1)) - (b |^ (n + 1))).| * 1,b * (b |^ n) are_coprime & |.((a |^ (n + 1)) - (b |^ (n + 1))).| * 1,a * (a |^ n) are_coprime ) by A1, A2, A3, INT_2:34;
then ( |.((a |^ (n + 1)) - (b |^ (n + 1))).|,b are_coprime & |.((a |^ (n + 1)) - (b |^ (n + 1))).|,a are_coprime ) by NEWTON01:41;
then |.((a |^ (n + 1)) - (b |^ (n + 1))).|,a * b are_coprime by INT_2:26;
hence a * b,(a |^ (n + 1)) - (b |^ (n + 1)) are_coprime by INT_6:14; :: thesis: verum