let a, b, c be Element of 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 Element of NAT ;

b is even

(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 ;

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

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

( 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 Element of NAT ;

b is even

proof

then reconsider b9 = b as even Element of NAT ;
assume
b is odd
; :: 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 odd Element of NAT ;

(a9 ^2) + (b9 ^2) = c ^2 by A1;

hence contradiction ; :: thesis: verum

(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 ;

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

then
n9 is square
by A6, Th1;
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 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;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

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