Type  Label  Description 
Statement 

Theorem  elnnnn0 8001 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10May2004.)



Theorem  elnnnn0b 8002 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1Sep2005.)



Theorem  elnnnn0c 8003 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10Jan2006.)



Theorem  nn0addge1 8004 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge2 8005 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge1i 8006 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge2i 8007 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0le2xi 8008 
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0lele2xi 8009 
'Less than or equal to' implies 'less than or equal to twice' for
nonnegative integers. (Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0supp 8010 
Two ways to write the support of a function on . (Contributed by
Mario Carneiro, 29Dec2014.)



Theorem  nnnn0d 8011 
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  nn0red 8012 
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27May2016.)



Theorem  nn0cnd 8013 
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  nn0ge0d 8014 
A nonnegative integer is greater than or equal to zero. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  nn0addcld 8015 
Closure of addition of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  nn0mulcld 8016 
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  nn0readdcl 8017 
Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6Apr2018.)



Theorem  nn0ge2m1nn 8018 
If a nonnegative integer is greater than or equal to two, the integer
decreased by 1 is a positive integer. (Contributed by Alexander van der
Vekens, 1Aug2018.) (Revised by AV, 4Jan2020.)



Theorem  nn0ge2m1nn0 8019 
If a nonnegative integer is greater than or equal to two, the integer
decreased by 1 is also a nonnegative integer. (Contributed by Alexander
van der Vekens, 1Aug2018.)



Theorem  nn0nndivcl 8020 
Closure law for dividing of a nonnegative integer by a positive integer.
(Contributed by Alexander van der Vekens, 14Apr2018.)



3.4.8 Integers (as a subset of complex
numbers)


Syntax  cz 8021 
Extend class notation to include the class of integers.



Definition  dfz 8022 
Define the set of integers, which are the positive and negative integers
together with zero. Definition of integers in [Apostol] p. 22. The
letter Z abbreviates the German word Zahlen meaning "numbers."
(Contributed by NM, 8Jan2002.)



Theorem  elz 8023 
Membership in the set of integers. (Contributed by NM, 8Jan2002.)



Theorem  nnnegz 8024 
The negative of a positive integer is an integer. (Contributed by NM,
12Jan2002.)



Theorem  zre 8025 
An integer is a real. (Contributed by NM, 8Jan2002.)



Theorem  zcn 8026 
An integer is a complex number. (Contributed by NM, 9May2004.)



Theorem  zrei 8027 
An integer is a real number. (Contributed by NM, 14Jul2005.)



Theorem  zssre 8028 
The integers are a subset of the reals. (Contributed by NM,
2Aug2004.)



Theorem  zsscn 8029 
The integers are a subset of the complex numbers. (Contributed by NM,
2Aug2004.)



Theorem  zex 8030 
The set of integers exists. (Contributed by NM, 30Jul2004.) (Revised
by Mario Carneiro, 17Nov2014.)



Theorem  elnnz 8031 
Positive integer property expressed in terms of integers. (Contributed by
NM, 8Jan2002.)



Theorem  0z 8032 
Zero is an integer. (Contributed by NM, 12Jan2002.)



Theorem  0zd 8033 
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8Dec2018.)



Theorem  elnn0z 8034 
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9May2004.)



Theorem  elznn0nn 8035 
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10May2004.)



Theorem  elznn0 8036 
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9May2004.)



Theorem  elznn 8037 
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12Jul2005.)



Theorem  nnssz 8038 
Positive integers are a subset of integers. (Contributed by NM,
9Jan2002.)



Theorem  nn0ssz 8039 
Nonnegative integers are a subset of the integers. (Contributed by NM,
9May2004.)



Theorem  nnz 8040 
A positive integer is an integer. (Contributed by NM, 9May2004.)



Theorem  nn0z 8041 
A nonnegative integer is an integer. (Contributed by NM, 9May2004.)



Theorem  nnzi 8042 
A positive integer is an integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  nn0zi 8043 
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  elnnz1 8044 
Positive integer property expressed in terms of integers. (Contributed by
NM, 10May2004.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nnzrab 8045 
Positive integers expressed as a subset of integers. (Contributed by NM,
3Oct2004.)



Theorem  nn0zrab 8046 
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3Oct2004.)



Theorem  1z 8047 
One is an integer. (Contributed by NM, 10May2004.)



Theorem  1zzd 8048 
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6Dec2018.)



Theorem  2z 8049 
Two is an integer. (Contributed by NM, 10May2004.)



Theorem  3z 8050 
3 is an integer. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  4z 8051 
4 is an integer. (Contributed by BJ, 26Mar2020.)



Theorem  znegcl 8052 
Closure law for negative integers. (Contributed by NM, 9May2004.)



Theorem  neg1z 8053 
1 is an integer (common case). (Contributed by David A. Wheeler,
5Dec2018.)



Theorem  znegclb 8054 
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13Sep2014.)



Theorem  nn0negz 8055 
The negative of a nonnegative integer is an integer. (Contributed by NM,
9May2004.)



