:: 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 b₁ being number st b₁ is square holds
b₁ 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 b₁ being Element of NAT st
( b₁ is even & b₁ 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 b₁ being Element of NAT st
( not b₁ is even & b₁ is square )

proof end;

end;

registration

cluster V21() V22() integer ext-real even square set ;
existence
ex b₁ being Integer st
( b₁ is even & b₁ is square )

proof end;

end;

registration

cluster V21() V22() integer ext-real odd square set ;
existence
ex b₁ being Integer st
( not b₁ is even & b₁ 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 b₁ being Subset of NAT ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b₁ = {a,b,c} )

proof end;

end;

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

registration

cluster -> finite Pythagorean_triple ;
coherence
for b₁ being Pythagorean_triple holds b₁ 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 b₁ being Subset of NAT holds
( b₁ is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b₁ = {(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 b₁ being Subset of NAT holds
( b₁ is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b₁ = {(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 b₁ being Pythagorean_triple st
( not b₁ is degenerate & b₁ 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;