:: PYTHTRIP semantic presentation

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

proof end;

end;

:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def 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

proof end;

end;

:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def 2 :

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 :

registration

cluster square -> natural set ;
coherence

proof end;

end;

registration

let n be Nat;
cluster n ^2 -> natural square ;
coherence by Def3;

end;

registration

cluster even square Element of NAT ;
existence

proof end;

end;

registration

cluster odd square Element of NAT ;
existence

proof end;

end;

registration

cluster natural even square set ;
existence

proof end;

end;

registration

cluster natural odd square set ;
existence

proof end;

end;

registration

let m, n be square number ;
cluster m * n -> natural square ;
coherence

proof end;

end;

theorem Th1: :: PYTHTRIP:1

for m, n being Nat st m * n is square & m,n are_relative_prime holds
( m is square & n is square )

proof end;

registration

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

end;

registration

let i be odd Integer;
cluster i ^2 -> odd ;
coherence ;

end;

theorem Th2: :: PYTHTRIP:2

for i being Integer holds
( i is even iff i ^2 is even )

proof end;

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 number ;
cluster m + n -> non square ;
coherence

proof end;

end;

theorem Th5: :: PYTHTRIP:5

for m, n being Nat st m ^2 = n ^2 holds
m = n

proof end;

theorem Th6: :: PYTHTRIP:6

for m, n being Nat holds
( m divides n iff m ^2 divides n ^2 )

proof end;

theorem Th7: :: PYTHTRIP:7

for m, n, k being 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 Nat holds (k * m) hcf (k * n) = k * (m hcf n)

proof end;

theorem Th9: :: PYTHTRIP:9

for X being set st ( for m being Nat ex n being Nat st
( n >= m & n in X ) ) holds
not X is finite

proof end;

theorem Th10: :: PYTHTRIP:10

for a, b being 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 Nat st (a ^2 ) + (b ^2 ) = c ^2 & a,b are_relative_prime & not a is even holds
ex m, n being 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 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 Nat st
( (a ^2 ) + (b ^2 ) = c ^2 & it = {a,b,c} );
existence

proof end;

end;

:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def 4 :

registration

cluster -> finite Pythagorean_triple ;
coherence

proof end;

end;

definition

redefine mode Pythagorean_triple means :Def5: :: PYTHTRIP:def 5
ex k, m, n being Nat st
( m <= n & it = {(k * ((n ^2 ) - (m ^2 ))),(k * ((2 * m) * n)),(k * ((n ^2 ) + (m ^2 )))} );
compatibility

proof end;

end;

:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :

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 :

theorem :: PYTHTRIP:13

for n being 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 Nat st ( for n being Nat st n in X holds
k divides n ) holds
k = 1;

end;

:: deftheorem Def7 defines simplified PYTHTRIP:def 7 :

definition

let X be Pythagorean_triple ;
redefine attr X is simplified means :Def8: :: PYTHTRIP:def 8
ex m, n being Nat st
( m in X & n in X & m,n are_relative_prime );
compatibility

proof end;

end;

:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :

theorem Th14: :: PYTHTRIP:14

for n being 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

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;