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) * n)),(0 * ((n ^2) + ()))} )

take 0 ; :: thesis: ( 0 <= 0 & X = {(0 * (() - ())),(0 * ((2 * 0) * 0)),(0 * (() + ()))} )
thus ( 0 <= 0 & X = {(0 * (() - ())),(0 * ((2 * 0) * 0)),(0 * (() + ()))} ) by ; :: 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 ;
consider b9 being Nat such that
A9: b = (a gcd b) * b9 by ;
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 ;
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 ;
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 ;
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 ;
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 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
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)))} ) ; :: thesis:
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 ;
then reconsider a9 = (n ^2) - (m ^2) as Element of NAT by ;
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 ; :: thesis: verum