Type  Label  Description 
Statement 

Theorem  4t2e8 8501 
4 times 2 equals 8. (Contributed by NM, 2Aug2004.)



Theorem  2t0e0 8502 
2 times 0 equals 0. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  4d2e2 8503 
One half of four is two. (Contributed by NM, 3Sep1999.)



Theorem  2nn 8504 
2 is a positive integer. (Contributed by NM, 20Aug2001.)



Theorem  3nn 8505 
3 is a positive integer. (Contributed by NM, 8Jan2006.)



Theorem  4nn 8506 
4 is a positive integer. (Contributed by NM, 8Jan2006.)



Theorem  5nn 8507 
5 is a positive integer. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  6nn 8508 
6 is a positive integer. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  7nn 8509 
7 is a positive integer. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  8nn 8510 
8 is a positive integer. (Contributed by Mario Carneiro, 15Sep2013.)



Theorem  9nn 8511 
9 is a positive integer. (Contributed by NM, 21Oct2012.)



Theorem  1lt2 8512 
1 is less than 2. (Contributed by NM, 24Feb2005.)



Theorem  2lt3 8513 
2 is less than 3. (Contributed by NM, 26Sep2010.)



Theorem  1lt3 8514 
1 is less than 3. (Contributed by NM, 26Sep2010.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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

# 

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



3.4.5 Simple number properties


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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  cnm2m1cnm3 8593 
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 8594 
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 8595 
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 8596* 
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 8597* 
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 8598* 
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 8599 
Extend class notation to include the class of nonnegative integers.



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

