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, INT_2:3;
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 a' being Nat such that
A8: a = (a gcd b) * a' by A3, NAT_D:def 3;
consider b' being Nat such that
A9: b = (a gcd b) * b' by A4, NAT_D:def 3;
reconsider a' = a', b' = b' as Element of NAT by ORDINAL1:def 13;
(a gcd b) * (a' gcd b') = (a gcd b) * 1 by A8, A9, Th8;
then a' gcd b' = 1 by A6, XCMPLX_1:5;
then A10: a',b' are_relative_prime by INT_2:def 4;
c ^2 = ((a gcd b) ^2 ) * ((a' ^2 ) + (b' ^2 )) by A1, A8, A9;
then (a gcd b) ^2 divides c ^2 by NAT_D:def 3;
then a gcd b divides c by Th6;
then consider c' being Nat such that
A11: c = (a gcd b) * c' by NAT_D:def 3;
reconsider c' = c' as Element of NAT by ORDINAL1:def 13;
((a gcd b) ^2 ) * ((a' ^2 ) + (b' ^2 )) = ((a gcd b) ^2 ) * (c' ^2 ) by A1, A8, A9, A11;
then A12: (a' ^2 ) + (b' ^2 ) = c' ^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 ( not a' is even or not b' is even ) by A10, Th10;

suppose not a' is even ; :: 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 & a' = (n ^2 ) - (m ^2 ) & b' = (2 * m) * n & c' = (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 not b' is even ; :: 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 & b' = (n ^2 ) - (m ^2 ) & a' = (2 * m) * n & c' = (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:99; :: 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: 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:77;
then reconsider a' = (n ^2 ) - (m ^2 ) as Element of NAT by INT_1:16, XREAL_1:50;
set a = k * a';
set c' = (n ^2 ) + (m ^2 );
set b' = (2 * m) * n;
set b = k * ((2 * m) * n);
set c = k * ((n ^2 ) + (m ^2 ));
((k * a') ^2 ) + ((k * ((2 * m) * n)) ^2 ) = (k * ((n ^2 ) + (m ^2 ))) ^2 ;
hence X is Pythagorean_triple by A16, Def4; :: thesis: verum