let a, b, n be Nat; :: thesis: ( a,b are_coprime implies ((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) gcd n )
A0: ( a |^ 2 = a * a & b |^ 2 = b * b ) by NEWTON:81;
assume A1: a,b are_coprime ; :: thesis: ((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) gcd n
A2: (a + b) |^ 2 = (a + b) * (a + b) by NEWTON:81
.= (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) + ((n * a) * b) by A0 ;
(a |^ (0 + 1)) + (b |^ (0 + 1)),a * b are_coprime by ;
then (a + b) |^ 2,a * b are_coprime by WSIERP_1:10;
then 1 = (((a + b) |^ 2) - (n * (a * b))) gcd (a * b) by Th5
.= (((((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) + ((n * a) * b)) - ((n * a) * b)) gcd (a * b) by A2 ;
then A4: ((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b),a * b are_coprime ;
((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((n * a) * b) + (1 * (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)))) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) by A2
.= (n * (a * b)) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) by Th5
.= n gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) by ;
hence ((a + b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) - (((n - 2) * a) * b)) gcd n ; :: thesis: verum