let a, b, c be Nat; :: thesis: ( (a ^2) + (b ^2) = c ^2 & a,b are_coprime & a is odd 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_coprime or not a is odd 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_coprime ; :: thesis: ( not a is odd 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 a is odd ; :: 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 a9 = a as odd Nat ;
b is even

proof

assume b is odd ; :: thesis: contradiction
then reconsider b9 = b as odd Nat ;
(a9 ^2) + (b9 ^2) = c ^2 by A1;
hence contradiction ; :: thesis: verum

end;

then reconsider b9 = b as even Nat ;
(a9 ^2) + (b9 ^2) = c ^2 by A1;
then reconsider c9 = c as odd Nat ;
2 divides c9 - a9 by ABIAN:def 1;
then consider i being Integer such that
A3: c9 - a9 = 2 * i ;
c ^2 >= (a ^2) + 0 by A1, XREAL_1:6;
then c >= a by SQUARE_1:16;
then 2 * i >= 2 * 0 by A3, XREAL_1:48;
then i >= 0 by XREAL_1:68;
then reconsider m9 = i as Element of NAT by INT_1:3;
consider n9 being Nat such that
A4: c9 + a9 = 2 * n9 by ABIAN:def 2;
consider k9 being Nat such that
A5: b9 = 2 * k9 by ABIAN:def 2;
reconsider n9 = n9, k9 = k9 as Element of NAT by ORDINAL1:def 12;
A6: n9 * m9 = ((c + a) / 2) * ((c - a) / 2) by A4, A3
.= (b / 2) ^2 by A1
.= k9 ^2 by A5 ;
A7: n9 + m9 = c by A4, A3;
A8: n9,m9 are_coprime

proof

let p be Prime; :: according to PYTHTRIP:def 2 :: thesis: ( not p divides n9 or not p divides m9 )
assume that
A9: p divides n9 and
A10: p divides m9 ; :: thesis: contradiction
reconsider p = p as prime Element of NAT by ORDINAL1:def 12;
p divides c by A7, A9, A10, NAT_D:8;
then A11: p divides c * c by NAT_D:9;
p divides - m9 by A10, INT_2:10;
then A12: p divides n9 + (- m9) by A9, WSIERP_1:4;
then p divides a * a by A4, A3, NAT_D:9;
then A13: p divides - (a * a) by INT_2:10;
b * b = (c * c) + (- (a * a)) by A1;
then p divides b * b by A13, A11, WSIERP_1:4;
then p divides b by NEWTON:80;
hence contradiction by A2, A4, A3, A12; :: thesis: verum

end;

then n9 is square by A6, Th1;
then consider n being Nat such that
A14: n9 = n ^2 ;
m9 is square by A8, A6, Th1;
then consider m being Nat such that
A15: m9 = m ^2 ;
reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;
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) )
n9 - m9 = a by A4, A3;
then m ^2 <= n ^2 by A14, A15, XREAL_1:49;
hence m <= n by SQUARE_1:16; :: 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:9
.= ((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