:: INT_2 semantic presentation

definition

let c₁ be integer number ;
redefine func abs as abs c₁ -> Nat;
coherence

proof end;

end;

theorem Th1: :: INT_2:1

canceled;

theorem Th2: :: INT_2:2

canceled;

theorem Th3: :: INT_2:3

for b₁ being Nat holds
( 0 divides b₁ iff b₁ = 0 )

proof end;

theorem Th4: :: INT_2:4

for b₁, b₂ being Nat holds
( ( b₁ = 0 or b₂ = 0 ) iff b₁ lcm b₂ = 0 )

proof end;

theorem Th5: :: INT_2:5

for b₁, b₂ being Nat holds
( ( b₁ = 0 & b₂ = 0 ) iff b₁ hcf b₂ = 0 )

proof end;

theorem Th6: :: INT_2:6

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

proof end;

theorem Th7: :: INT_2:7

canceled;

theorem Th8: :: INT_2:8

for b₁ being Nat holds
( - b₁ is Nat iff b₁ = 0 )

proof end;

theorem Th9: :: INT_2:9

- 1 is not Nat by Th8;

theorem Th10: :: INT_2:10

for b₁ being Integer holds
( 0 divides b₁ iff b₁ = 0 )

proof end;

theorem Th11: :: INT_2:11

for b₁ being Integer holds
( b₁ divides - b₁ & - b₁ divides b₁ )

proof end;

theorem Th12: :: INT_2:12

for b₁, b₂, b₃ being Integer st b₁ divides b₂ holds
b₁ divides b₂ * b₃

proof end;

theorem Th13: :: INT_2:13

for b₁, b₂, b₃ being Integer st b₁ divides b₂ & b₂ divides b₃ holds
b₁ divides b₃

proof end;

theorem Th14: :: INT_2:14

for b₁, b₂ being Integer holds
( ( b₁ divides b₂ implies b₁ divides - b₂ ) & ( b₁ divides - b₂ implies b₁ divides b₂ ) & ( b₁ divides b₂ implies - b₁ divides b₂ ) & ( - b₁ divides b₂ implies b₁ divides b₂ ) & ( b₁ divides b₂ implies - b₁ divides - b₂ ) & ( - b₁ divides - b₂ implies b₁ divides b₂ ) & ( b₁ divides - b₂ implies - b₁ divides b₂ ) & ( - b₁ divides b₂ implies b₁ divides - b₂ ) )

proof end;

theorem Th15: :: INT_2:15

for b₁, b₂ being Integer st b₁ divides b₂ & b₂ divides b₁ & not b₁ = b₂ holds
b₁ = - b₂

proof end;

theorem Th16: :: INT_2:16

for b₁ being Integer holds
( b₁ divides 0 & 1 divides b₁ & - 1 divides b₁ )

proof end;

theorem Th17: :: INT_2:17

for b₁ being Integer holds
( ( not b₁ divides 1 & not b₁ divides - 1 ) or b₁ = 1 or b₁ = - 1 )

proof end;

theorem Th18: :: INT_2:18

for b₁ being Integer st ( b₁ = 1 or b₁ = - 1 ) holds
( b₁ divides 1 & b₁ divides - 1 ) by Th16;

theorem Th19: :: INT_2:19

for b₁, b₂, b₃ being Integer holds
( b₁,b₂ are_congruent_mod b₃ iff b₃ divides b₁ - b₂ )

proof end;

theorem Th20: :: INT_2:20

for b₁ being Integer holds abs b₁ is Nat ;

theorem Th21: :: INT_2:21

for b₁, b₂ being Integer holds
( b₁ divides b₂ iff abs b₁ divides abs b₂ )

proof end;

definition

let c₁, c₂ be Integer;
canceled;
func c₁ lcm' c₂ -> Integer equals :: INT_2:def 2
(abs a₁) lcm (abs a₂);
coherence ;
commutativity ;

end;

:: deftheorem Def1 INT_2:def 1 :

:: deftheorem Def2 defines lcm' INT_2:def 2 :

theorem Th22: :: INT_2:22

canceled;

theorem Th23: :: INT_2:23

for b₁, b₂ being Integer holds b₁ lcm' b₂ is Nat ;

theorem Th24: :: INT_2:24

canceled;

theorem Th25: :: INT_2:25

for b₁, b₂ being Integer holds b₁ divides b₁ lcm' b₂

proof end;

theorem Th26: :: INT_2:26

for b₁, b₂ being Integer holds b₁ divides b₂ lcm' b₁ by Th25;

theorem Th27: :: INT_2:27

for b₁, b₂, b₃ being Integer st b₁ divides b₃ & b₂ divides b₃ holds
b₁ lcm' b₂ divides b₃

proof end;

definition

