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 a9 = a as odd Element of NAT ;
b is even

proof

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

end;

then reconsider b9 = b as even Element of NAT ;
(a9 ^2 ) + (b9 ^2 ) = c ^2 by A1;
then reconsider c9 = c as odd Element of NAT ;
2 divides c9 - a9 by ABIAN:def 1;
then consider i being Integer such that
A3: c9 - a9 = 2 * i by INT_1:def 9;
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 m9 = i as Element of NAT by INT_1:16;
consider n9 being Element of NAT such that
A4: c9 + a9 = 2 * n9 by ABIAN:def 2;
consider k9 being Element of NAT such that
A5: b9 = 2 * k9 by ABIAN:def 2;
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_relative_prime

proof

let p be prime Nat; :: 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 13;
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:14;
then A12: p divides n9 + (- m9) 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 n9 is square by A6, Th1;
then consider n being Nat such that
A14: n9 = n ^2 by Def3;
m9 is square by A8, A6, Th1;
then consider m being Nat such that
A15: m9 = 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 ) )
n9 - m9 = 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