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

definition

let m, n be Nat;

redefine pred m,n are_coprime means :: PYTHTRIP:def 1
for k being Nat st k divides m & k divides n holds
k = 1;

compatibility
( m,n are_coprime iff for k being Nat st k divides m & k divides n holds
k = 1 )

proof end;

end;

:: deftheorem defines are_coprime PYTHTRIP:def 1 :
for m, n being Nat holds
( m,n are_coprime 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_coprime means :: PYTHTRIP:def 2
for p being prime Nat holds
( not p divides m or not p divides n );

compatibility
( m,n are_coprime iff for p being prime Nat holds
( not p divides m or not p divides n ) )

proof end;

end;

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

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 for object ;

coherence
for b₁ being Number st b₁ is square holds
b₁ is natural ;

end;

registration

let n be Nat;

cluster n ^2 -> square ;

coherence
n ^2 is square ;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal natural V27() ext-real non negative V38() integer dim-like even square for 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 V27() ext-real non negative V38() integer dim-like odd square for Element of NAT ;

existence
ex b₁ being Element of NAT st
( b₁ is odd & b₁ is square )

proof end;

end;

registration

cluster V27() ext-real V38() integer even square for object ;

existence
ex b₁ being Integer st
( b₁ is even & b₁ is square )

proof end;

end;

registration

cluster V27() ext-real V38() integer odd square for object ;

existence
ex b₁ being Integer st
( b₁ is odd & b₁ is square )

proof end;

end;

registration

let m, n be square object ;

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_coprime 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 i is odd 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;

theorem Th7: :: PYTHTRIP:7

for k, m, n 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;

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
X is infinite

proof end;

theorem :: PYTHTRIP:10

for a, b being Element of NAT holds
( not a,b are_coprime or a is odd or b is odd ) ;

theorem Th11: :: PYTHTRIP:11

for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_coprime & a is odd 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, b, c, m, n 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 for Pythagorean_triple ;

coherence
for b₁ being Pythagorean_triple holds b₁ is finite

proof end;

end;

definition

:: Formula for Pythagorean Triples

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)))} ) );

notation

let X be Pythagorean_triple ;
synonym degenerate X for with_zero ;

end;

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 :: 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 PYTHTRIP:def 6 :
canceled;

:: deftheorem 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_coprime );

compatibility
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_coprime ) )

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_coprime ) );

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 non degenerate finite simplified for 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

{ X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite

proof end;