Theorem  nn0negzi 8056 
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18Feb2014.)



Theorem  peano2z 8057 
Second Peano postulate generalized to integers. (Contributed by NM,
13Feb2005.)



Theorem  zaddcllempos 8058 
Lemma for zaddcl 8061. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14Mar2020.)



Theorem  peano2zm 8059 
"Reverse" second Peano postulate for integers. (Contributed by NM,
12Sep2005.)



Theorem  zaddcllemneg 8060 
Lemma for zaddcl 8061. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14Mar2020.)



Theorem  zaddcl 8061 
Closure of addition of integers. (Contributed by NM, 9May2004.) (Proof
shortened by Mario Carneiro, 16May2014.)



Theorem  zsubcl 8062 
Closure of subtraction of integers. (Contributed by NM, 11May2004.)



Theorem  ztri3or0 8063 
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14Mar2020.)



Theorem  ztri3or 8064 
Integer trichotomy. (Contributed by Jim Kingdon, 14Mar2020.)



Theorem  zletric 8065 
Trichotomy law. (Contributed by Jim Kingdon, 27Mar2020.)



Theorem  zlelttric 8066 
Trichotomy law. (Contributed by Jim Kingdon, 17Apr2020.)



Theorem  zltnle 8067 
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14Mar2020.)



Theorem  zleloe 8068 
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8Apr2020.)



Theorem  znnnlt1 8069 
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13Jul2005.)



Theorem  zletr 8070 
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3Apr2018.)



Theorem  zrevaddcl 8071 
Reverse closure law for addition of integers. (Contributed by NM,
11May2004.)



Theorem  znnsub 8072 
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 7733.) (Contributed by NM, 11May2004.)



Theorem  zmulcl 8073 
Closure of multiplication of integers. (Contributed by NM,
30Jul2004.)



Theorem  zltp1le 8074 
Integer ordering relation. (Contributed by NM, 10May2004.) (Proof
shortened by Mario Carneiro, 16May2014.)



Theorem  zleltp1 8075 
Integer ordering relation. (Contributed by NM, 10May2004.)



Theorem  zlem1lt 8076 
Integer ordering relation. (Contributed by NM, 13Nov2004.)



Theorem  zltlem1 8077 
Integer ordering relation. (Contributed by NM, 13Nov2004.)



Theorem  zgt0ge1 8078 
An integer greater than
is greater than or equal to .
(Contributed by AV, 14Oct2018.)



Theorem  nnleltp1 8079 
Positive integer ordering relation. (Contributed by NM, 13Aug2001.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nnltp1le 8080 
Positive integer ordering relation. (Contributed by NM, 19Aug2001.)



Theorem  nnaddm1cl 8081 
Closure of addition of positive integers minus one. (Contributed by NM,
6Aug2003.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0ltp1le 8082 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Dec2002.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0leltp1 8083 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Apr2004.)



Theorem  nn0ltlem1 8084 
Nonnegative integer ordering relation. (Contributed by NM, 10May2004.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  znn0sub 8085 
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8086.) (Contributed by NM, 14Jul2005.)



Theorem  nn0sub 8086 
Subtraction of nonnegative integers. (Contributed by NM, 9May2004.)



Theorem  nn0n0n1ge2 8087 
A nonnegative integer which is neither 0 nor 1 is greater than or equal to
2. (Contributed by Alexander van der Vekens, 6Dec2017.)



Theorem  elz2 8088* 
Membership in the set of integers. Commonly used in constructions of
the integers as equivalence classes under subtraction of the positive
integers. (Contributed by Mario Carneiro, 16May2014.)



Theorem  dfz2 8089 
Alternative definition of the integers, based on elz2 8088.
(Contributed
by Mario Carneiro, 16May2014.)



Theorem  nn0sub2 8090 
Subtraction of nonnegative integers. (Contributed by NM, 4Sep2005.)



Theorem  zapne 8091 
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14Mar2020.)

# 

Theorem  zdceq 8092 
Equality of integers is decidable. (Contributed by Jim Kingdon,
14Mar2020.)

DECID


Theorem  zdcle 8093 
Integer is
decidable. (Contributed by Jim Kingdon, 7Apr2020.)

DECID 

Theorem  zdclt 8094 
Integer is
decidable. (Contributed by Jim Kingdon, 1Jun2020.)

DECID 

Theorem  zltlen 8095 
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7413 which is a similar result for complex
numbers. (Contributed
by Jim Kingdon, 14Mar2020.)



Theorem  nn0n0n1ge2b 8096 
A nonnegative integer is neither 0 nor 1 if and only if it is greater than
or equal to 2. (Contributed by Alexander van der Vekens, 17Jan2018.)



Theorem  nn0lt10b 8097 
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22Jun2011.)



Theorem  nn0lt2 8098 
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16Sep2018.)



Theorem  nn0lem1lt 8099 
Nonnegative integer ordering relation. (Contributed by NM,
21Jun2005.)



Theorem  nnlem1lt 8100 
Positive integer ordering relation. (Contributed by NM, 21Jun2005.)

