:: by Grzegorz Bancerek

::

:: Received January 11, 1989

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

registration
end;

:: The results of axioms of Nats

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;

:: Addition and multiplication

:: The Nats are real numbers therefore some theorems of real

:: numbers are translated for Nats.

:: The Nats are real numbers therefore some theorems of real

:: numbers are translated for Nats.

registration
end;

definition

let n be natural Number ;

let k be Element of NAT ;

:: original: +

redefine func n + k -> Element of NAT ;

coherence

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

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 12;

reconsider N = NAT as Subset of REAL by NUMBERS:19;

canceled;

:: Like addition, the result of multiplication of two Nats is a Nat.

registration
end;

definition

let n, k be Element of NAT ;

:: original: *

redefine func n * k -> Element of NAT ;

coherence

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

end;
:: original: *

redefine func n * k -> Element of NAT ;

coherence

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

:: Order relation ::

:: Some theorems of not great relation "<=" in real numbers are translated

:: to Nat easy and it is necessary to have them here.

:: Some theorems of not great relation "<=" in real numbers are translated

:: to Nat easy and it is necessary to have them here.

registration

existence

ex b_{1} being object st

( b_{1} is zero & b_{1} is natural )

ex b_{1} being object st

( not b_{1} is zero & b_{1} is natural )

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

registration

let m be natural Number ;

let n be natural non zero Number ;

coherence

not m + n is zero by Th7;

coherence

not n + m is zero ;

end;
let n be natural non zero Number ;

coherence

not m + n is zero by Th7;

coherence

not n + m is zero ;

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;

:: Exact division and rest of division

theorem :: NAT_1:18

for n, m, k, t, k1, t1 being natural Number 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;

:: from ALGSEQ_1

registration

not for b_{1} being Element of NAT holds b_{1} is zero
end;

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

existence not for b

proof end;

:: from JORDAN4

:: Moved from CQC_THE1 on 07.07.2006 by AK

:: from HENMODEL, 2007.03.15, A.T.

definition

let A be set ;

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

