:: NAT_2 semantic presentation

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

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

provided

E1: for b₁ being Nat st 1 <= b₁ & b₁ < F₃() holds
for b₂ being Element of F₁() ex b₃ being Element of F₁() st P₁[b₁,b₂,b₃]

proof end;

theorem Th1: :: NAT_2:1

canceled;

theorem Th2: :: NAT_2:2

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

proof end;

theorem Th3: :: NAT_2:3

canceled;

theorem Th4: :: NAT_2:4

for b₁ being natural number holds 0 div b₁ = 0

proof end;

theorem Th5: :: NAT_2:5

for b₁ being non empty Nat holds b₁ div b₁ = 1

proof end;

theorem Th6: :: NAT_2:6

for b₁ being Nat holds b₁ div 1 = b₁

proof end;

theorem Th7: :: NAT_2:7

for b₁, b₂, b₃, b₄ being natural number st b₁ <= b₂ & b₃ <= b₂ & b₁ = (b₂ -' b₃) + b₄ holds
b₃ = (b₂ -' b₁) + b₄

proof end;

theorem Th8: :: NAT_2:8

for b₁, b₂ being natural number st b₁ in Seg b₂ holds
(b₂ -' b₁) + 1 in Seg b₂

proof end;

theorem Th9: :: NAT_2:9

for b₁, b₂ being natural number st b₂ < b₁ holds
(b₁ -' (b₂ + 1)) + 1 = b₁ -' b₂

proof end;

theorem Th10: :: NAT_2:10

for b₁, b₂ being natural number st b₁ >= b₂ holds
b₂ -' b₁ = 0

proof end;

theorem Th11: :: NAT_2:11

for b₁, b₂ being non empty natural number holds b₁ -' b₂ < b₁

proof end;

theorem Th12: :: NAT_2:12

for b₁, b₂ being natural number st b₂ <= b₁ holds
2 to_power b₁ = (2 to_power b₂) * (2 to_power (b₁ -' b₂))

proof end;

theorem Th13: :: NAT_2:13

for b₁, b₂ being Nat st b₂ <= b₁ holds
2 to_power b₂ divides 2 to_power b₁

proof end;

theorem Th14: :: NAT_2:14

for b₁, b₂ being natural number st b₂ > 0 & b₁ div b₂ = 0 holds
b₁ < b₂

proof end;

theorem Th15: :: NAT_2:15

for b₁, b₂ being natural number st b₁ > 0 & b₁ <= b₂ holds
b₂ div b₁ >= 1

proof end;

theorem Th16: :: NAT_2:16

for b₁, b₂ being natural number st b₁ <> 0 holds
(b₂ + b₁) div b₁ = (b₂ div b₁) + 1

proof end;

theorem Th17: :: NAT_2:17

for b₁, b₂, b₃ being natural number st b₁ divides b₂ & 1 <= b₂ & 1 <= b₃ & b₃ <= b₁ holds
(b₂ -' b₃) div b₁ = (b₂ div b₁) - 1

proof end;

theorem Th18: :: NAT_2:18

for b₁, b₂ being Nat st b₂ <= b₁ holds
(2 to_power b₁) div (2 to_power b₂) = 2 to_power (b₁ -' b₂)

proof end;

theorem Th19: :: NAT_2:19

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

proof end;

theorem Th20: :: NAT_2:20

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

proof end;

theorem Th21: :: NAT_2:21

for b₁ being non empty natural number st b₁ <> 1 holds
b₁ > 1

proof end;

theorem Th22: :: NAT_2:22

for b₁, b₂ being natural number st b₁ <= b₂ & b₂ < b₁ + b₁ holds
b₂ div b₁ = 1

proof end;

theorem Th23: :: NAT_2:23

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

proof end;

theorem Th24: :: NAT_2:24

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

proof end;

theorem Th25: :: NAT_2:25

for b₁, b₂, b₃ being Nat st 1 <= b₃ & b₂ <= b₁ & 2 * b₃ divides b₂ holds
( b₁ div b₃ is even iff (b₁ -' b₂) div b₃ is even )

proof end;

theorem Th26: :: NAT_2:26

for b₁, b₂, b₃ being Nat st b₁ <= b₂ holds
b₁ div b₃ <= b₂ div b₃

proof end;

theorem Th27: :: NAT_2:27

for b₁, b₂ being Nat st b₂ <= 2 * b₁ holds
(b₂ + 1) div 2 <= b₁

proof end;

theorem Th28: :: NAT_2:28

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

proof end;

theorem Th29: :: NAT_2:29

for b₁, b₂, b₃ being Nat holds (b₁ div b₂) div b₃ = b₁ div (b₂ * b₃)

proof end;

definition

let c₁ be natural number ;
redefine attr a₁ is trivial means :Def1: :: NAT_2:def 1
( a₁ = 0 or a₁ = 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 Th30: :: NAT_2:30

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

theorem Th31: :: NAT_2:31

for b₁ being natural non trivial number holds b₁ >= 2

proof end;

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

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

provided

E9: P₁[2] and
E10: for b₁ being non trivial Nat st P₁[b₁] holds
P₁[b₁ + 1]

proof end;