:: 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 funck div l ->  Nat means :Def1: :: NAT_D:def 1
( ex t being Nat st
( k = (l * it) + t &amp; t < l ) or ( it = 0 &amp; l = 0 ) );
compatibility
 for b1 being Nat holds
( b1 = k div l iff ( ex t being Nat st
( k = (l * b1) + t &amp; t < l ) or ( b1 = 0 &amp; l = 0 ) ) )
proofend;
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 &amp; t < l ) or ( b3 = 0 &amp; l = 0 ) ) );

definition
let k, l be Nat;
:: original:mod
redefine funck mod l ->  Nat means :Def2: :: NAT_D:def 2
( ex t being Nat st
( k = (l * t) + it &amp; it < l ) or ( it = 0 &amp; l = 0 ) );
compatibility
 for b1 being Nat holds
( b1 = k mod l iff ( ex t being Nat st
( k = (l * t) + b1 &amp; b1 < l ) or ( b1 = 0 &amp; l = 0 ) ) )
proofend;
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 &amp; b3 < l ) or ( b3 = 0 &amp; l = 0 ) ) );

definition
let k, l be Nat;
:: original:div
redefine funck div l ->  Element of NAT ;
coherence
 k div l is Element of NAT
proofend;
:: original:mod
redefine funck mod l ->  Element of NAT ;
coherence
 k mod l is Element of NAT
proofend;
end;

theorem Th1: :: NAT_D:1
for i, j being Nat st 0 < i holds
j mod i < i
proofend;

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 predk 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 )
proofend;
reflexivity
 for k being Nat ex t being Nat st k = k * t
proofend;
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) )
proofend;

theorem :: NAT_D:4
for i, j, h being Nat st i divides j &amp; j divides h holds
i divides h
proofend;

theorem Th5: :: NAT_D:5
for i, j being Nat st i divides j &amp; j divides i holds
i = j
proofend;

theorem Th6: :: NAT_D:6
for i being Nat holds
( i divides 0 &amp; 1 divides i )
proofend;

theorem :: NAT_D:7
for j, i being Nat st 0 < j &amp; i divides j holds
i <= j
proofend;

theorem Th8: :: NAT_D:8
for i, j, h being Nat st i divides j &amp; i divides h holds
i divides j + h
proofend;

theorem Th9: :: NAT_D:9
for i, j, h being Nat st i divides j holds
i divides j * h
proofend;

theorem Th10: :: NAT_D:10
for i, j, h being Nat st i divides j &amp; i divides j + h holds
i divides h
proofend;

theorem Th11: :: NAT_D:11
for i, j, h being Nat st i divides j &amp; i divides h holds
i divides j mod h
proofend;

:: 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 &amp; n divides it &amp; ( for m being Nat st k divides m &amp; n divides m holds
it divides m ) );
compatibility
 for b1 being set holds
( b1 = k lcm n iff ( k divides b1 &amp; n divides b1 &amp; ( for m being Nat st k divides m &amp; n divides m holds
b1 divides m ) ) )
proofend;
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 &amp; n divides b3 &amp; ( for m being Nat st k divides m &amp; n divides m holds
b3 divides m ) ) );

definition
let k, n be Nat;
:: original:lcm
redefine funck 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 &amp; it divides n &amp; ( for m being Nat st m divides k &amp; m divides n holds
m divides it ) );
compatibility
 for b1 being set holds
( b1 = k gcd n iff ( b1 divides k &amp; b1 divides n &amp; ( for m being Nat st m divides k &amp; m divides n holds
m divides b1 ) ) )
proofend;
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 &amp; b3 divides n &amp; ( for m being Nat st m divides k &amp; m divides n holds
m divides b3 ) ) );

definition
let k, n be Nat;
:: original:gcd
redefine funck 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() &amp; F1((n + 1)) = 0 )
provided
A1: ( 0 < F3() &amp; F3() < F2() ) and
A2: ( F1(0) = F2() &amp; F1(1) = F3() ) and
A3: for n being Element of NAT holds F1((n + 2)) = F1(n) mod F1((n + 1))
proofend;

