Type  Label  Description 
Statement 

Theorem  1lt4 8901 
1 is less than 4. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  4lt5 8902 
4 is less than 5. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  3lt5 8903 
3 is less than 5. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  2lt5 8904 
2 is less than 5. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  1lt5 8905 
1 is less than 5. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  5lt6 8906 
5 is less than 6. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  4lt6 8907 
4 is less than 6. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  3lt6 8908 
3 is less than 6. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  2lt6 8909 
2 is less than 6. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  1lt6 8910 
1 is less than 6. (Contributed by NM, 19Oct2012.)



Theorem  6lt7 8911 
6 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  5lt7 8912 
5 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  4lt7 8913 
4 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  3lt7 8914 
3 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  2lt7 8915 
2 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  1lt7 8916 
1 is less than 7. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  7lt8 8917 
7 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  6lt8 8918 
6 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  5lt8 8919 
5 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  4lt8 8920 
4 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  3lt8 8921 
3 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  2lt8 8922 
2 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  1lt8 8923 
1 is less than 8. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  8lt9 8924 
8 is less than 9. (Contributed by Mario Carneiro, 19Feb2014.)



Theorem  7lt9 8925 
7 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  6lt9 8926 
6 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  5lt9 8927 
5 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  4lt9 8928 
4 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  3lt9 8929 
3 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  2lt9 8930 
2 is less than 9. (Contributed by Mario Carneiro, 9Mar2015.)



Theorem  1lt9 8931 
1 is less than 9. (Contributed by NM, 19Oct2012.) (Revised by Mario
Carneiro, 9Mar2015.)



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



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



Theorem  1ap2 8934 
1 is apart from 2. (Contributed by Jim Kingdon, 29Oct2022.)

# 

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



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



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



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



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



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



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



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



Theorem  halfge0 8943 
Onehalf is not negative. (Contributed by AV, 7Jun2020.)



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



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



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



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



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



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



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

# 

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

# 

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



4.4.5 Simple number properties


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  xp1d2m1eqxm1d2 8979 
A complex number increased by 1, then divided by 2, then decreased by 1
equals the complex number decreased by 1 and then divided by 2.
(Contributed by AV, 24May2020.)



Theorem  div4p1lem1div2 8980 
An integer greater than 5, divided by 4 and increased by 1, is less than
or equal to the half of the integer minus 1. (Contributed by AV,
8Jul2021.)



4.4.6 The Archimedean property


Theorem  arch 8981* 
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 8982* 
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 8983* 
A bounded real sequence is less than or equal to at least
one of its indices. (Contributed by NM, 18Jan2008.)



4.4.7 Nonnegative integers (as a subset of
complex numbers)


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

