:: by Grzegorz Bancerek

::

:: Received January 11, 1989

:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem Th1: :: NAT_1:1

for X being Subset of REAL st 0 in X & ( for x being Real st x in X holds

x + 1 in X ) holds

for n being Nat holds n in X

x + 1 in X ) holds

for n being Nat holds n in X

proof end;

definition

let n be Nat;

let k be Element of NAT ;

:: original: +

redefine func n + k -> Element of NAT ;

coherence

n + k is Element of NAT by ORDINAL1:def 13;

end;
let k be Element of NAT ;

:: original: +

redefine func n + k -> Element of NAT ;

coherence

n + k is Element of NAT by ORDINAL1:def 13;

definition

let n be Element of NAT ;

let k be Nat;

:: original: +

redefine func n + k -> Element of NAT ;

coherence

n + k is Element of NAT by ORDINAL1:def 13;

end;
let k be Nat;

:: original: +

redefine func n + k -> Element of NAT ;

coherence

n + k is Element of NAT by ORDINAL1:def 13;

definition

let n be Nat;

let k be Element of NAT ;

:: original: *

redefine func n * k -> Element of NAT ;

coherence

n * k is Element of NAT by ORDINAL1:def 13;

end;
let k be Element of NAT ;

:: original: *

redefine func n * k -> Element of NAT ;

coherence

n * k is Element of NAT by ORDINAL1:def 13;

definition

let n be Element of NAT ;

let k be Nat;

:: original: *

redefine func n * k -> Element of NAT ;

coherence

n * k is Element of NAT by ORDINAL1:def 13;

end;
let k be Nat;

:: original: *

redefine func n * k -> Element of NAT ;

coherence

n * k is Element of NAT by ORDINAL1:def 13;

theorem Th2: :: NAT_1:2

proof end;

theorem :: NAT_1:3

theorem :: NAT_1:4

proof end;

theorem :: NAT_1:5

proof end;

theorem Th6: :: NAT_1:6

proof end;

theorem Th7: :: NAT_1:7

proof end;

registration

cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set ;

existence

not for b_{1} being Nat holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let m be Nat;

let n be non zero Nat;

cluster m + n -> non zero ;

coherence

not m + n is empty by Th7;

cluster n + m -> non zero ;

coherence

not n + m is empty ;

end;
let n be non zero Nat;

cluster m + n -> non zero ;

coherence

not m + n is empty by Th7;

cluster n + m -> non zero ;

coherence

not n + m is empty ;

scheme :: NAT_1:sch 3

DefbyInd{ F_{1}() -> Nat, F_{2}( Nat, Nat) -> Nat, P_{1}[ Nat, Nat] } :

DefbyInd{ F

( ( for k being Nat ex n being Nat st P_{1}[k,n] ) & ( for k, n, m being Nat st P_{1}[k,n] & P_{1}[k,m] holds

n = m ) )

providedn = m ) )

A1:
for k, n being Nat holds

( P_{1}[k,n] iff ( ( k = 0 & n = F_{1}() ) or ex m, l being Nat st

( k = m + 1 & P_{1}[m,l] & n = F_{2}(k,l) ) ) )

