:: Pythagorean triples
:: by Freek Wiedijk
::
:: Received August 26, 2001
:: Copyright (c) 2001-2011 Association of Mizar Users


begin

definition
let m, n be Nat;
redefine pred m,n are_relative_prime means :Def1: :: PYTHTRIP:def 1
for k being Nat st k divides m & k divides n holds
k = 1;
compatibility
( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds
k = 1 )
proof end;
end;

:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def 1 :
for m, n being Nat holds
( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds
k = 1 );

definition
let m, n be Nat;
redefine pred m,n are_relative_prime means :Def2: :: PYTHTRIP:def 2
for p being prime Nat holds
( not p divides m or not p divides n );
compatibility
( m,n are_relative_prime iff for p being prime Nat holds
( not p divides m or not p divides n ) )
proof end;
end;

:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def 2 :
for m, n being Nat holds
( m,n are_relative_prime iff for p being prime Nat holds
( not p divides m or not p divides n ) );

begin

definition
let n be number ;
attr n is square means :Def3: :: PYTHTRIP:def 3
ex m being Nat st n = m ^2 ;
end;

:: deftheorem Def3 defines square PYTHTRIP:def 3 :
for n being number holds
( n is square iff ex m being Nat st n = m ^2 );

registration
cluster square -> natural set ;
coherence
for b1 being number st b1 is square holds
b1 is natural
proof end;
end;

registration
let n be Nat;
cluster n ^2 -> square ;
coherence
n ^2 is square
by Def3;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural V21() V22() integer ext-real non negative even square Element of NAT ;
existence
ex b1 being Element of NAT st
( b1 is even & b1 is square )
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal natural V21() V22() integer ext-real non negative odd square Element of NAT ;
existence
ex b1 being Element of NAT st
( not b1 is even & b1 is square )
proof end;
end;

registration
cluster V21() V22() integer ext-real even square set ;
existence
ex b1 being Integer st
( b1 is even & b1 is square )
proof end;
end;

registration
cluster V21() V22() integer ext-real odd square set ;
existence
ex b1 being Integer st
( not b1 is even & b1 is square )
proof end;
end;

registration
let m, n be square number ;
cluster m * n -> square ;
coherence
m * n is square
proof end;
end;

theorem Th1: :: PYTHTRIP:1
for m, n being Element of NAT st m * n is square & m,n are_relative_prime holds
( m is square & n is square )
proof end;

registration
let i be Integer;
cluster i ^2 -> integer ;
coherence
i ^2 is integer
;
end;

registration
let i be even Integer;
cluster i ^2 -> even ;
coherence
i ^2 is even
;
end;

registration
let i be odd Integer;
cluster i ^2 -> odd ;
coherence
not i ^2 is even
;
end;

theorem :: PYTHTRIP:2
for i being Integer holds
( i is even iff i ^2 is even ) ;

theorem Th3: :: PYTHTRIP:3
for i being Integer st i is even holds
(i ^2) mod 4 = 0
proof end;

theorem Th4: :: PYTHTRIP:4
for i being Integer st not i is even holds
(i ^2) mod 4 = 1
proof end;

registration
let m, n be odd square Integer;
cluster m + n -> non square ;
coherence
not m + n is square
proof end;
end;

theorem Th5: :: PYTHTRIP:5
for m, n being Element of NAT st m ^2 = n ^2 holds
m = n
proof end;

theorem Th6: :: PYTHTRIP:6
for m, n being Element of NAT holds
( m divides n iff m ^2 divides n ^2 )
proof end;

begin

theorem Th7: :: PYTHTRIP:7
for m, n, k being Element of NAT holds
( ( m divides n or k = 0 ) iff k * m divides k * n )
proof end;

theorem Th8: :: PYTHTRIP:8
for k, m, n being Element of NAT holds (k * m) gcd (k * n) = k * (m gcd n)
proof end;

begin

theorem Th9: :: PYTHTRIP:9
for X being set st ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) holds
not X is finite
proof end;

begin

theorem Th10: :: PYTHTRIP:10
for a, b being Element of NAT holds
( not a,b are_relative_prime or not a is even or not b is even )
proof end;

theorem Th11: :: PYTHTRIP:11
for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & not a is even holds
ex m, n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )
proof end;

theorem :: PYTHTRIP:12
for a, n, m, b, c being Element of NAT st a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) holds
(a ^2) + (b ^2) = c ^2 ;

definition
mode Pythagorean_triple -> Subset of NAT means :Def4: :: PYTHTRIP:def 4
ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & it = {a,b,c} );
existence
ex b1 being Subset of NAT ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} )
proof end;
end;

:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) );

registration
cluster -> finite Pythagorean_triple ;
coherence
for b1 being Pythagorean_triple holds b1 is finite
proof end;
end;

definition
redefine mode Pythagorean_triple means :Def5: :: PYTHTRIP:def 5
ex k, m, n being Element of NAT st
( m <= n & it = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} );
compatibility
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) )
proof end;
end;

:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) );

definition
let X be Pythagorean_triple ;
attr X is degenerate means :Def6: :: PYTHTRIP:def 6
0 in X;
end;

:: deftheorem Def6 defines degenerate PYTHTRIP:def 6 :
for X being Pythagorean_triple holds
( X is degenerate iff 0 in X );

theorem :: PYTHTRIP:13
for n being Element of NAT st n > 2 holds
ex X being Pythagorean_triple st
( not X is degenerate & n in X )
proof end;

definition
let X be Pythagorean_triple ;
attr X is simplified means :Def7: :: PYTHTRIP:def 7
for k being Element of NAT st ( for n being Element of NAT st n in X holds
k divides n ) holds
k = 1;
end;

:: deftheorem Def7 defines simplified PYTHTRIP:def 7 :
for X being Pythagorean_triple holds
( X is simplified iff for k being Element of NAT st ( for n being Element of NAT st n in X holds
k divides n ) holds
k = 1 );

definition
let X be Pythagorean_triple ;
redefine attr X is simplified means :Def8: :: PYTHTRIP:def 8
ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime );
compatibility
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) )
proof end;
end;

:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :
for X being Pythagorean_triple holds
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) );

theorem Th14: :: PYTHTRIP:14
for n being Element of NAT st n > 0 holds
ex X being Pythagorean_triple st
( not X is degenerate & X is simplified & 4 * n in X )
proof end;

registration
cluster finite non degenerate simplified Pythagorean_triple ;
existence
ex b1 being Pythagorean_triple st
( not b1 is degenerate & b1 is simplified )
proof end;
end;

theorem :: PYTHTRIP:15
{3,4,5} is non degenerate simplified Pythagorean_triple
proof end;

theorem :: PYTHTRIP:16
not { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is finite
proof end;