:: Divisibility of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 3, 2007
:: Copyright (c) 2007 Association of Mizar Users

begin

Lm1: now

let k, l be Nat; :: thesis: k div l is Nat
k div l in NAT by INT_1:16, INT_1:82;
hence k div l is Nat ; :: thesis: verum

end;

Lm2: now

let k, l be Nat; :: thesis: k mod l is Nat
k mod l in NAT by INT_1:16, INT_1:84;
hence k mod l is Nat ; :: thesis: verum

end;

definition

let k, l be Nat;
:: original: div
redefine func k div l -> Nat means :Def1: :: NAT_D:def 1
( ex t being Nat st
( k = (l * it) + t & t < l ) or ( it = 0 & l = 0 ) );
compatibility
for b₁ being Nat holds
( b₁ = k div l iff ( ex t being Nat st
( k = (l * b₁) + t & t < l ) or ( b₁ = 0 & l = 0 ) ) )

proof end;

coherence
k div l is Nat by Lm1;

end;

:: deftheorem Def1 defines div NAT_D:def 1 :
for k, l, b₃ being Nat holds
( b₃ = k div l iff ( ex t being Nat st
( k = (l * b₃) + t & t < l ) or ( b₃ = 0 & l = 0 ) ) );

definition

let k, l be Nat;
:: original: mod
redefine func k mod l -> Nat means :Def2: :: NAT_D:def 2
( ex t being Nat st
( k = (l * t) + it & it < l ) or ( it = 0 & l = 0 ) );
compatibility
for b₁ being Nat holds
( b₁ = k mod l iff ( ex t being Nat st
( k = (l * t) + b₁ & b₁ < l ) or ( b₁ = 0 & l = 0 ) ) )

proof end;

coherence
k mod l is Nat by Lm2;

end;

:: deftheorem Def2 defines mod NAT_D:def 2 :
for k, l, b₃ being Nat holds
( b₃ = k mod l iff ( ex t being Nat st
( k = (l * t) + b₃ & b₃ < l ) or ( b₃ = 0 & l = 0 ) ) );

definition

let k, l be Nat;
:: original: div
redefine func k div l -> Element of NAT ;
coherence
k div l is Element of NAT

proof end;

:: original: mod
redefine func k mod l -> Element of NAT ;
coherence
k mod l is Element of NAT

proof end;

end;

theorem Th1: :: NAT_D:1

for i, j being Nat st 0 < i holds
j mod i < i

proof end;

theorem :: NAT_D:2

for i, j being Nat st 0 < i holds
j = (i * (j div i)) + (j mod i) by INT_1:86;

definition

let k, l be Nat;
:: original: divides
redefine pred k divides l means :Def3: :: NAT_D:def 3
ex t being Nat st l = k * t;
compatibility
( k divides l iff ex t being Nat st l = k * t )

proof end;

reflexivity
for k being Nat ex t being Nat st k = k * t

proof end;

end;

:: deftheorem Def3 defines divides NAT_D:def 3 :
for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t );

theorem Th3: :: NAT_D:3

for j, i being Nat holds
( j divides i iff i = j * (i div j) )

proof end;

theorem :: NAT_D:4

for i, j, h being Nat st i divides j & j divides h holds
i divides h

proof end;

theorem Th5: :: NAT_D:5

for i, j being Nat st i divides j & j divides i holds
i = j

proof end;

theorem Th6: :: NAT_D:6

for i being Nat holds
( i divides 0 & 1 divides i )

proof end;

theorem :: NAT_D:7

for j, i being Nat st 0 < j & i divides j holds
i <= j

proof end;

theorem Th8: :: NAT_D:8

for i, j, h being Nat st i divides j & i divides h holds
i divides j + h

proof end;

theorem Th9: :: NAT_D:9

for i, j, h being Nat st i divides j holds
i divides j * h

proof end;

theorem Th10: :: NAT_D:10

for i, j, h being Nat st i divides j & i divides j + h holds
i divides h

proof end;

theorem Th11: :: NAT_D:11

for i, j, h being Nat st i divides j & i divides h holds
i divides j mod h

proof end;

definition

let k, n be Nat;
redefine func k lcm n means :Def4: :: NAT_D:def 4
( k divides it & n divides it & ( for m being Nat st k divides m & n divides m holds
it divides m ) );
compatibility
for b₁ being set holds
( b₁ = k lcm n iff ( k divides b₁ & n divides b₁ & ( for m being Nat st k divides m & n divides m holds
b₁ divides m ) ) )

