let a, b, n be Nat; ( 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
; ((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 A1, Th28;
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 A4, INT_6:19
;
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; verum