let X be Subset of NAT; :: thesis: ( X is Pythagorean_triple iff ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) )

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ; :: thesis: X is Pythagorean_triple

then consider k, m, n being Element of NAT such that

A15: m <= n and

A16: X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ;

m ^2 <= n ^2 by A15, SQUARE_1:15;

then reconsider a9 = (n ^2) - (m ^2) as Element of NAT by INT_1:3, XREAL_1:48;

set c9 = (n ^2) + (m ^2);

set b9 = (2 * m) * n;

((k * a9) ^2) + ((k * ((2 * m) * n)) ^2) = (k * ((n ^2) + (m ^2))) ^2 ;

hence X is Pythagorean_triple by A16, Def4; :: thesis: verum

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) )

hereby :: thesis: ( ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) implies X is Pythagorean_triple )

assume
ex k, m, n being Element of NAT st ( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) implies X is Pythagorean_triple )

assume
X is Pythagorean_triple
; :: thesis: ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then consider a, b, c being Element of NAT such that

A1: (a ^2) + (b ^2) = c ^2 and

A2: X = {a,b,c} by Def4;

set k = a gcd b;

A3: a gcd b divides a by NAT_D:def 5;

A4: a gcd b divides b by NAT_D:def 5;

end;( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then consider a, b, c being Element of NAT such that

A1: (a ^2) + (b ^2) = c ^2 and

A2: X = {a,b,c} by Def4;

set k = a gcd b;

A3: a gcd b divides a by NAT_D:def 5;

A4: a gcd b divides b by NAT_D:def 5;

per cases
( a gcd b = 0 or a gcd b <> 0 )
;

end;

suppose
a gcd b = 0
; :: thesis: ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then A5:
( a = 0 & b = 0 )
by A3, A4;

thus ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) :: thesis: verum

end;thus ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) :: thesis: verum

proof

take
0
; :: thesis: ex m, n being Element of NAT st

( m <= n & X = {(0 * ((n ^2) - (m ^2))),(0 * ((2 * m) * n)),(0 * ((n ^2) + (m ^2)))} )

take 0 ; :: thesis: ex n being Element of NAT st

( 0 <= n & X = {(0 * ((n ^2) - (0 ^2))),(0 * ((2 * 0) * n)),(0 * ((n ^2) + (0 ^2)))} )

take 0 ; :: thesis: ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} )

thus ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} ) by A1, A2, A5, XCMPLX_1:6; :: thesis: verum

end;( m <= n & X = {(0 * ((n ^2) - (m ^2))),(0 * ((2 * m) * n)),(0 * ((n ^2) + (m ^2)))} )

take 0 ; :: thesis: ex n being Element of NAT st

( 0 <= n & X = {(0 * ((n ^2) - (0 ^2))),(0 * ((2 * 0) * n)),(0 * ((n ^2) + (0 ^2)))} )

take 0 ; :: thesis: ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} )

thus ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} ) by A1, A2, A5, XCMPLX_1:6; :: thesis: verum

suppose A6:
a gcd b <> 0
; :: thesis: ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then A7:
(a gcd b) * (a gcd b) <> 0
by XCMPLX_1:6;

consider a9 being Nat such that

A8: a = (a gcd b) * a9 by A3, NAT_D:def 3;

consider b9 being Nat such that

A9: b = (a gcd b) * b9 by A4, NAT_D:def 3;

reconsider a9 = a9, b9 = b9 as Element of NAT by ORDINAL1:def 12;

(a gcd b) * (a9 gcd b9) = (a gcd b) * 1 by A8, A9, Th8;

then a9 gcd b9 = 1 by A6, XCMPLX_1:5;

then A10: a9,b9 are_coprime ;

c ^2 = ((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) by A1, A8, A9;

then (a gcd b) ^2 divides c ^2 ;

then a gcd b divides c by Th6;

then consider c9 being Nat such that

A11: c = (a gcd b) * c9 by NAT_D:def 3;

reconsider c9 = c9 as Element of NAT by ORDINAL1:def 12;

((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) = ((a gcd b) ^2) * (c9 ^2) by A1, A8, A9, A11;

then A12: (a9 ^2) + (b9 ^2) = c9 ^2 by A7, XCMPLX_1:5;

thus ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) :: thesis: verum

end;consider a9 being Nat such that

A8: a = (a gcd b) * a9 by A3, NAT_D:def 3;

consider b9 being Nat such that

A9: b = (a gcd b) * b9 by A4, NAT_D:def 3;

reconsider a9 = a9, b9 = b9 as Element of NAT by ORDINAL1:def 12;

(a gcd b) * (a9 gcd b9) = (a gcd b) * 1 by A8, A9, Th8;

then a9 gcd b9 = 1 by A6, XCMPLX_1:5;

then A10: a9,b9 are_coprime ;

c ^2 = ((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) by A1, A8, A9;

then (a gcd b) ^2 divides c ^2 ;

then a gcd b divides c by Th6;

then consider c9 being Nat such that

A11: c = (a gcd b) * c9 by NAT_D:def 3;

reconsider c9 = c9 as Element of NAT by ORDINAL1:def 12;

((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) = ((a gcd b) ^2) * (c9 ^2) by A1, A8, A9, A11;

then A12: (a9 ^2) + (b9 ^2) = c9 ^2 by A7, XCMPLX_1:5;

thus ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) :: thesis: verum

proof
end;

per cases
( a9 is odd or b9 is odd )
by A10;

end;

suppose
a9 is odd
; :: thesis: ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then consider m, n being Element of NAT such that

A13: ( m <= n & a9 = (n ^2) - (m ^2) & b9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11;

take a gcd b ; :: thesis: ex m, n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take m ; :: thesis: ex n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take n ; :: thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A13; :: thesis: verum

end;A13: ( m <= n & a9 = (n ^2) - (m ^2) & b9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11;

take a gcd b ; :: thesis: ex m, n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take m ; :: thesis: ex n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take n ; :: thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A13; :: thesis: verum

suppose
b9 is odd
; :: thesis: ex k, m, n being Element of NAT st

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} )

then consider m, n being Element of NAT such that

A14: ( m <= n & b9 = (n ^2) - (m ^2) & a9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11;

take a gcd b ; :: thesis: ex m, n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take m ; :: thesis: ex n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take n ; :: thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A14, ENUMSET1:58; :: thesis: verum

end;A14: ( m <= n & b9 = (n ^2) - (m ^2) & a9 = (2 * m) * n & c9 = (n ^2) + (m ^2) ) by A12, A10, Th11;

take a gcd b ; :: thesis: ex m, n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take m ; :: thesis: ex n being Element of NAT st

( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

take n ; :: thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )

thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A14, ENUMSET1:58; :: thesis: verum

( m <= n & X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) ; :: thesis: X is Pythagorean_triple

then consider k, m, n being Element of NAT such that

A15: m <= n and

A16: X = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ;

m ^2 <= n ^2 by A15, SQUARE_1:15;

then reconsider a9 = (n ^2) - (m ^2) as Element of NAT by INT_1:3, XREAL_1:48;

set c9 = (n ^2) + (m ^2);

set b9 = (2 * m) * n;

((k * a9) ^2) + ((k * ((2 * m) * n)) ^2) = (k * ((n ^2) + (m ^2))) ^2 ;

hence X is Pythagorean_triple by A16, Def4; :: thesis: verum