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

Lm1: now :: thesis: for k, l being natural Number holds k div l is Nat

let k, l be natural Number ; :: thesis: k div l is Nat
reconsider k1 = k, l1 = l as Nat by TARSKI:1;
k1 div l1 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 natural Number holds k mod l is Nat

let k, l be natural Number ; :: 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 natural Number ;

:: 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 being natural Number
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 ) ) );

definition

let k, l be natural Number ;

:: 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 being natural Number
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 ) ) );

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 natural Number st 0 < i holds
j mod i < i by INT_1:58;

theorem :: NAT_D:2

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

:: The divisibility relation

definition

let k, l be natural Number ;

:: original: divides
redefine pred k divides l means :: 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 natural Number ex t being Nat st k = k * t

proof end;

end;

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

theorem Th3: :: NAT_D:3

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

proof end;

theorem :: NAT_D:4

for h, i, j being natural Number st i divides j & j divides h holds
i divides h by INT_2:9;

theorem Th5: :: NAT_D:5

for i, j being natural Number st i divides j & j divides i holds
i = j

proof end;

theorem Th6: :: NAT_D:6

for i being natural Number holds
( i divides 0 & 1 divides i ) by INT_2:12;

theorem :: NAT_D:7

for i, j being natural Number st 0 < j & i divides j holds
i <= j by INT_2:27;

theorem Th8: :: NAT_D:8

for h, i, j being natural Number st i divides j & i divides h holds
i divides j + h

proof end;

theorem Th9: :: NAT_D:9

for h, i, j being natural Number st i divides j holds
i divides j * h by INT_2:2;

theorem Th10: :: NAT_D:10

for h, i, j being natural Number st i divides j & i divides j + h holds
i divides h

proof end;

theorem Th11: :: NAT_D:11

for h, i, j being natural Number 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 natural Number ;

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 natural Number
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 12;

end;

definition

let k, n be natural Number ;

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 natural Number
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 12;

end;

:: Correctness of Euclid's Algorithm
:: Greatest Common Divisor Algorithm

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

ex n being 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 Nat holds F₁((n + 2)) = F₁(n) mod F₁((n + 1))

proof end;

theorem :: NAT_D:12

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

proof end;

theorem :: NAT_D:13

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

proof end;

theorem :: NAT_D:14

for k being natural Number st k > 1 holds
1 mod k = 1

proof end;

theorem :: NAT_D:15

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

proof end;

theorem :: NAT_D:16

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

proof end;

theorem :: NAT_D:17

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

proof end;

theorem :: NAT_D:18

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

proof end;

theorem :: NAT_D:19

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

proof end;

theorem :: NAT_D:20

canceled;

::$CT
:: from GR_CY_1, 2005.11.16, A.T.

theorem Th21: :: NAT_D:21

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

proof end;

theorem Th22: :: NAT_D:22

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

proof end;

theorem :: NAT_D:23

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

theorem Th24: :: NAT_D:24

for k, n being natural Number st k < n holds
k mod n = k

proof end;

theorem Th25: :: NAT_D:25

for n being natural Number holds n mod n = 0

proof end;

theorem Th26: :: NAT_D:26

for n being natural Number holds 0 = 0 mod n

proof end;

:: from JORDAN4

theorem Th27: :: NAT_D:27

for i, j being natural Number 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 natural Number 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{ 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;

:: moved from INT_2, 2007.11.7, A.T,

theorem :: NAT_D:29

for i, j being natural Number 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 natural Number holds i lcm i = i

proof end;

theorem :: NAT_D:32

for i being natural Number holds i gcd i = i

proof end;

:: from SCMPDS_9. 2008.05.06, A.T.

theorem :: NAT_D:33

for i, j being natural Number 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 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 natural Number st n -' i = 0 holds
n <= i

proof end;

theorem :: NAT_D:37

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

theorem :: NAT_D:38

for k, i, j being natural Number 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 n, i1, i2 being natural Number st i1 <= i2 holds
n -' i2 <= n -' i1

proof end;

theorem Th42: :: NAT_D:42

for n, i1, i2 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 k, i, j being natural Number st i -' k <= j holds
i <= j + k

proof end;

theorem :: NAT_D:53

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

proof end;

theorem :: NAT_D:54

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

proof end;

theorem :: NAT_D:55

for k, i, j 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 k, i, j being natural Number 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 natural Number st i <= j holds
j -' (j -' i) = i

proof end;

:: from LEXBFS, 2008.08.23, A.T.

theorem :: NAT_D:59

for k, n being natural Number 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 natural Number 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 natural Number
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 Th67: :: NAT_D:67

for n, a, b being Integer holds (a * b) mod n = ((a mod n) * (b mod n)) mod n

proof end;

:: Bezout's identity
:: Bezout's lemma

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 k, n being natural Number st n mod k = k - 1 holds
(n + 1) mod k = 0

proof end;

theorem :: NAT_D:70

for k, n being natural Number st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1

proof end;

theorem :: NAT_D:71

for i being Integer
for n being Nat holds (i * n) mod n = 0

proof end;

theorem :: NAT_D:72

for m, n being natural Number st m - n >= 0 holds
(m -' n) + n = m

proof end;