:: Natural Numbers
:: by Robert Milewski
::
:: Received February 23, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: NAT_2:1
canceled;
theorem :: NAT_2:2
theorem :: NAT_2:3
canceled;
theorem Th4: :: NAT_2:4
theorem :: NAT_2:5
theorem :: NAT_2:6
theorem :: NAT_2:7
for
i,
j,
k,
l being
Nat st
i <= j &
k <= j &
i = (j -' k) + l holds
k = (j -' i) + l
theorem :: NAT_2:8
theorem :: NAT_2:9
for
j,
i being
Nat st
j < i holds
(i -' (j + 1)) + 1
= i -' j
theorem Th10: :: NAT_2:10
for
i,
j being
Nat st
i >= j holds
j -' i = 0
theorem Th11: :: NAT_2:11
theorem Th12: :: NAT_2:12
theorem :: NAT_2:13
theorem Th14: :: NAT_2:14
theorem :: NAT_2:15
theorem :: NAT_2:16
theorem :: NAT_2:17
theorem :: NAT_2:18
theorem :: NAT_2:19
theorem :: NAT_2:20
theorem :: NAT_2:21
theorem :: NAT_2:22
for
n,
k being
Nat st
n <= k &
k < n + n holds
k div n = 1
theorem Th23: :: NAT_2:23
theorem :: NAT_2:24
for
n being
Nat holds
( not
n is
even iff
n mod 2
= 1 )
theorem :: NAT_2:25
theorem Th26: :: NAT_2:26
theorem :: NAT_2:27
theorem :: NAT_2:28
theorem :: NAT_2:29
:: deftheorem Def1 defines trivial NAT_2:def 1 :
theorem :: NAT_2:30
theorem :: NAT_2:31
theorem :: NAT_2:32
for
i,
j,
k being
Nat holds
(i -' j) -' k = i -' (j + k)