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
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 n' being Element of NAT such that
A3:
c' + a' = 2 * n'
by ABIAN:def 2;
consider i being Integer such that
A4:
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 A4, XREAL_1:50;
then
i >= 0
by XREAL_1:70;
then reconsider m' = i as Element of NAT by INT_1:16;
consider k' being Element of NAT such that
A5:
b' = 2 * k'
by ABIAN:def 2;
A6:
n' - m' = a
by A3, A4;
A7:
n' + m' = c
by A3, A4;
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 A9:
(
p divides n' &
p divides m' )
;
:: thesis: contradiction
reconsider p =
p as
prime Element of
NAT by ORDINAL1:def 13;
p divides - m'
by A9, INT_2:14;
then A10:
p divides n' + (- m')
by A9, WSIERP_1:9;
then
p divides a * a
by A3, A4, NAT_D:9;
then A11:
p divides - (a * a)
by INT_2:14;
p divides c
by A7, A9, NAT_D:8;
then A12:
p divides c * c
by NAT_D:9;
b * b = (c * c) + (- (a * a))
by A1;
then
p divides b * b
by A11, A12, WSIERP_1:9;
then
p divides b
by NEWTON:98;
hence
contradiction
by A2, A3, A4, A10, Def2;
:: thesis: verum
end;
A13: n' * m' =
((c + a) / 2) * ((c - a) / 2)
by A3, A4
.=
(b / 2) ^2
by A1
.=
k' ^2
by A5
;
then A14:
( n' is square & m' is square )
by A8, Th1;
then consider n being Nat such that
A15:
n' = n ^2
by Def3;
consider m being Nat such that
A16:
m' = m ^2
by A14, 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 >= 0 & m ^2 <= n ^2 )
by A6, A15, A16, 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 A3, A4, A15, A16; :: thesis: ( b = (2 * m) * n & c = (n ^2 ) + (m ^2 ) )
b ^2 =
(2 ^2 ) * ((n * m) ^2 )
by A5, A13, A15, A16, 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 A3, A4, A15, A16; :: thesis: verum