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 & X = {a,b,c} ) by Def4;
set k = a gcd b;
A2: ( a gcd b divides a & 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 A3: ( a = 0 & b = 0 ) by A2, 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, A3, XCMPLX_1:6; :: thesis: verum

end;

end;

suppose A4: 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 gcd b) * (a gcd b) <> 0 by XCMPLX_1:6;
consider a' being Nat such that
A6: a = (a gcd b) * a' by A2, NAT_D:def 3;
consider b' being Nat such that
A7: b = (a gcd b) * b' by A2, NAT_D:def 3;
reconsider a' = a', b' = b' as Element of NAT by ORDINAL1:def 13;
c ^2 = ((a gcd b) ^2 ) * ((a' ^2 ) + (b' ^2 )) by A1, A6, A7;
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
A8: 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, A6, A7, A8;
then A9: (a' ^2 ) + (b' ^2 ) = c' ^2 by A5, XCMPLX_1:5;
(a gcd b) * (a' gcd b') = (a gcd b) * 1 by A6, A7, Th8;
then a' gcd b' = 1 by A4, XCMPLX_1:5;
then A10: ( a',b' are_relative_prime & b',a' are_relative_prime ) by INT_2:def 4;
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
A11: ( m <= n & a' = (n ^2 ) - (m ^2 ) & b' = (2 * m) * n & c' = (n ^2 ) + (m ^2 ) ) by A9, 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 A1, A6, A7, A8, A11; :: 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
A12: ( m <= n & b' = (n ^2 ) - (m ^2 ) & a' = (2 * m) * n & c' = (n ^2 ) + (m ^2 ) ) by A9, 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 A1, A6, A7, A8, A12, 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
A13: ( m <= n & X = {(k * ((n ^2 ) - (m ^2 ))),(k * ((2 * m) * n)),(k * ((n ^2 ) + (m ^2 )))} ) ;
m ^2 <= n ^2 by A13, SQUARE_1:77;
then reconsider a' = (n ^2 ) - (m ^2 ) as Element of NAT by INT_1:16, XREAL_1:50;
set b' = (2 * m) * n;
set c' = (n ^2 ) + (m ^2 );
set a = k * a';
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 A13, Def4; :: thesis: verum