proof end;

end;

:: deftheorem Def4 defines lcm NAT_D:def 4 :
for k, n being Nat
for b₃ being set holds
( b₃ = k lcm n iff ( k divides b₃ & n divides b₃ & ( for m being Nat st k divides m & n divides m holds
b₃ divides m ) ) );

definition

let k, n be Nat;
:: original: lcm
redefine func k lcm n -> Element of NAT ;
coherence
k lcm n is Element of NAT by ORDINAL1:def 13;

end;

definition

let k, n be Nat;
redefine func k gcd n means :Def5: :: NAT_D:def 5
( it divides k & it divides n & ( for m being Nat st m divides k & m divides n holds
m divides it ) );
compatibility
for b₁ being set holds
( b₁ = k gcd n iff ( b₁ divides k & b₁ divides n & ( for m being Nat st m divides k & m divides n holds
m divides b₁ ) ) )

proof end;

end;

:: deftheorem Def5 defines gcd NAT_D:def 5 :
for k, n being Nat
for b₃ being set holds
( b₃ = k gcd n iff ( b₃ divides k & b₃ divides n & ( for m being Nat st m divides k & m divides n holds
m divides b₃ ) ) );

definition

let k, n be Nat;
:: original: gcd
redefine func k gcd n -> Element of NAT ;
coherence
k gcd n is Element of NAT by ORDINAL1:def 13;

end;

scheme :: NAT_D:sch 1
Euklides{ F₁( Nat) -> Nat, F₂() -> Nat, F₃() -> Nat } :

ex n being Element of NAT st
( F₁(n) = F₂() gcd F₃() & F₁((n + 1)) = 0 )

provided

A1: ( 0 < F₃() & F₃() < F₂() ) and
A2: ( F₁(0) = F₂() & F₁(1) = F₃() ) and
A3: for n being Element of NAT holds F₁((n + 2)) = F₁(n) mod F₁((n + 1))

proof end;

theorem :: NAT_D:12

for n being Nat holds
( n mod 2 = 0 or n mod 2 = 1 )

proof end;

theorem :: NAT_D:13

for k, n being Nat holds (k * n) mod k = 0

proof end;

theorem :: NAT_D:14

for k being Nat st k > 1 holds
1 mod k = 1

proof end;

theorem :: NAT_D:15

for k, n, l, m being Nat st k mod n = 0 & l = k - (m * n) holds
l mod n = 0

proof end;

theorem :: NAT_D:16

for n, k, l being Nat st n <> 0 & k mod n = 0 & l < n holds
(k + l) mod n = l

proof end;

theorem :: NAT_D:17

for k, n, l being Nat st k mod n = 0 holds
(k + l) mod n = l mod n

proof end;

theorem :: NAT_D:18

for k, n being Nat st k <> 0 holds
(k * n) div k = n

proof end;

theorem :: NAT_D:19

for k, n, l being Nat st k mod n = 0 holds
(k + l) div n = (k div n) + (l div n)

proof end;

begin

theorem :: NAT_D:20

for k, m being Nat st k <> 0 holds
(m * k) div k = m

proof end;

theorem Th21: :: NAT_D:21

for m, n, k being Nat holds m mod n = ((n * k) + m) mod n

proof end;

theorem Th22: :: NAT_D:22

for p, s, n being Nat holds (p + s) mod n = ((p mod n) + s) mod n

proof end;

theorem :: NAT_D:23

for p, s, n being Nat holds (p + s) mod n = (p + (s mod n)) mod n by Th22;

theorem Th24: :: NAT_D:24

for k, n being Nat st k < n holds
k mod n = k

proof end;

theorem :: NAT_D:25

for n being Nat holds n mod n = 0

proof end;

theorem :: NAT_D:26

for n being Nat holds 0 = 0 mod n

proof end;

theorem Th27: :: NAT_D:27

for i, j being Nat st i < j holds
i div j = 0

proof end;

theorem Th28: :: NAT_D:28

for m, n being Nat st m > 0 holds
n gcd m = m gcd (n mod m)

proof end;

scheme :: NAT_D:sch 2
INDI{ F₁() -> Element of NAT , F₂() -> Element of NAT , P₁[ set ] } :

P₁[F₂()]

provided

A1: P₁[ 0 ] and
A2: F₁() > 0 and
A3: for i, j being Nat st P₁[F₁() * i] & j <> 0 & j <= F₁() holds
P₁[(F₁() * i) + j]

proof end;

theorem :: NAT_D:29

