let a, b be Nat; :: thesis: ( a,b are_coprime implies a + b,((a |^ 2) + (b |^ 2)) + (a * b) are_coprime )
assume A1: a,b are_coprime ; :: thesis: a + b,((a |^ 2) + (b |^ 2)) + (a * b) are_coprime
A2: |.(((a |^ 2) + (b |^ 2)) - (((1 - 2) * a) * b)).| in NAT by INT_1:3;
((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) + (a * b)) = |.(((a |^ 2) + (b |^ 2)) - (((1 - 2) * a) * b)).| gcd |.1.| by A1, Th74
.= 1 by NEWTON:51, A2 ;
then (a + b) |^ 2,((a |^ 2) + (b |^ 2)) + (a * b) are_coprime ;
hence a + b,((a |^ 2) + (b |^ 2)) + (a * b) are_coprime by Th73; :: thesis: verum