:: NAT_2 semantic presentation

scheme :: NAT_2:sch 1
NonUniqPiFinRecExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Nat, P₁[ set , set , set ] } :

ex p being FinSequence of F₁() st
( len p = F₃() & ( p /. 1 = F₂() or F₃() = 0 ) & ( for n being Nat st 1 <= n & n < F₃() holds
P₁[n,p /. n,p /. (n + 1)] ) )

provided

A1: for n being Nat st 1 <= n & n < F₃() holds
for x being Element of F₁() ex y being Element of F₁() st P₁[n,x,y]

proof end;

theorem :: NAT_2:1

canceled;

theorem :: NAT_2:2

for x, y being real number st x >= 0 & y > 0 holds
x / ([\(x / y)/] + 1) < y

proof end;

theorem :: NAT_2:3

canceled;

theorem Th4: :: NAT_2:4

for n being natural number holds 0 div n = 0

proof end;

theorem :: NAT_2:5

for n being non empty Nat holds n div n = 1

proof end;

theorem :: NAT_2:6

for n being Nat holds n div 1 = n

proof end;

theorem :: NAT_2:7

for i, j, k, l being natural number st i <= j & k <= j & i = (j -' k) + l holds
k = (j -' i) + l

proof end;

theorem :: NAT_2:8

for i, n being natural number st i in Seg n holds
(n -' i) + 1 in Seg n

proof end;

theorem :: NAT_2:9

for i, j being natural number st j < i holds
(i -' (j + 1)) + 1 = i -' j

proof end;

theorem Th10: :: NAT_2:10

for i, j being natural number st i >= j holds
j -' i = 0

proof end;

theorem Th11: :: NAT_2:11

for i, j being non empty natural number holds i -' j < i

proof end;

theorem Th12: :: NAT_2:12

for n, k being natural number st k <= n holds
2 to_power n = (2 to_power k) * (2 to_power (n -' k))

proof end;

theorem :: NAT_2:13

for n, k being Nat st k <= n holds
2 to_power k divides 2 to_power n

proof end;

theorem Th14: :: NAT_2:14

for n, k being natural number st k > 0 & n div k = 0 holds
n < k

proof end;

theorem :: NAT_2:15

for k, n being natural number st k > 0 & k <= n holds
n div k >= 1

proof end;

theorem :: NAT_2:16

for k, n being natural number st k <> 0 holds
(n + k) div k = (n div k) + 1

proof end;

theorem :: NAT_2:17

for k, n, i being natural number st k divides n & 1 <= n & 1 <= i & i <= k holds
(n -' i) div k = (n div k) - 1

proof end;

theorem :: NAT_2:18

for n, k being Nat st k <= n holds
(2 to_power n) div (2 to_power k) = 2 to_power (n -' k)

proof end;

theorem :: NAT_2:19

for n being Nat st n > 0 holds
(2 to_power n) mod 2 = 0

proof end;

theorem :: NAT_2:20

for n being Nat st n > 0 holds
( n mod 2 = 0 iff (n -' 1) mod 2 = 1 )

proof end;

theorem :: NAT_2:21

for n being non empty natural number st n <> 1 holds
n > 1

proof end;

theorem :: NAT_2:22

for n, k being natural number st n <= k & k < n + n holds
k div n = 1

proof end;

theorem Th23: :: NAT_2:23

for n being Nat holds
( n is even iff n mod 2 = 0 )

proof end;

theorem :: NAT_2:24

for n being Nat holds
( not n is even iff n mod 2 = 1 )

proof end;

theorem :: NAT_2:25

for n, k, t being Nat st 1 <= t & k <= n & 2 * t divides k holds
( n div t is even iff (n -' k) div t is even )

proof end;

theorem Th26: :: NAT_2:26

for n, m, k being Nat st n <= m holds
n div k <= m div k

proof end;

theorem :: NAT_2:27

for n, k being Nat st k <= 2 * n holds
(k + 1) div 2 <= n

proof end;

theorem :: NAT_2:28

for n being even Nat holds n div 2 = (n + 1) div 2

proof end;

theorem :: NAT_2:29

for n, k, i being Nat holds (n div k) div i = n div (k * i)

proof end;

definition

let n be natural number ;
redefine attr n is trivial means :Def1: :: NAT_2:def 1
( n = 0 or n = 1 );
compatibility

proof end;

end;

:: deftheorem Def1 defines trivial NAT_2:def 1 :

registration

cluster non trivial Element of K76();
existence

proof end;

cluster natural non trivial set ;
existence

proof end;

end;

theorem :: NAT_2:30

for k being natural number holds
( not k is trivial iff ( not k is empty & k <> 1 ) ) by Def1;

theorem :: NAT_2:31

for k being natural non trivial number holds k >= 2

proof end;

scheme :: NAT_2:sch 2
Indfrom2{ P₁[ Nat] } :

for k being non trivial Nat holds P₁[k]

provided

A1: P₁[2] and
A2: for k being non trivial Nat st P₁[k] holds
P₁[k + 1]

proof end;