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, Th27;
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
; verum