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


begin

Lm1: now :: thesis: for k, l being Nat holds k div l is Nat
let k, l be Nat; :: thesis: k div l is Nat
k div l in NAT by INT_1:3, INT_1:55;
hence k div l is Nat ; :: thesis: verum
end;

Lm2: now :: thesis: for k, l being Nat holds k mod l is Nat
let k, l be Nat; :: thesis: k mod l is Nat
k mod l in NAT by INT_1:3, INT_1:57;
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:59;

:: The divisibility relation
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;

:: The least common multiple and the greatest common divisor
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 12;
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 12;
end;

:: WP: Correctness of Euclide Algorithm
:: WP: Greatest Common Divisor Algorithm
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

:: from AMI_5, 2005.11.16, A.T.
theorem :: NAT_D:20
for k, m being Nat st k <> 0 holds
(m * k) div k = m
proof end;

:: from GR_CY_1, 2005.11.16, A.T.
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 Th25: :: 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;

:: from JORDAN4
theorem Th27: :: NAT_D:27
for i, j being Nat st i < j holds
i div j = 0
proof end;

:: Moved from SCMP_GCD by AK on 28.12.2006
theorem Th28: :: NAT_D:28
for m, n being Nat st m > 0 holds
n gcd m = m gcd (n mod m)
proof end;

:: from AMI_3, 2007.06.14, A.T.
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;

:: moved from INT_2, 2007.11.7, A.T,
theorem :: NAT_D:29
for i, j being Nat holds i * j = (i lcm j) * (i gcd j)
proof end;

:: from from SCMP_GCD, 2007.07.26, A.T.
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;

:: ???, 2007.07.26, A.T.
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;

:: from SCMPDS_9. 2008.05.06, A.T.
theorem :: NAT_D:33
for i, j being Nat st i < j & i <> 0 holds
not i / j is integer
proof end;

:: from BINARITH, 2008.08.18, A.T.
definition
let i, j be Nat;
:: 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 Nat holds (i + j) -' j = i
proof end;

theorem Th35: :: NAT_D:35
for a, b being Nat 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:233;

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 Nat st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
i -' i1 = i - i1
proof end;

theorem :: NAT_D:40
for n being Nat holds n -' 0 = n
proof end;

theorem :: NAT_D:41
for i1, i2, n being Nat st i1 <= i2 holds
n -' i2 <= n -' i1
proof end;

theorem Th42: :: NAT_D:42
for i1, i2, n being Nat st i1 <= i2 holds
i1 -' n <= i2 -' n
proof end;

theorem Th43: :: NAT_D:43
for i, i1 being Nat st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
(i -' i1) + i1 = i
proof end;

theorem :: NAT_D:44
for i1, i2 being Nat st i1 <= i2 holds
i1 -' 1 <= i2
proof end;

theorem Th45: :: NAT_D:45
for i being Nat holds i -' 2 = (i -' 1) -' 1
proof end;

theorem Th46: :: NAT_D:46
for i1, i2 being Nat st i1 + 1 <= i2 holds
( i1 -' 1 < i2 & i1 -' 2 < i2 & i1 <= i2 )
proof end;

theorem :: NAT_D:47
for i1, i2 being Nat 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 Nat 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 Nat st ( i1 < i2 or i1 + 1 <= i2 ) holds
i1 <= i2 -' 1
proof end;

theorem Th50: :: NAT_D:50
for i, i1, i2 being Nat st i >= i1 holds
i >= i1 -' i2
proof end;

theorem :: NAT_D:51
for i, i1 being Nat st 1 <= i & 1 <= i1 -' i holds
i1 -' i < i1
proof end;

theorem Th52: :: NAT_D:52
for i, k, j being Nat st i -' k <= j holds
i <= j + k
proof end;

theorem :: NAT_D:53
for i, j, k being Nat st i <= j + k holds
i -' k <= j
proof end;

theorem :: NAT_D:54
for i, j, k being Nat st i <= j -' k & k <= j holds
i + k <= j
proof end;

theorem :: NAT_D:55
for j, k, i being Nat st j + k <= i holds
k <= i -' j
proof end;

theorem :: NAT_D:56
for k, i, j being Nat st k <= i & i < j holds
i -' k < j -' k
proof end;

theorem :: NAT_D:57
for i, j, k being Nat st i < j & k < j holds
i -' k < j -' k
proof end;

:: form JCT_MISC, 2008.08.21, A.T.
theorem :: NAT_D:58
for i, j being Nat st i <= j holds
j -' (j -' i) = i
proof end;

:: from LEXBFS, 2008.08.23, A.T.
theorem :: NAT_D:59
for n, k being Nat st n < k holds
(k -' (n + 1)) + 1 = k -' n
proof end;

theorem :: NAT_D:60
for A being finite set holds
( A is trivial iff card A < 2 )
proof end;

:: from INT_3, 2011.04.28, A.T.
theorem Th61: :: NAT_D:61
for n, a, k being Integer holds
( ( n <> 0 implies (a + (n * k)) div n = (a div n) + k ) & (a + (n * k)) mod n = a mod n )
proof end;

theorem Th62: :: NAT_D:62
for n being Nat st n > 0 holds
for a being Integer holds
( a mod n >= 0 & a mod n < n )
proof end;

theorem Th63: :: NAT_D:63
for n, a being Integer holds
( ( 0 <= a & a < n implies a mod n = a ) & ( 0 > a & a >= - n implies a mod n = n + a ) )
proof end;

theorem Th64: :: NAT_D:64
for n, a, b being Integer holds
( ( n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n ) & ( a,b are_congruent_mod n implies a mod n = b mod n ) )
proof end;

theorem :: NAT_D:65
for n being Nat
for a being Integer holds (a mod n) mod n = a mod n
proof end;

theorem :: NAT_D:66
for n, a, b being Integer holds (a + b) mod n = ((a mod n) + (b mod n)) mod n
proof end;

theorem :: NAT_D:67
for n, a, b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n
proof end;

theorem :: NAT_D:68
for a, b being Integer ex s, t being Integer st a gcd b = (s * a) + (t * b)
proof end;

:: from RADIX_1, 2011.07.31, A.T.
theorem :: NAT_D:69
for n, k being Nat st n mod k = k - 1 holds
(n + 1) mod k = 0
proof end;

theorem :: NAT_D:70
for n, k being Nat st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1
proof end;