let a, b, n be Nat; ( a,b are_coprime implies a * b,(a |^ (n + 1)) + (b |^ (n + 1)) are_coprime )
assume
a,b are_coprime
; 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; verum