:: The Fundamental Properties of Natural Numbers
:: by Grzegorz Bancerek
::
:: Received January 11, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: NAT_1:1
theorem Th2: :: NAT_1:2
theorem :: NAT_1:3
theorem :: NAT_1:4
for
i,
j,
h being
Nat st
i <= j holds
i * h <= j * h
theorem :: NAT_1:5
for
i being
Nat holds
0 < i + 1
theorem Th6: :: NAT_1:6
for
i being
Nat holds
(
i = 0 or ex
k being
Nat st
i = k + 1 )
theorem Th7: :: NAT_1:7
for
i,
j being
Nat st
i + j = 0 holds
(
i = 0 &
j = 0 )
scheme :: NAT_1:sch 3
DefbyInd{
F1()
-> Nat,
F2(
Nat,
Nat)
-> Nat,
P1[
Nat,
Nat] } :
( ( for
k being
Nat ex
n being
Nat st
P1[
k,
n] ) & ( for
k,
n,
m being
Nat st
P1[
k,
n] &
P1[
k,
m] holds
n = m ) )
provided
A1:
for
k,
n being
Nat holds
(
P1[
k,
n] iff ( (
k = 0 &
n = F1() ) or ex
m,
l being
Nat st
(
k = m + 1 &
P1[
m,
l] &
n = F2(
k,
l) ) ) )
theorem Th8: :: NAT_1:8
for
i,
j being
Nat holds
( not
i <= j + 1 or
i <= j or
i = j + 1 )
theorem :: NAT_1:9
for
i,
j being
Nat st
i <= j &
j <= i + 1 & not
i = j holds
j = i + 1
theorem Th10: :: NAT_1:10
for
i,
j being
Nat st
i <= j holds
ex
k being
Nat st
j = i + k
theorem Th11: :: NAT_1:11
for
i,
j being
Nat holds
i <= i + j
theorem Th12: :: NAT_1:12
for
i,
j,
h being
Nat st
i <= j holds
i <= j + h
theorem Th13: :: NAT_1:13
for
i,
j being
Nat holds
(
i < j + 1 iff
i <= j )
theorem Th14: :: NAT_1:14
for
j being
Nat st
j < 1 holds
j = 0
theorem :: NAT_1:15
for
i,
j being
Nat st
i * j = 1 holds
i = 1
theorem Th16: :: NAT_1:16
for
k,
n being
Nat st
k <> 0 holds
n < n + k
theorem :: NAT_1:17
for
m being
Nat st
0 < m holds
for
n being
Nat ex
k,
t being
Nat st
(
n = (m * k) + t &
t < m )
theorem :: NAT_1:18
for
n,
m,
k,
t,
k1,
t1 being
Nat st
n = (m * k) + t &
t < m &
n = (m * k1) + t1 &
t1 < m holds
(
k = k1 &
t = t1 )
theorem :: NAT_1:19
for
k,
n being
Nat holds
(
k < k + n iff 1
<= n )
theorem :: NAT_1:20
theorem :: NAT_1:21
theorem Th22: :: NAT_1:22
for
m,
n being
Nat holds
( not
m < n + 1 or
m < n or
m = n )
theorem :: NAT_1:23
for
k being
Nat holds
( not
k < 2 or
k = 0 or
k = 1 )
theorem :: NAT_1:24
for
i,
h,
j being
Nat st
i <> 0 &
h = j * i holds
j <= h
theorem :: NAT_1:25
canceled;
theorem Th26: :: NAT_1:26
for
n being
Nat holds
( not
n <= 1 or
n = 0 or
n = 1 )
theorem Th27: :: NAT_1:27
for
n being
Nat holds
( not
n <= 2 or
n = 0 or
n = 1 or
n = 2 )
theorem Th28: :: NAT_1:28
for
n being
Nat holds
( not
n <= 3 or
n = 0 or
n = 1 or
n = 2 or
n = 3 )
theorem Th29: :: NAT_1:29
for
n being
Nat holds
( not
n <= 4 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 )
theorem Th30: :: NAT_1:30
for
n being
Nat holds
( not
n <= 5 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 )
theorem Th31: :: NAT_1:31
for
n being
Nat holds
( not
n <= 6 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 )
theorem Th32: :: NAT_1:32
for
n being
Nat holds
( not
n <= 7 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 )
theorem Th33: :: NAT_1:33
for
n being
Nat holds
( not
n <= 8 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 )
theorem Th34: :: NAT_1:34
for
n being
Nat holds
( not
n <= 9 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 )
theorem Th35: :: NAT_1:35
for
n being
Nat holds
( not
n <= 10 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 )
theorem Th36: :: NAT_1:36
for
n being
Nat holds
( not
n <= 11 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 )
theorem Th37: :: NAT_1:37
for
n being
Nat holds
( not
n <= 12 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 or
n = 12 )
theorem :: NAT_1:38
for
n being
Nat holds
( not
n <= 13 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 or
n = 12 or
n = 13 )
:: deftheorem defines min* NAT_1:def 1 :
theorem Th39: :: NAT_1:39
theorem Th40: :: NAT_1:40
for
n,
m being
Nat holds
(
n <= m iff
n c= m )
theorem Th41: :: NAT_1:41
theorem Th42: :: NAT_1:42
theorem :: NAT_1:43
:: deftheorem defines succ NAT_1:def 2 :
theorem :: NAT_1:44
theorem :: NAT_1:45
for
k,
n being
Nat holds
(
k in n iff
k < n )
theorem :: NAT_1:46
for
n being
Nat holds
n in n + 1
theorem :: NAT_1:47
for
k,
n being
Nat st
k <= n holds
k = k /\ n
scheme :: NAT_1:sch 13
RecUn{
F1()
-> set ,
F2()
-> Function,
F3()
-> Function,
P1[
set ,
set ,
set ] } :
provided
A1:
dom F2()
= NAT
and B1:
F2()
. 0 = F1()
and C1:
for
n being
Nat holds
P1[
n,
F2()
. n,
F2()
. (n + 1)]
and A2:
dom F3()
= NAT
and B2:
F3()
. 0 = F1()
and C2:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (n + 1)]
and A3:
for
n being
Nat for
x,
y1,
y2 being
set st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2
scheme :: NAT_1:sch 14
RecUnD{
F1()
-> non
empty set ,
F2()
-> Element of
F1(),
P1[
set ,
set ,
set ],
F3()
-> Function of
NAT ,
F1(),
F4()
-> Function of
NAT ,
F1() } :
provided
A1:
F3()
. 0 = F2()
and B2:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (n + 1)]
and A2:
F4()
. 0 = F2()
and B3:
for
n being
Nat holds
P1[
n,
F4()
. n,
F4()
. (n + 1)]
and A3:
for
n being
Nat for
x,
y1,
y2 being
Element of
F1() st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2
:: deftheorem Def3 defines ^\ NAT_1:def 3 :
theorem :: NAT_1:48
theorem Th59: :: NAT_1:49
theorem :: NAT_1:50
theorem :: NAT_1:51
theorem :: NAT_1:52
theorem :: NAT_1:53