:: by Freek Wiedijk

::

:: Received August 26, 2001

:: Copyright (c) 2001-2018 Association of Mizar Users

definition

let m, n be Nat;

( m,n are_coprime iff for k being Nat st k divides m & k divides n holds

k = 1 )

end;
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 for k being Nat st k divides m & k divides n holds

k = 1;

( m,n are_coprime iff for k being Nat st k divides m & k divides n holds

k = 1 )

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

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;

( m,n are_coprime iff for p being prime Nat holds

( not p divides m or not p divides n ) )

end;
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 for p being prime Nat holds

( not p divides m or not p divides n );

( m,n are_coprime iff for p being prime Nat holds

( not p divides m or not p divides n ) )

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

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

for n being Number holds

( n is square iff ex m being Nat st n = m ^2 );

registration

ex b_{1} being Element of NAT st

( b_{1} is even & b_{1} is square )
end;

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

( b

proof end;

registration

ex b_{1} being Element of NAT st

( b_{1} is odd & b_{1} is square )
end;

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

( b

proof end;

registration
end;

registration
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 )

( m is square & n is square )

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

( n >= m & n in X ) ) holds

X is infinite

proof end;

theorem :: PYTHTRIP:10

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

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

definition

ex b_{1} being Subset of NAT ex a, b, c being Element of NAT st

( (a ^2) + (b ^2) = c ^2 & b_{1} = {a,b,c} )
end;

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 a, b, c being Element of NAT st

( (a ^2) + (b ^2) = c ^2 & it = {a,b,c} );

ex b

( (a ^2) + (b ^2) = c ^2 & b

proof end;

:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :

for b_{1} being Subset of NAT holds

( b_{1} is Pythagorean_triple iff ex a, b, c being Element of NAT st

( (a ^2) + (b ^2) = c ^2 & b_{1} = {a,b,c} ) );

for b

( b

( (a ^2) + (b ^2) = c ^2 & b

definition

for b_{1} being Subset of NAT holds

( b_{1} is Pythagorean_triple iff ex k, m, n being Element of NAT st

( m <= n & b_{1} = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) )
end;

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

for b

( b

( m <= n & b

proof end;

:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :

for b_{1} being Subset of NAT holds

( b_{1} is Pythagorean_triple iff ex k, m, n being Element of NAT st

( m <= n & b_{1} = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) );

for b

( b

( m <= n & b

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 )

ex X being Pythagorean_triple st

( not X is degenerate & n in X )

proof end;

definition

let X be Pythagorean_triple ;

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

for k being Element of NAT st ( for n being Element of NAT st n in X holds

k divides n ) holds

k = 1;

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

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 ;

( X is simplified iff ex m, n being Element of NAT st

( m in X & n in X & m,n are_coprime ) )

end;
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 ex m, n being Element of NAT st

( m in X & n in X & m,n are_coprime );

( X is simplified iff ex m, n being Element of NAT st

( m in X & n in X & m,n are_coprime ) )

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

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 )

ex X being Pythagorean_triple st

( not X is degenerate & X is simplified & 4 * n in X )

proof end;

registration

existence

ex b_{1} being Pythagorean_triple st

( not b_{1} is degenerate & b_{1} is simplified )

end;
ex b

( not b

proof end;

theorem :: PYTHTRIP:16

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

proof end;