:: Divisibility of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 3, 2007
:: Copyright (c) 2007-2011 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 b1 being Nat holds
( b1 = k div l iff ( ex t being Nat st
( k = (l * b1) + t & t < l ) or ( b1 = 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, b3 being Nat holds
( b3 = k div l iff ( ex t being Nat st
( k = (l * b3) + t & t < l ) or ( b3 = 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 b1 being Nat holds
( b1 = k mod l iff ( ex t being Nat st
( k = (l * t) + b1 & b1 < l ) or ( b1 = 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, b3 being Nat holds
( b3 = k mod l iff ( ex t being Nat st
( k = (l * t) + b3 & b3 < l ) or ( b3 = 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 b1 being set holds
( b1 = k lcm n iff ( k divides b1 & n divides b1 & ( for m being Nat st k divides m & n divides m holds
b1 divides m ) ) )
proof end;
end;

:: deftheorem Def4 defines lcm NAT_D:def 4 :
for k, n being Nat
for b3 being set holds
( b3 = k lcm n iff ( k divides b3 & n divides b3 & ( for m being Nat st k divides m & n divides m holds
b3 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 b1 being set holds
( b1 = k gcd n iff ( b1 divides k & b1 divides n & ( for m being Nat st m divides k & m divides n holds
m divides b1 ) ) )
proof end;
end;

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

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{ F1( Nat) -> Nat, F2() -> Nat, F3() -> Nat } :
ex n being Element of NAT st
( F1(n) = F2() gcd F3() & F1((n + 1)) = 0 )
provided
A1: ( 0 < F3() & F3() < F2() ) and
A2: ( F1(0) = F2() & F1(1) = F3() ) and
A3: for n being Element of NAT holds F1((n + 2)) = F1(n) mod F1((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{ F1() -> Element of NAT , F2() -> Element of NAT , P1[ set ] } :
P1[F2()]
provided
A1: P1[ 0 ] and
A2: F1() > 0 and
A3: for i, j being Nat st P1[F1() * i] & j <> 0 & j <= F1() holds
P1[(F1() * 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;