let a, b, c be Element of NAT ; :: thesis: ( (a ^2 ) + (b ^2 ) = c ^2 & a,b are_relative_prime & not a is even implies ex m, n being Element of NAT st
( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) ) )
assume A1: (a ^2 ) + (b ^2 ) = c ^2 ; :: thesis: ( not a,b are_relative_prime or a is even or ex m, n being Element of NAT st
( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) ) )
assume A2: a,b are_relative_prime ; :: thesis: ( a is even or ex m, n being Element of NAT st
( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) ) )
assume not a is even ; :: thesis: ex m, n being Element of NAT st
( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
then reconsider a' = a as odd Element of NAT ;
b is even

proof

assume not b is even ; :: thesis: contradiction
then reconsider b' = b as odd Element of NAT ;
(a' ^2 ) + (b' ^2 ) = c ^2 by A1;
hence contradiction ; :: thesis: verum

end;

then reconsider b' = b as even Element of NAT ;
(a' ^2 ) + (b' ^2 ) = c ^2 by A1;
then reconsider c' = c as odd Element of NAT ;
consider i being Integer such that
A3: c' - a' = 2 * i by ABIAN:def 1;
c ^2 >= (a ^2 ) + 0 by A1, XREAL_1:8;
then c >= a by SQUARE_1:78;
then 2 * i >= 2 * 0 by A3, XREAL_1:50;
then i >= 0 by XREAL_1:70;
then reconsider m' = i as Element of NAT by INT_1:16;
consider n' being Element of NAT such that
A4: c' + a' = 2 * n' by ABIAN:def 2;
consider k' being Element of NAT such that
A5: b' = 2 * k' by ABIAN:def 2;
A6: n' * m' = ((c + a) / 2) * ((c - a) / 2) by A4, A3
.= (b / 2) ^2 by A1
.= k' ^2 by A5 ;
A7: n' + m' = c by A4, A3;
A8: n',m' are_relative_prime

proof

let p be prime Nat; :: according to PYTHTRIP:def 2 :: thesis: ( not p divides n' or not p divides m' )
assume that
A9: p divides n' and
A10: p divides m' ; :: thesis: contradiction
reconsider p = p as prime Element of NAT by ORDINAL1:def 13;
p divides c by A7, A9, A10, NAT_D:8;
then A11: p divides c * c by NAT_D:9;
p divides - m' by A10, INT_2:14;
then A12: p divides n' + (- m') by A9, WSIERP_1:9;
then p divides a * a by A4, A3, NAT_D:9;
then A13: p divides - (a * a) by INT_2:14;
b * b = (c * c) + (- (a * a)) by A1;
then p divides b * b by A13, A11, WSIERP_1:9;
then p divides b by NEWTON:98;
hence contradiction by A2, A4, A3, A12, Def2; :: thesis: verum

end;

then n' is square by A6, Th1;
then consider n being Nat such that
A14: n' = n ^2 by Def3;
m' is square by A8, A6, Th1;
then consider m being Nat such that
A15: m' = m ^2 by Def3;
reconsider m = m, n = n as Element of NAT by ORDINAL1:def 13;
take m ; :: thesis: ex n being Element of NAT st
( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
take n ; :: thesis: ( m <= n & a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
n' - m' = a by A4, A3;
then m ^2 <= n ^2 by A14, A15, XREAL_1:51;
hence m <= n by SQUARE_1:78; :: thesis: ( a = (n ^2 ) - (m ^2 ) & b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
thus a = (n ^2 ) - (m ^2 ) by A4, A3, A14, A15; :: thesis: ( b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
b ^2 = (2 ^2 ) * ((n * m) ^2 ) by A5, A6, A14, A15, SQUARE_1:68
.= ((2 * m) * n) ^2 ;
hence b = (2 * m) * n by Th5; :: thesis: c = (n ^2 ) + (m ^2 )
thus c = (n ^2 ) + (m ^2 ) by A4, A3, A14, A15; :: thesis: verum