( ( 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_{2} being Element of NAT holds

( ( A is non empty Subset of NAT implies ( b_{2} = min* A iff ( b_{2} in A & ( for k being Nat st k in A holds

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

for A being set

for b

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

b

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

:: from CARD_1, 2007.10.28,A.T.

::$CT 12

canceled;

::$CD

::$CT

:: from MODELC_2, 2008.08.18, A.T.

:: from MODELC_2, 2008.08.18, A.T.

scheme :: NAT_1:sch 13

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

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}[ object , object , object ], F_{3}() -> sequence of F_{1}(), F_{4}() -> sequence of 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}() -> object , F_{2}( object , object ) -> object , 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}( object , object ) -> Element of F_{1}(), F_{4}() -> sequence of F_{1}(), F_{5}() -> sequence of 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;

:: missing, 2008.02.22, A.T.

registration

let x, y be natural Number ;

coherence

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

coherence

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

end;
coherence

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

coherence

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

definition

let x, y be Element of NAT ;

:: original: min

redefine func min (x,y) -> Element of NAT ;

coherence

min (x,y) is Element of NAT by XXREAL_0:15;

:: original: max

redefine func max (x,y) -> Element of NAT ;

coherence

max (x,y) is Element of NAT by XXREAL_0:16;

end;
:: original: min

redefine func min (x,y) -> Element of NAT ;

coherence

min (x,y) is Element of NAT by XXREAL_0:15;

:: original: max

redefine func max (x,y) -> Element of NAT ;

coherence

max (x,y) is Element of NAT by XXREAL_0:16;

:: from SEQM_3, BHSP_3, COMSEQ_3, KURATO_2, LOPBAN_3, CLVECT_2, CLOPBAN3

:: (generalized), 2008.08.23, A.T.

:: (generalized), 2008.08.23, A.T.

definition

let s be ManySortedSet of NAT ;

let k be natural Number ;

ex b_{1} being ManySortedSet of NAT st

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

for b_{1}, b_{2} being ManySortedSet of NAT 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 k be natural Number ;

func s ^\ k -> ManySortedSet of NAT means :Def2: :: NAT_1:def 2

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

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

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines ^\ NAT_1:def 2 :

for s being ManySortedSet of NAT

for k being natural Number

for b_{3} being ManySortedSet of NAT holds

( b_{3} = s ^\ k iff for n being Nat holds b_{3} . n = s . (n + k) );

for s being ManySortedSet of NAT

for k being natural Number

for b

( b

Lm1: for s being ManySortedSet of NAT

for k being natural Number holds rng (s ^\ k) c= rng s

proof end;

registration

let X be non empty set ;

let s be X -valued ManySortedSet of NAT ;

let k be natural Number ;

coherence

s ^\ k is X -valued

end;
let s be X -valued ManySortedSet of NAT ;

let k be natural Number ;

coherence

s ^\ k is X -valued

proof end;

definition

let X be non empty set ;

let s be sequence of X;

let k be Nat;

:: original: ^\

redefine func s ^\ k -> sequence of X;

coherence

s ^\ k is sequence of X

end;
let s be sequence of X;

let k be Nat;

:: original: ^\

redefine func s ^\ k -> sequence of X;

coherence

s ^\ k is sequence of X

proof end;

theorem Th35: :: NAT_1:48

for k, m being Nat

for X being non empty set

for s being sequence of X holds (s ^\ k) ^\ m = s ^\ (k + m)

for X being non empty set

for s being sequence of X holds (s ^\ k) ^\ m = s ^\ (k + m)

proof end;

theorem :: NAT_1:49

for k, m being Nat

for X being non empty set

for s being sequence of X holds (s ^\ k) ^\ m = (s ^\ m) ^\ k

for X being non empty set

for s being sequence of X holds (s ^\ k) ^\ m = (s ^\ m) ^\ k

proof end;

registration

let N be sequence of NAT;

let X be non empty set ;

let s be sequence of X;

coherence

( s * N is Function-like & s * N is NAT -defined & s * N is X -valued ) ;

end;
let X be non empty set ;

let s be sequence of X;

coherence

( s * N is Function-like & s * N is NAT -defined & s * N is X -valued ) ;

registration
end;

theorem :: NAT_1:50

for k being Nat

for X being non empty set

for s being sequence of X

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

for X being non empty set

for s being sequence of X

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

proof end;

theorem :: NAT_1:52

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;

:: from UPROOTS, 2009.07.21, A.T.

registration
end;

registration
end;

theorem :: NAT_1:55

:: from GLIB_002, 2011.07.30, A.T.

::$CT 3

::$CT 3

definition

let D be set ;

let s be sequence of D;

let n be natural Number ;

:: original: .

redefine func s . n -> Element of D;

coherence

s . n is Element of D

end;
let s be sequence of D;

let n be natural Number ;

:: original: .

redefine func s . n -> Element of D;

coherence

s . n is Element of D

proof end;

registration
end;

registration

let A be non zero object ;

coherence

{A} is with_non-empty_elements by TARSKI:def 1;

let B be non zero object ;

coherence

{A,B} is with_non-empty_elements by TARSKI:def 2;

let C be non zero object ;

coherence

{A,B,C} is with_non-empty_elements by ENUMSET1:def 1;

let D be non zero object ;

coherence

{A,B,C,D} is with_non-empty_elements by ENUMSET1:def 2;

let E be non zero object ;

coherence

{A,B,C,D,E} is with_non-empty_elements by ENUMSET1:def 3;

let F be non zero object ;

coherence

{A,B,C,D,E,F} is with_non-empty_elements by ENUMSET1:def 4;

let G be non zero object ;

coherence

{A,B,C,D,E,F,G} is with_non-empty_elements by ENUMSET1:def 5;

let H be non zero object ;

coherence

{A,B,C,D,E,F,G,H} is with_non-empty_elements by ENUMSET1:def 6;

let I be non zero object ;

coherence

{A,B,C,D,E,F,G,H,I} is with_non-empty_elements by ENUMSET1:def 7;

let J be non zero object ;

coherence

{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements by ENUMSET1:def 8;

end;
coherence

{A} is with_non-empty_elements by TARSKI:def 1;

let B be non zero object ;

coherence

{A,B} is with_non-empty_elements by TARSKI:def 2;

let C be non zero object ;

coherence

{A,B,C} is with_non-empty_elements by ENUMSET1:def 1;

let D be non zero object ;

coherence

{A,B,C,D} is with_non-empty_elements by ENUMSET1:def 2;

let E be non zero object ;

coherence

{A,B,C,D,E} is with_non-empty_elements by ENUMSET1:def 3;

let F be non zero object ;

coherence

{A,B,C,D,E,F} is with_non-empty_elements by ENUMSET1:def 4;

let G be non zero object ;

coherence

{A,B,C,D,E,F,G} is with_non-empty_elements by ENUMSET1:def 5;

let H be non zero object ;

coherence

{A,B,C,D,E,F,G,H} is with_non-empty_elements by ENUMSET1:def 6;

let I be non zero object ;

coherence

{A,B,C,D,E,F,G,H,I} is with_non-empty_elements by ENUMSET1:def 7;

let J be non zero object ;

coherence

{A,B,C,D,E,F,G,H,I,J} is with_non-empty_elements by ENUMSET1:def 8;

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is zero
;

coherence

for b_{1} being set st not b_{1} is zero holds

not b_{1} is empty
;

end;
for b

b

coherence

for b

not b

definition

let G be non empty set ;

let B be Function of [:G,NAT:],G;

let g be Element of G;

let i be Nat;

:: original: .

redefine func B . (g,i) -> Element of G;

coherence

B . (g,i) is Element of G

end;
let B be Function of [:G,NAT:],G;

let g be Element of G;

let i be Nat;

:: original: .

redefine func B . (g,i) -> Element of G;

coherence

B . (g,i) is Element of G

proof end;

definition

let G be non empty set ;

let B be Function of [:NAT,G:],G;

let i be Nat;

let g be Element of G;

:: original: .

redefine func B . (i,g) -> Element of G;

coherence

B . (i,g) is Element of G

end;
let B be Function of [:NAT,G:],G;

let i be Nat;

let g be Element of G;

:: original: .

redefine func B . (i,g) -> Element of G;

coherence

B . (i,g) is Element of G

proof end;