:: PYTHTRIP semantic presentation

definition

let c₁, c₂ be Nat;
redefine pred c₁,c₂ are_relative_prime means :Def1: :: PYTHTRIP:def 1
for b₁ being Nat st b₁ divides a₁ & b₁ divides a₂ holds
b₁ = 1;
compatibility

proof end;

end;

:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def 1 :

definition

let c₁, c₂ be Nat;
redefine pred c₁,c₂ are_relative_prime means :Def2: :: PYTHTRIP:def 2
for b₁ being prime Nat holds
( not b₁ divides a₁ or not b₁ divides a₂ );
compatibility

proof end;

end;

:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def 2 :

definition

let c₁ be number ;
attr a₁ is square means :Def3: :: PYTHTRIP:def 3
ex b₁ being Nat st a₁ = b₁ ^2 ;

end;

:: deftheorem Def3 defines square PYTHTRIP:def 3 :

registration

cluster square -> natural set ;
coherence

proof end;

end;

registration

let c₁ be Nat;
cluster a₁ ^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 c₁, c₂ be square number ;
cluster a₁ * a₂ -> natural square ;
coherence

proof end;

end;

theorem Th1: :: PYTHTRIP:1

for b₁, b₂ being Nat st b₁ * b₂ is square & b₁,b₂ are_relative_prime holds
( b₁ is square & b₂ is square )

proof end;

registration

let c₁ be even Integer;
cluster a₁ ^2 -> even ;
coherence ;

end;

registration

let c₁ be odd Integer;
cluster a₁ ^2 -> odd ;
coherence ;

end;

theorem Th2: :: PYTHTRIP:2

for b₁ being Integer holds
( b₁ is even iff b₁ ^2 is even )

proof end;

theorem Th3: :: PYTHTRIP:3

for b₁ being Integer st b₁ is even holds
(b₁ ^2 ) mod 4 = 0

proof end;

theorem Th4: :: PYTHTRIP:4

for b₁ being Integer st not b₁ is even holds
(b₁ ^2 ) mod 4 = 1

proof end;

registration

let c₁, c₂ be odd square number ;
cluster a₁ + a₂ -> non square ;
coherence

proof end;

end;

theorem Th5: :: PYTHTRIP:5

for b₁, b₂ being Nat st b₁ ^2 = b₂ ^2 holds
b₁ = b₂

proof end;

theorem Th6: :: PYTHTRIP:6

for b₁, b₂ being Nat holds
( b₁ divides b₂ iff b₁ ^2 divides b₂ ^2 )

proof end;

theorem Th7: :: PYTHTRIP:7

for b₁, b₂, b₃ being Nat holds
( ( b₁ divides b₂ or b₃ = 0 ) iff b₃ * b₁ divides b₃ * b₂ )

proof end;

theorem Th8: :: PYTHTRIP:8

for b₁, b₂, b₃ being Nat holds (b₁ * b₂) hcf (b₁ * b₃) = b₁ * (b₂ hcf b₃)

proof end;

theorem Th9: :: PYTHTRIP:9

for b₁ being set st ( for b₂ being Nat ex b₃ being Nat st
( b₃ >= b₂ & b₃ in b₁ ) ) holds
not b₁ is finite

proof end;

theorem Th10: :: PYTHTRIP:10

for b₁, b₂ being Nat holds
( not b₁,b₂ are_relative_prime or not b₁ is even or not b₂ is even )

proof end;

theorem Th11: :: PYTHTRIP:11

for b₁, b₂, b₃ being Nat st (b₁ ^2 ) + (b₂ ^2 ) = b₃ ^2 & b₁,b₂ are_relative_prime & not b₁ is even holds
ex b₄, b₅ being Nat st
( b₄ <= b₅ & b₁ = (b₅ ^2 ) - (b₄ ^2 ) & b₂ = (2 * b₄) * b₅ & b₃ = (b₅ ^2 ) + (b₄ ^2 ) )

proof end;

theorem Th12: :: PYTHTRIP:12

for b₁, b₂, b₃, b₄, b₅ being Nat st b₁ = (b₂ ^2 ) - (b₃ ^2 ) & b₄ = (2 * b₃) * b₂ & b₅ = (b₂ ^2 ) + (b₃ ^2 ) holds
(b₁ ^2 ) + (b₄ ^2 ) = b₅ ^2 ;

definition

mode Pythagorean_triple -> Subset of NAT means :Def4: :: PYTHTRIP:def 4
ex b₁, b₂, b₃ being Nat st
( (b₁ ^2 ) + (b₂ ^2 ) = b₃ ^2 & a₁ = {b₁,b₂,b₃} );
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 -> Subset of NAT means :Def5: :: PYTHTRIP:def 5
ex b₁, b₂, b₃ being Nat st
( b₂ <= b₃ & a₁ = {(b₁ * ((b₃ ^2 ) - (b₂ ^2 ))),(b₁ * ((2 * b₂) * b₃)),(b₁ * ((b₃ ^2 ) + (b₂ ^2 )))} );
compatibility

proof end;

end;

:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def 5 :

definition

let c₁ be Pythagorean_triple ;
attr a₁ is degenerate means :Def6: :: PYTHTRIP:def 6
0 in a₁;

end;

:: deftheorem Def6 defines degenerate PYTHTRIP:def 6 :

theorem Th13: :: PYTHTRIP:13

for b₁ being Nat st b₁ > 2 holds
ex b₂ being Pythagorean_triple st
( not b₂ is degenerate & b₁ in b₂ )

proof end;

definition

let c₁ be Pythagorean_triple ;
attr a₁ is simplified means :Def7: :: PYTHTRIP:def 7
for b₁ being Nat st ( for b₂ being Nat st b₂ in a₁ holds
b₁ divides b₂ ) holds
b₁ = 1;

end;

:: deftheorem Def7 defines simplified PYTHTRIP:def 7 :

definition

let c₁ be Pythagorean_triple ;
redefine attr a₁ is simplified means :Def8: :: PYTHTRIP:def 8
ex b₁, b₂ being Nat st
( b₁ in a₁ & b₂ in a₁ & b₁,b₂ are_relative_prime );
compatibility

proof end;

end;

:: deftheorem Def8 defines simplified PYTHTRIP:def 8 :

theorem Th14: :: PYTHTRIP:14

for b₁ being Nat st b₁ > 0 holds
ex b₂ being Pythagorean_triple st
( not b₂ is degenerate & b₂ is simplified & 4 * b₁ in b₂ )

proof end;

registration

cluster finite non degenerate simplified Pythagorean_triple ;
existence

proof end;

end;

theorem Th15: :: PYTHTRIP:15

{3,4,5} is non degenerate simplified Pythagorean_triple

proof end;

theorem Th16: :: PYTHTRIP:16

not { b₁ where B is Pythagorean_triple : ( not b₁ is degenerate & b₁ is simplified ) } is finite

proof end;