let c₁, c₂ be Integer;
func c₁ gcd c₂ -> Integer equals :: INT_2:def 3
(abs a₁) hcf (abs a₂);
coherence ;
commutativity ;

end;

:: deftheorem Def3 defines gcd INT_2:def 3 :

theorem Th28: :: INT_2:28

canceled;

theorem Th29: :: INT_2:29

for b₁, b₂ being Integer holds b₁ gcd b₂ is Nat ;

theorem Th30: :: INT_2:30

canceled;

theorem Th31: :: INT_2:31

for b₁, b₂ being Integer holds b₁ gcd b₂ divides b₁

proof end;

theorem Th32: :: INT_2:32

for b₁, b₂ being Integer holds b₁ gcd b₂ divides b₂ by Th31;

theorem Th33: :: INT_2:33

for b₁, b₂, b₃ being Integer st b₃ divides b₁ & b₃ divides b₂ holds
b₃ divides b₁ gcd b₂

proof end;

theorem Th34: :: INT_2:34

for b₁, b₂ being Integer holds
( ( b₁ = 0 or b₂ = 0 ) iff b₁ lcm' b₂ = 0 )

proof end;

theorem Th35: :: INT_2:35

for b₁, b₂ being Integer holds
( ( b₁ = 0 & b₂ = 0 ) iff b₁ gcd b₂ = 0 )

proof end;

definition

let c₁, c₂ be Integer;
pred c₁,c₂ are_relative_prime means :Def4: :: INT_2:def 4
a₁ gcd a₂ = 1;
symmetry ;

end;

:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :

theorem Th36: :: INT_2:36

canceled;

theorem Th37: :: INT_2:37

canceled;

theorem Th38: :: INT_2:38

for b₁, b₂ being Integer st ( b₁ <> 0 or b₂ <> 0 ) holds
ex b₃, b₄ being Integer st
( b₁ = (b₁ gcd b₂) * b₃ & b₂ = (b₁ gcd b₂) * b₄ & b₃,b₄ are_relative_prime )

proof end;

theorem Th39: :: INT_2:39

for b₁, b₂, b₃ being Integer st b₁,b₂ are_relative_prime holds
( (b₃ * b₁) gcd (b₃ * b₂) = abs b₃ & (b₃ * b₁) gcd (b₂ * b₃) = abs b₃ & (b₁ * b₃) gcd (b₃ * b₂) = abs b₃ & (b₁ * b₃) gcd (b₂ * b₃) = abs b₃ )

proof end;

theorem Th40: :: INT_2:40

for b₁, b₂, b₃ being Integer st b₁ divides b₂ * b₃ & b₂,b₁ are_relative_prime holds
b₁ divides b₃

proof end;

theorem Th41: :: INT_2:41

for b₁, b₂, b₃ being Integer st b₁,b₂ are_relative_prime & b₃,b₂ are_relative_prime holds
b₁ * b₃,b₂ are_relative_prime

proof end;

definition

let c₁ be Nat;
attr a₁ is prime means :Def5: :: INT_2:def 5
( a₁ > 1 & ( for b₁ being Nat holds
( not b₁ divides a₁ or b₁ = 1 or b₁ = a₁ ) ) );

end;

:: deftheorem Def5 defines prime INT_2:def 5 :

definition

let c₁, c₂ be Nat;
pred c₁,c₂ are_relative_prime means :Def6: :: INT_2:def 6
a₁ hcf a₂ = 1;
symmetry ;

end;

:: deftheorem Def6 defines are_relative_prime INT_2:def 6 :

theorem Th42: :: INT_2:42

canceled;

theorem Th43: :: INT_2:43

canceled;

theorem Th44: :: INT_2:44

2 is prime

proof end;

theorem Th45: :: INT_2:45

canceled;

theorem Th46: :: INT_2:46

not 4 is prime

proof end;

theorem Th47: :: INT_2:47

for b₁, b₂ being Nat st b₁ is prime & b₂ is prime & not b₁,b₂ are_relative_prime holds
b₁ = b₂

proof end;

scheme :: INT_2:sch 1
s1{ F₁() -> Nat, P₁[ Nat] } :

for b₁ being Nat st b₁ >= F₁() holds
P₁[b₁]

provided

E23: P₁[F₁()] and
E24: for b₁ being Nat st b₁ >= F₁() & P₁[b₁] holds
P₁[b₁ + 1]

proof end;

scheme :: INT_2:sch 2
s2{ F₁() -> Nat, P₁[ Nat] } :

for b₁ being Nat st b₁ >= F₁() holds
P₁[b₁]

provided

E23: for b₁ being Nat st b₁ >= F₁() & ( for b₂ being Nat st b₂ >= F₁() & b₂ < b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

theorem Th48: :: INT_2:48

for b₁ being Nat st b₁ >= 2 holds
ex b₂ being Nat st
( b₂ is prime & b₂ divides b₁ )

proof end;