theorem :: NAT_D:12
for n being Nat holds
( n mod 2 = 0 or n mod 2 = 1 )
proofend;

theorem :: NAT_D:13
for k, n being Nat holds (k * n) mod k = 0
proofend;

theorem :: NAT_D:14
for k being Nat st k > 1 holds
1 mod k = 1
proofend;

theorem :: NAT_D:15
for k, n, l, m being Nat st k mod n = 0 &amp; l = k - (m * n) holds
l mod n = 0
proofend;

theorem :: NAT_D:16
for n, k, l being Nat st n <> 0 &amp; k mod n = 0 &amp; l < n holds
(k + l) mod n = l
proofend;

theorem :: NAT_D:17
for k, n, l being Nat st k mod n = 0 holds
(k + l) mod n = l mod n
proofend;

theorem :: NAT_D:18
for k, n being Nat st k <> 0 holds
(k * n) div k = n
proofend;

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)
proofend;

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
proofend;

:: 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
proofend;

theorem Th22: :: NAT_D:22
for p, s, n being Nat holds (p + s) mod n = ((p mod n) + s) mod n
proofend;

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
proofend;

theorem Th25: :: NAT_D:25
for n being Nat holds n mod n = 0
proofend;

theorem :: NAT_D:26
for n being Nat holds 0 = 0 mod n
proofend;

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

:: 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)
proofend;

:: 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] &amp; j <> 0 &amp; j <= F1() holds
P1[(F1() * i) + j]
proofend;

:: 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)
proofend;

:: from from SCMP_GCD, 2007.07.26, A.T.
theorem :: NAT_D:30
for i, j being Integer st i >= 0 &amp; j > 0 holds
i gcd j = j gcd (i mod j)
proofend;

:: ???, 2007.07.26, A.T.
theorem :: NAT_D:31
for i being Nat holds i lcm i = i
proofend;

theorem :: NAT_D:32
for i being Nat holds i gcd i = i
proofend;

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

:: from BINARITH, 2008.08.18, A.T.
definition
let i, j be Nat;
:: original:-'
redefine funci -' j ->  Element of NAT ;
coherence
 i -' j is Element of NAT
proofend;
end;

theorem Th34: :: NAT_D:34
for i, j being Nat holds (i + j) -' j = i
proofend;

theorem Th35: :: NAT_D:35
for a, b being Nat holds a -' b <= a
proofend;

theorem Th36: :: NAT_D:36
for n, i being Nat st n -' i = 0 holds
n <= i
proofend;

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
proofend;

theorem Th39: :: NAT_D:39
for i, i1 being Nat st ( i -' i1 >= 1 or i - i1 >= 1 ) holds
i -' i1 = i - i1
proofend;

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

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

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

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

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

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

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

theorem :: NAT_D:47
for i1, i2 being Nat st ( i1 + 2 <= i2 or (i1 + 1) + 1 <= i2 ) holds
( i1 + 1 < i2 &amp; (i1 + 1) -' 1 < i2 &amp; (i1 + 1) -' 2 < i2 &amp; i1 + 1 <= i2 &amp; (i1 -' 1) + 1 < i2 &amp; ((i1 -' 1) + 1) -' 1 < i2 &amp; i1 < i2 &amp; i1 -' 1 < i2 &amp; i1 -' 2 < i2 &amp; i1 <= i2 )
proofend;

theorem :: NAT_D:48
for i1, i2 being Nat st ( i1 <= i2 or i1 <= i2 -' 1 ) holds
( i1 < i2 + 1 &amp; i1 <= i2 + 1 &amp; i1 < (i2 + 1) + 1 &amp; i1 <= (i2 + 1) + 1 &amp; i1 < i2 + 2 &amp; i1 <= i2 + 2 )
proofend;

theorem :: NAT_D:49
for i1, i2 being Nat st ( i1 < i2 or i1 + 1 <= i2 ) holds
i1 <= i2 -' 1
proofend;

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

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

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

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

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

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

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

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

:: 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
proofend;

:: 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
proofend;

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

:: 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 ) &amp; (a + (n * k)) mod n = a mod n )
proofend;

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

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

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

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

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

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

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

:: 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
proofend;

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