( P

( k = m + 1 & P

proof end;

theorem Th8: :: NAT_1:8

proof end;

theorem :: NAT_1:9

proof end;

theorem Th10: :: NAT_1:10

proof end;

theorem Th11: :: NAT_1:11

proof end;

theorem Th12: :: NAT_1:12

proof end;

theorem Th13: :: NAT_1:13

proof end;

theorem Th14: :: NAT_1:14

proof end;

theorem :: NAT_1:15

proof end;

theorem Th16: :: NAT_1:16

proof end;

scheme :: NAT_1:sch 7

Regr{ P_{1}[ Nat] } :

provided

Regr{ P

provided

A1:
ex k being Nat st P_{1}[k]
and

A2: for k being Nat st k <> 0 & P_{1}[k] holds

ex n being Nat st

( n < k & P_{1}[n] )

A2: for k being Nat st k <> 0 & P

ex n being Nat st

( n < k & P

proof end;

theorem :: NAT_1:17

proof end;

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 )

( k = k1 & t = t1 )

proof end;

registration
end;

registration

cluster non empty ordinal Element of K6(REAL);

existence

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is ordinal )

end;
existence

ex b

( not b

proof end;

theorem :: NAT_1:19

proof end;

theorem :: NAT_1:20

proof end;

theorem :: NAT_1:21

proof end;

begin

theorem Th22: :: NAT_1:22

proof end;

theorem :: NAT_1:23

proof end;

registration

cluster non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT ;

existence

not for b_{1} being Element of NAT holds b_{1} is empty

end;
existence

not for b

proof end;

registration

cluster -> non negative Element of NAT ;

coherence

for b_{1} being Element of NAT holds not b_{1} is negative
by Th2;

end;
coherence

for b

registration

cluster natural -> non negative set ;

coherence

for b_{1} being Nat holds not b_{1} is negative
by Th2;

end;
coherence

for b

theorem :: NAT_1:24

proof end;

theorem :: NAT_1:25

canceled;

scheme :: NAT_1:sch 9

CompInd1{ F_{1}() -> Nat, P_{1}[ Nat] } :

provided

CompInd1{ F

provided

A1:
for k being Nat st k >= F_{1}() & ( for n being Nat st n >= F_{1}() & n < k holds

P_{1}[n] ) holds

P_{1}[k]

P

P

proof end;

theorem Th26: :: NAT_1:26

proof end;

theorem Th27: :: NAT_1:27

proof end;

theorem Th28: :: NAT_1:28

proof end;

theorem Th29: :: NAT_1:29

proof end;

theorem Th30: :: NAT_1:30

proof end;

theorem Th31: :: NAT_1:31

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

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 )

( 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 )

proof end;

definition

let A be set ;

func min* A -> Element of NAT means :Def1: :: NAT_1:def 1

( it in A & ( for k being Nat st k in A holds

it <= k ) ) if A is non empty Subset of NAT

otherwise it = 0 ;

existence

( ( A is non empty Subset of NAT implies ex b_{1} being Element of NAT st

( b_{1} in A & ( for k being Nat st k in A holds

b_{1} <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b_{1} being Element of NAT st b_{1} = 0 ) )

for b_{1}, b_{2} being Element of NAT holds

( ( A is non empty Subset of NAT & b_{1} in A & ( for k being Nat st k in A holds

b_{1} <= k ) & b_{2} in A & ( for k being Nat st k in A holds

b_{2} <= k ) implies b_{1} = b_{2} ) & ( A is not non empty Subset of NAT & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Element of NAT holds verum
;

end;
func min* A -> Element of NAT means :Def1: :: NAT_1:def 1

( it in A & ( for k being Nat st k in A holds

it <= k ) ) if A is non empty Subset of NAT

otherwise it = 0 ;

existence

( ( A is non empty Subset of NAT implies ex b

( b

b

proof end;

uniqueness for b

( ( A is non empty Subset of NAT & b

b

b

proof end;

consistency for b

:: deftheorem Def1 defines min* NAT_1:def 1 :

for A being set

for b

( ( A is non empty Subset of NAT implies ( b

b

theorem Th39: :: NAT_1:39

proof end;

theorem Th40: :: NAT_1:40

proof end;

theorem Th41: :: NAT_1:41

proof end;

theorem Th42: :: NAT_1:42

proof end;

theorem :: NAT_1:43

proof end;

definition

let n be natural number ;

redefine func succ n equals :: NAT_1:def 2

n + 1;

compatibility

for b_{1} being set holds

( b_{1} = succ n iff b_{1} = n + 1 )
by Th39;

end;
redefine func succ n equals :: NAT_1:def 2

n + 1;

compatibility

for b

( b

:: deftheorem defines succ NAT_1:def 2 :

for n being natural number holds succ n = n + 1;

theorem :: NAT_1:44

proof end;

theorem :: NAT_1:45

proof end;

theorem :: NAT_1:46

proof end;

theorem :: NAT_1:47

proof end;

scheme :: NAT_1:sch 11

LambdaRecEx{ F_{1}() -> set , F_{2}( set , set ) -> set } :

LambdaRecEx{ F

ex f being Function st

( dom f = NAT & f . 0 = F_{1}() & ( for n being Nat holds f . (n + 1) = F_{2}(n,(f . n)) ) )

( dom f = NAT & f . 0 = F

proof end;

scheme :: NAT_1:sch 12

LambdaRecExD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( set , set ) -> Element of F_{1}() } :

LambdaRecExD{ F

ex f being Function of NAT,F_{1}() st

( f . 0 = F_{2}() & ( for n being Nat holds f . (n + 1) = F_{3}(n,(f . n)) ) )

( f . 0 = F

proof end;

scheme :: NAT_1:sch 13

RecUn{ F_{1}() -> set , F_{2}() -> Function, F_{3}() -> Function, P_{1}[ set , set , set ] } :

provided

RecUn{ F

provided

A1:
dom F_{2}() = NAT
and

A2: F_{2}() . 0 = F_{1}()
and

A3: for n being Nat holds P_{1}[n,F_{2}() . n,F_{2}() . (n + 1)]
and

A4: dom F_{3}() = NAT
and

A5: F_{3}() . 0 = F_{1}()
and

A6: for n being Nat holds P_{1}[n,F_{3}() . n,F_{3}() . (n + 1)]
and

A7: for n being Nat

for x, y1, y2 being set st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2

A2: F

A3: for n being Nat holds P

A4: dom F

A5: F

A6: for n being Nat holds P

A7: for n being Nat

for x, y1, y2 being set st P

y1 = y2

proof end;

scheme :: NAT_1:sch 14

RecUnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), P_{1}[ set , set , set ], F_{3}() -> Function of NAT,F_{1}(), F_{4}() -> Function of NAT,F_{1}() } :

provided

RecUnD{ F

provided

A1:
F_{3}() . 0 = F_{2}()
and

A2: for n being Nat holds P_{1}[n,F_{3}() . n,F_{3}() . (n + 1)]
and

A3: F_{4}() . 0 = F_{2}()
and

A4: for n being Nat holds P_{1}[n,F_{4}() . n,F_{4}() . (n + 1)]
and

A5: for n being Nat

for x, y1, y2 being Element of F_{1}() st P_{1}[n,x,y1] & P_{1}[n,x,y2] holds

y1 = y2

A2: for n being Nat holds P

A3: F

A4: for n being Nat holds P

A5: for n being Nat

for x, y1, y2 being Element of F

y1 = y2

proof end;

scheme :: NAT_1:sch 15

LambdaRecUn{ F_{1}() -> set , F_{2}( set , set ) -> set , F_{3}() -> Function, F_{4}() -> Function } :

provided

LambdaRecUn{ F

provided

A1:
dom F_{3}() = NAT
and

A2: F_{3}() . 0 = F_{1}()
and

A3: for n being Nat holds F_{3}() . (n + 1) = F_{2}(n,(F_{3}() . n))
and

A4: dom F_{4}() = NAT
and

A5: F_{4}() . 0 = F_{1}()
and

A6: for n being Nat holds F_{4}() . (n + 1) = F_{2}(n,(F_{4}() . n))

A2: F

A3: for n being Nat holds F

A4: dom F

A5: F

A6: for n being Nat holds F

proof end;

scheme :: NAT_1:sch 16

LambdaRecUnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}( set , set ) -> Element of F_{1}(), F_{4}() -> Function of NAT,F_{1}(), F_{5}() -> Function of NAT,F_{1}() } :

provided

LambdaRecUnD{ F

provided

A1:
F_{4}() . 0 = F_{2}()
and

A2: for n being Nat holds F_{4}() . (n + 1) = F_{3}(n,(F_{4}() . n))
and

A3: F_{5}() . 0 = F_{2}()
and

A4: for n being Nat holds F_{5}() . (n + 1) = F_{3}(n,(F_{5}() . n))

A2: for n being Nat holds F

A3: F

A4: for n being Nat holds F

proof end;

registration

let x, y be Nat;

cluster min (x,y) -> natural ;

coherence

min (x,y) is natural by XXREAL_0:15;

cluster max (x,y) -> natural ;

coherence

max (x,y) is natural by XXREAL_0:16;

end;
cluster min (x,y) -> natural ;

coherence

min (x,y) is natural by XXREAL_0:15;

cluster max (x,y) -> natural ;

coherence

max (x,y) is natural by XXREAL_0:16;

definition

let D be set ;

let f be Function of NAT,D;

let n be Nat;

:: original: .

redefine func f . n -> Element of D;

coherence

f . n is Element of D

end;
let f be Function of NAT,D;

let n be Nat;

:: original: .

redefine func f . n -> Element of D;

coherence

f . n is Element of D

proof end;

definition

let X be non empty set ;

let s be sequence of X;

let k be Nat;

func s ^\ k -> sequence of X means :Def3: :: NAT_1:def 3

for n being Nat holds it . n = s . (n + k);

existence

ex b_{1} being sequence of X st

for n being Nat holds b_{1} . n = s . (n + k)

for b_{1}, b_{2} being sequence of X st ( for n being Nat holds b_{1} . n = s . (n + k) ) & ( for n being Nat holds b_{2} . n = s . (n + k) ) holds

b_{1} = b_{2}

end;
let s be sequence of X;

let k be Nat;

func s ^\ k -> sequence of X means :Def3: :: NAT_1:def 3

for n being Nat holds it . n = s . (n + k);

existence

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines ^\ NAT_1:def 3 :

for X being non empty set

for s being sequence of X

for k being Nat

for b

( b

theorem :: NAT_1:48

proof end;

theorem Th49: :: NAT_1:49

for X being non empty set

for s being sequence of X

for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)

for s being sequence of X

for k, m being Nat holds (s ^\ k) ^\ m = s ^\ (k + m)

proof end;

theorem :: NAT_1:50

for X being non empty set

for s being sequence of X

for k, m being Nat holds (s ^\ k) ^\ m = (s ^\ m) ^\ k

for s being sequence of X

for k, m being Nat holds (s ^\ k) ^\ m = (s ^\ m) ^\ k

proof end;

theorem :: NAT_1:51

for X being non empty set

for s being sequence of X

for k being Nat

for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)

for s being sequence of X

for k being Nat

for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)

proof end;

theorem :: NAT_1:52

proof end;

theorem :: NAT_1:53

for Y being set

for X being non empty set

for s being sequence of X st ( for n being Nat holds s . n in Y ) holds

rng s c= Y

for X being non empty set

for s being sequence of X st ( for n being Nat holds s . n in Y ) holds

rng s c= Y

proof end;

theorem :: NAT_1:54

proof end;

theorem :: NAT_1:55

proof end;

scheme :: NAT_1:sch 18

MinPred{ F_{1}( Element of NAT ) -> Element of NAT , P_{1}[ set ] } :

provided

MinPred{ F

provided

proof end;

registration

let k be Ordinal;

let x be set ;

cluster k --> x -> T-Sequence-like ;

coherence

k --> x is T-Sequence-like

end;
let x be set ;

cluster k --> x -> T-Sequence-like ;

coherence

k --> x is T-Sequence-like

proof end;