Type  Label  Description 
Statement 

Theorem  8lt10 7901 
8 is less than 10. (Contributed by Mario Carneiro, 8Feb2015.)



Theorem  7lt10 7902 
7 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  6lt10 7903 
6 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  5lt10 7904 
5 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  4lt10 7905 
4 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  3lt10 7906 
3 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  2lt10 7907 
2 is less than 10. (Contributed by Mario Carneiro, 10Mar2015.)



Theorem  1lt10 7908 
1 is less than 10. (Contributed by NM, 7Nov2012.) (Revised by Mario
Carneiro, 9Mar2015.)



Theorem  0ne2 7909 
0 is not equal to 2. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  1ne2 7910 
1 is not equal to 2. (Contributed by NM, 19Oct2012.)



Theorem  1le2 7911 
1 is less than or equal to 2 (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  2cnne0 7912 
2 is a nonzero complex number (common case). (Contributed by David A.
Wheeler, 7Dec2018.)



Theorem  2rene0 7913 
2 is a nonzero real number (common case). (Contributed by David A.
Wheeler, 8Dec2018.)



Theorem  1le3 7914 
1 is less than or equal to 3. (Contributed by David A. Wheeler,
8Dec2018.)



Theorem  neg1mulneg1e1 7915 
is
1 (common case). (Contributed by David A. Wheeler,
8Dec2018.)



Theorem  halfre 7916 
Onehalf is real. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  halfcn 7917 
Onehalf is complex. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  halfgt0 7918 
Onehalf is greater than zero. (Contributed by NM, 24Feb2005.)



Theorem  halflt1 7919 
Onehalf is less than one. (Contributed by NM, 24Feb2005.)



Theorem  1mhlfehlf 7920 
Prove that 1  1/2 = 1/2. (Contributed by David A. Wheeler,
4Jan2017.)



Theorem  8th4div3 7921 
An eighth of four thirds is a sixth. (Contributed by Paul Chapman,
24Nov2007.)



Theorem  halfpm6th 7922 
One half plus or minus one sixth. (Contributed by Paul Chapman,
17Jan2008.)



Theorem  it0e0 7923 
i times 0 equals 0 (common case). (Contributed by David A. Wheeler,
8Dec2018.)



Theorem  2mulicn 7924 
(common case). (Contributed by David
A. Wheeler,
8Dec2018.)



Theorem  iap0 7925 
The imaginary unit
is apart from zero. (Contributed by Jim
Kingdon, 9Mar2020.)

# 

Theorem  2muliap0 7926 
is apart from zero. (Contributed by Jim Kingdon,
9Mar2020.)

# 

Theorem  2muline0 7927 
. See also 2muliap0 7926. (Contributed by David A.
Wheeler, 8Dec2018.)



3.4.5 Simple number properties


Theorem  halfcl 7928 
Closure of half of a number (common case). (Contributed by NM,
1Jan2006.)



Theorem  rehalfcl 7929 
Real closure of half. (Contributed by NM, 1Jan2006.)



Theorem  half0 7930 
Half of a number is zero iff the number is zero. (Contributed by NM,
20Apr2006.)



Theorem  2halves 7931 
Two halves make a whole. (Contributed by NM, 11Apr2005.)



Theorem  halfpos2 7932 
A number is positive iff its half is positive. (Contributed by NM,
10Apr2005.)



Theorem  halfpos 7933 
A positive number is greater than its half. (Contributed by NM,
28Oct2004.) (Proof shortened by Mario Carneiro, 27May2016.)



Theorem  halfnneg2 7934 
A number is nonnegative iff its half is nonnegative. (Contributed by NM,
9Dec2005.)



Theorem  halfaddsubcl 7935 
Closure of halfsum and halfdifference. (Contributed by Paul Chapman,
12Oct2007.)



Theorem  halfaddsub 7936 
Sum and difference of halfsum and halfdifference. (Contributed by Paul
Chapman, 12Oct2007.)



Theorem  lt2halves 7937 
A sum is less than the whole if each term is less than half. (Contributed
by NM, 13Dec2006.)



Theorem  addltmul 7938 
Sum is less than product for numbers greater than 2. (Contributed by
Stefan Allan, 24Sep2010.)



Theorem  nominpos 7939* 
There is no smallest positive real number. (Contributed by NM,
28Oct2004.)



Theorem  avglt1 7940 
Ordering property for average. (Contributed by Mario Carneiro,
28May2014.)



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnm2m1cnm3 7953 
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 7954* 
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 7955* 
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 7956* 
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 7957 
Extend class notation to include the class of nonnegative integers.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

