:: Divisibility of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 3, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: 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 ) ) );
:: 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 ) ) );
theorem Th1: :: NAT_D:1
for
i,
j being
Nat st
0 < i holds
j mod i < i
theorem :: NAT_D:2
:: deftheorem Def3 defines divides NAT_D:def 3 :
theorem Th3: :: NAT_D:3
theorem :: NAT_D:4
theorem Th5: :: NAT_D:5
theorem Th6: :: NAT_D:6
theorem :: NAT_D:7
theorem Th8: :: NAT_D:8
theorem Th9: :: NAT_D:9
theorem Th10: :: NAT_D:10
theorem Th11: :: NAT_D:11
:: deftheorem Def4 defines lcm NAT_D:def 4 :
:: deftheorem Def5 defines gcd NAT_D:def 5 :
theorem :: NAT_D:12
theorem :: NAT_D:13
theorem :: NAT_D:14
for
k being
Nat st
k > 1 holds
1
mod k = 1
theorem :: NAT_D:15
theorem :: NAT_D:16
theorem :: NAT_D:17
theorem :: NAT_D:18
theorem :: NAT_D:19
theorem :: NAT_D:20
theorem Th21: :: NAT_D:21
theorem Th22: :: NAT_D:22
theorem :: NAT_D:23
theorem Th24: :: NAT_D:24
for
k,
n being
Nat st
k < n holds
k mod n = k
theorem :: NAT_D:25
theorem :: NAT_D:26
theorem Th27: :: NAT_D:27
for
i,
j being
Nat st
i < j holds
i div j = 0
theorem Th28: :: NAT_D:28
theorem :: NAT_D:29
theorem :: NAT_D:30
theorem :: NAT_D:31
theorem :: NAT_D:32
theorem :: NAT_D:33
theorem Th39: :: NAT_D:34
theorem Th52: :: NAT_D:35
theorem Th54: :: NAT_D:36
for
n,
i being
Nat st
n -' i = 0 holds
n <= i
theorem :: NAT_D:37
theorem :: NAT_D:38
for
i,
j,
k being
Nat st
i <= j holds
(j + k) -' i = (j -' i) + k
theorem Th57: :: NAT_D:39
theorem :: NAT_D:40
theorem :: NAT_D:41
theorem Th60: :: NAT_D:42
theorem Th61: :: NAT_D:43
theorem :: NAT_D:44
theorem Th63: :: NAT_D:45
theorem Th64: :: NAT_D:46
theorem :: NAT_D:47
theorem :: NAT_D:48
theorem :: NAT_D:49
theorem Thxx: :: NAT_D:50
theorem :: NAT_D:51
theorem Th70: :: NAT_D:52
theorem :: NAT_D:53
theorem :: NAT_D:54
theorem :: NAT_D:55
theorem :: NAT_D:56
theorem :: NAT_D:57
theorem :: NAT_D:58
theorem :: NAT_D:59