Type  Label  Description 
Statement 

Theorem  6p4e10 7801 
6 + 4 = 10. (Contributed by NM, 5Feb2007.)



Theorem  7p2e9 7802 
7 + 2 = 9. (Contributed by NM, 11May2004.)



Theorem  7p3e10 7803 
7 + 3 = 10. (Contributed by NM, 5Feb2007.)



Theorem  8p2e10 7804 
8 + 2 = 10. (Contributed by NM, 5Feb2007.)



Theorem  1t1e1 7805 
1 times 1 equals 1. (Contributed by David A. Wheeler, 7Jul2016.)



Theorem  2t1e2 7806 
2 times 1 equals 2. (Contributed by David A. Wheeler, 6Dec2018.)



Theorem  2t2e4 7807 
2 times 2 equals 4. (Contributed by NM, 1Aug1999.)



Theorem  3t1e3 7808 
3 times 1 equals 3. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  3t2e6 7809 
3 times 2 equals 6. (Contributed by NM, 2Aug2004.)



Theorem  3t3e9 7810 
3 times 3 equals 9. (Contributed by NM, 11May2004.)



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



Theorem  5t2e10 7812 
5 times 2 equals 10. (Contributed by NM, 5Feb2007.)



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



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



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



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



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



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



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



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



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



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



Theorem  10nn 7823 
10 is a positive integer. (Contributed by NM, 8Nov2012.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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

# 

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

# 

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



3.4.5 Simple number properties


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



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



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



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



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



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



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



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



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



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



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



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



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

