let a, b, n be Nat; :: thesis: ( a,b are_coprime implies a * b,(a |^ (n + 1)) + (b |^ (n + 1)) are_coprime )
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 NEWTON:6;
then ( (a |^ (n + 1)) + (b |^ (n + 1)),b are_coprime & (a |^ (n + 1)) + (b |^ (n + 1)),a are_coprime ) by NEWTON01:41;
hence a * b,(a |^ (n + 1)) + (b |^ (n + 1)) are_coprime by INT_2:26; :: thesis: verum