Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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

# 

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



3.4.5 Simple number properties


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnm2m1cnm3 8176 
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  div4p1lem1div2 8177 
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.)



3.4.6 The Archimedean property


Theorem  arch 8178* 
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 8179* 
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 8180* 
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 8181 
Extend class notation to include the class of nonnegative integers.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

