Type  Label  Description 
Statement 

Theorem  avglt2 7901 
Ordering property for average. (Contributed by Mario Carneiro,
28May2014.)



Theorem  avgle1 7902 
Ordering property for average. (Contributed by Mario Carneiro,
28May2014.)



Theorem  avgle2 7903 
Ordering property for average. (Contributed by Jeff Hankins,
15Sep2013.) (Revised by Mario Carneiro, 28May2014.)



Theorem  2timesd 7904 
Two times a number. (Contributed by Mario Carneiro, 27May2016.)



Theorem  times2d 7905 
A number times 2. (Contributed by Mario Carneiro, 27May2016.)



Theorem  halfcld 7906 
Closure of half of a number (frequently used special case).
(Contributed by Mario Carneiro, 27May2016.)



Theorem  2halvesd 7907 
Two halves make a whole. (Contributed by Mario Carneiro,
27May2016.)



Theorem  rehalfcld 7908 
Real closure of half. (Contributed by Mario Carneiro, 27May2016.)



Theorem  lt2halvesd 7909 
A sum is less than the whole if each term is less than half.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  rehalfcli 7910 
Half a real number is real. Inference form. (Contributed by David
Moews, 28Feb2017.)



Theorem  add1p1 7911 
Adding two times 1 to a number. (Contributed by AV, 22Sep2018.)



Theorem  sub1m1 7912 
Subtracting two times 1 from a number. (Contributed by AV,
23Oct2018.)



Theorem  cnm2m1cnm3 7913 
Subtracting 2 and afterwards 1 from a number results in the difference
between the number and 3. (Contributed by Alexander van der Vekens,
16Sep2018.)



3.4.6 The Archimedean property


Theorem  arch 7914* 
Archimedean property of real numbers. For any real number, there is an
integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed
by NM, 21Jan1997.)



Theorem  nnrecl 7915* 
There exists a positive integer whose reciprocal is less than a given
positive real. Exercise 3 of [Apostol]
p. 28. (Contributed by NM,
8Nov2004.)



Theorem  bndndx 7916* 
A bounded real sequence is less than or equal to at least
one of its indices. (Contributed by NM, 18Jan2008.)



3.4.7 Nonnegative integers (as a subset of
complex numbers)


Syntax  cn0 7917 
Extend class notation to include the class of nonnegative integers.



Definition  dfn0 7918 
Define the set of nonnegative integers. (Contributed by Raph Levien,
10Dec2002.)



Theorem  elnn0 7919 
Nonnegative integers expressed in terms of naturals and zero.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nnssnn0 7920 
Positive naturals are a subset of nonnegative integers. (Contributed by
Raph Levien, 10Dec2002.)



Theorem  nn0ssre 7921 
Nonnegative integers are a subset of the reals. (Contributed by Raph
Levien, 10Dec2002.)



Theorem  nn0sscn 7922 
Nonnegative integers are a subset of the complex numbers.) (Contributed
by NM, 9May2004.)



Theorem  nn0ex 7923 
The set of nonnegative integers exists. (Contributed by NM,
18Jul2004.)



Theorem  nnnn0 7924 
A positive integer is a nonnegative integer. (Contributed by NM,
9May2004.)



Theorem  nnnn0i 7925 
A positive integer is a nonnegative integer. (Contributed by NM,
20Jun2005.)



Theorem  nn0re 7926 
A nonnegative integer is a real number. (Contributed by NM,
9May2004.)



Theorem  nn0cn 7927 
A nonnegative integer is a complex number. (Contributed by NM,
9May2004.)



Theorem  nn0rei 7928 
A nonnegative integer is a real number. (Contributed by NM,
14May2003.)



Theorem  nn0cni 7929 
A nonnegative integer is a complex number. (Contributed by NM,
14May2003.)



Theorem  dfn2 7930 
The set of positive integers defined in terms of nonnegative integers.
(Contributed by NM, 23Sep2007.) (Proof shortened by Mario Carneiro,
13Feb2013.)



Theorem  elnnne0 7931 
The positive integer property expressed in terms of difference from zero.
(Contributed by Stefan O'Rear, 12Sep2015.)



Theorem  0nn0 7932 
0 is a nonnegative integer. (Contributed by Raph Levien, 10Dec2002.)



Theorem  1nn0 7933 
1 is a nonnegative integer. (Contributed by Raph Levien, 10Dec2002.)



Theorem  2nn0 7934 
2 is a nonnegative integer. (Contributed by Raph Levien, 10Dec2002.)



Theorem  3nn0 7935 
3 is a nonnegative integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  4nn0 7936 
4 is a nonnegative integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  5nn0 7937 
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  6nn0 7938 
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  7nn0 7939 
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  8nn0 7940 
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  9nn0 7941 
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  10nn0 7942 
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  nn0ge0 7943 
A nonnegative integer is greater than or equal to zero. (Contributed by
NM, 9May2004.) (Revised by Mario Carneiro, 16May2014.)



Theorem  nn0nlt0 7944 
A nonnegative integer is not less than zero. (Contributed by NM,
9May2004.) (Revised by Mario Carneiro, 27May2016.)



Theorem  nn0ge0i 7945 
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10Dec2002.)



Theorem  nn0le0eq0 7946 
A nonnegative integer is less than or equal to zero iff it is equal to
zero. (Contributed by NM, 9Dec2005.)



Theorem  nn0p1gt0 7947 
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3Oct2018.)



Theorem  nnnn0addcl 7948 
A positive integer plus a nonnegative integer is a positive integer.
(Contributed by NM, 20Apr2005.) (Proof shortened by Mario Carneiro,
16May2014.)



Theorem  nn0nnaddcl 7949 
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22Dec2005.)



Theorem  0mnnnnn0 7950 
The result of subtracting a positive integer from 0 is not a nonnegative
integer. (Contributed by Alexander van der Vekens, 19Mar2018.)



Theorem  un0addcl 7951 
If is closed under
addition, then so is
.
(Contributed by Mario Carneiro, 17Jul2014.)



Theorem  un0mulcl 7952 
If is closed under
multiplication, then so is .
(Contributed by Mario Carneiro, 17Jul2014.)



Theorem  nn0addcl 7953 
Closure of addition of nonnegative integers. (Contributed by Raph Levien,
10Dec2002.) (Proof shortened by Mario Carneiro, 17Jul2014.)



Theorem  nn0mulcl 7954 
Closure of multiplication of nonnegative integers. (Contributed by NM,
22Jul2004.) (Proof shortened by Mario Carneiro, 17Jul2014.)



Theorem  nn0addcli 7955 
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0mulcli 7956 
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0p1nn 7957 
A nonnegative integer plus 1 is a positive integer. (Contributed by Raph
Levien, 30Jun2006.) (Revised by Mario Carneiro, 16May2014.)



Theorem  peano2nn0 7958 
Second Peano postulate for nonnegative integers. (Contributed by NM,
9May2004.)



Theorem  nnm1nn0 7959 
A positive integer minus 1 is a nonnegative integer. (Contributed by
Jason Orendorff, 24Jan2007.) (Revised by Mario Carneiro,
16May2014.)



Theorem  elnn0nn 7960 
The nonnegative integer property expressed in terms of positive integers.
(Contributed by NM, 10May2004.) (Proof shortened by Mario Carneiro,
16May2014.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nn0ge2m1nn 7978 
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 7979 
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 7980 
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 7981 
Extend class notation to include the class of integers.



Definition  dfz 7982 
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 7983 
Membership in the set of integers. (Contributed by NM, 8Jan2002.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

