Type  Label  Description 
Statement 

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



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



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



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



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

# 

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

# 

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



3.4.5 Simple number properties


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnm2m1cnm3 8233 
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 8234 
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 8235 
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 8236* 
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 8237* 
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 8238* 
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 8239 
Extend class notation to include the class of nonnegative integers.



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nn0ge2m1nn 8299 
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 8300 
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.)