for i, j being Nat holds i * j = (i lcm j) * (i gcd j)

proof end;

theorem :: NAT_D:30

for i, j being Integer st i >= 0 & j > 0 holds
i gcd j = j gcd (i mod j)

proof end;

theorem :: NAT_D:31

for i being Nat holds i lcm i = i

proof end;

theorem :: NAT_D:32

for i being Nat holds i gcd i = i

proof end;

theorem :: NAT_D:33

for i, j being Nat st i < j & i <> 0 holds
not i / j is integer

proof end;

definition

let i, j be natural number ;
:: original: -'
redefine func i -' j -> Element of NAT ;
coherence
i -' j is Element of NAT

proof end;

end;

theorem Th34: :: NAT_D:34

for i, j being natural number holds (i + j) -' j = i

proof end;

theorem Th35: :: NAT_D:35

for a, b being natural number holds a -' b <= a

proof end;

theorem Th36: :: NAT_D:36

for n, i being Nat st n -' i = 0 holds
n <= i

proof end;

theorem :: NAT_D:37

for i, j, k being Nat st i <= j holds
(j + k) -' i = (j + k) - i by NAT_1:12, XREAL_1:235;

theorem :: NAT_D:38

for i, j, k being Nat st i <= j holds
(j + k) -' i = (j -' i) + k

proof end;

theorem Th39: :: NAT_D:39

for i, i1 being natural number st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
i -' i1 = i - i1

proof end;

theorem :: NAT_D:40

for n being natural number holds n -' 0 = n

proof end;

theorem :: NAT_D:41

for i1, i2, n being natural number st i1 <= i2 holds
n -' i2 <= n -' i1

proof end;

theorem Th42: :: NAT_D:42

for i1, i2, n being natural number st i1 <= i2 holds
i1 -' n <= i2 -' n

proof end;

theorem Th43: :: NAT_D:43

for i, i1 being natural number st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
(i -' i1) + i1 = i

proof end;

theorem :: NAT_D:44

for i1, i2 being natural number st i1 <= i2 holds
i1 -' 1 <= i2

proof end;

theorem Th45: :: NAT_D:45

for i being natural number holds i -' 2 = (i -' 1) -' 1

proof end;

theorem Th46: :: NAT_D:46

for i1, i2 being natural number st i1 + 1 <= i2 holds
( i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )

proof end;

theorem :: NAT_D:47

for i1, i2 being natural number st ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) holds
( i1 + 1 < i2 & (i1 + 1) -' 1 < i2 & (i1 + 1) -' 2 < i2 & i1 + 1 <= i2 & (i1 -' 1) + 1 < i2 & ((i1 -' 1) + 1) -' 1 < i2 & i1 < i2 & i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )

proof end;

theorem :: NAT_D:48

for i1, i2 being natural number st ( i1 <= i2 or i1 <= i2 -' 1 ) holds
( i1 < i2 + 1 & i1 <= i2 + 1 & i1 < (i2 + 1) + 1 & i1 <= (i2 + 1) + 1 & i1 < i2 + 2 & i1 <= i2 + 2 )

proof end;

theorem :: NAT_D:49

for i1, i2 being natural number st ( i1 < i2 or i1 + 1 <= i2 ) holds
i1 <= i2 -' 1

proof end;

theorem Th50: :: NAT_D:50

for i, i1, i2 being natural number st i >= i1 holds
i >= i1 -' i2

proof end;

theorem :: NAT_D:51

for i, i1 being natural number st 1 <= i & 1 <= i1 -' i holds
i1 -' i < i1

proof end;

theorem Th52: :: NAT_D:52

for i, k, j being natural number st i -' k <= j holds
i <= j + k

proof end;

theorem :: NAT_D:53

for i, j, k being natural number st i <= j + k holds
i -' k <= j

proof end;

theorem :: NAT_D:54

for i, j, k being natural number st i <= j -' k & k <= j holds
i + k <= j

proof end;

theorem :: NAT_D:55

for j, k, i being natural number st j + k <= i holds
k <= i -' j

proof end;

theorem :: NAT_D:56

for k, i, j being natural number st k <= i & i < j holds
i -' k < j -' k

proof end;

theorem :: NAT_D:57

for i, j, k being natural number st i < j & k < j holds
i -' k < j -' k

proof end;

theorem :: NAT_D:58

for i, j being natural number st i <= j holds
j -' (j -' i) = i

proof end;

theorem :: NAT_D:59

for n, k being natural number st n < k holds
(k -' (n + 1)) + 1 = k -' n

proof end;