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)))} ) )

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 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;

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

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)))} )

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

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;

end;

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)))} )

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

proof

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

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)))} )

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;

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)))} )

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;

end;

end;

end;

end;

end;

given 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)))} ; :: thesis: X is Pythagorean_triple
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