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 by Th1; :: thesis: verum