Type  Label  Description 
Statement 

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

⊢ (6 + 4) = 10 

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

⊢ (7 + 2) = 9 

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

⊢ (7 + 3) = 10 

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

⊢ (8 + 2) = 10 

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

⊢ (1 · 1) = 1 

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

⊢ (2 · 1) = 2 

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

⊢ (2 · 2) = 4 

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

⊢ (3 · 1) = 3 

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

⊢ (3 · 2) = 6 

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

⊢ (3 · 3) = 9 

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

⊢ (4 · 2) = 8 

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

⊢ (5 · 2) = 10 

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

⊢ (2 · 0) = 0 

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

⊢ (4 / 2) = 2 

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

⊢ 2 ∈
ℕ 

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

⊢ 3 ∈
ℕ 

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

⊢ 4 ∈
ℕ 

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

⊢ 5 ∈
ℕ 

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

⊢ 6 ∈
ℕ 

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

⊢ 7 ∈
ℕ 

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

⊢ 8 ∈
ℕ 

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

⊢ 9 ∈
ℕ 

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

⊢ 10 ∈
ℕ 

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

⊢ 1 < 2 

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

⊢ 2 < 3 

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

⊢ 1 < 3 

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

⊢ 3 < 4 

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

⊢ 2 < 4 

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

⊢ 1 < 4 

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

⊢ 4 < 5 

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

⊢ 3 < 5 

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

⊢ 2 < 5 

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

⊢ 1 < 5 

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

⊢ 5 < 6 

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

⊢ 4 < 6 

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

⊢ 3 < 6 

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

⊢ 2 < 6 

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

⊢ 1 < 6 

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

⊢ 6 < 7 

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

⊢ 5 < 7 

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

⊢ 4 < 7 

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

⊢ 3 < 7 

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

⊢ 2 < 7 

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

⊢ 1 < 7 

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

⊢ 7 < 8 

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

⊢ 6 < 8 

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

⊢ 5 < 8 

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

⊢ 4 < 8 

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

⊢ 3 < 8 

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

⊢ 2 < 8 

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

⊢ 1 < 8 

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

⊢ 8 < 9 

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

⊢ 7 < 9 

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

⊢ 6 < 9 

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

⊢ 5 < 9 

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

⊢ 4 < 9 

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

⊢ 3 < 9 

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

⊢ 2 < 9 

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

⊢ 1 < 9 

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

⊢ 9 < 10 

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

⊢ 8 < 10 

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

⊢ 7 < 10 

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

⊢ 6 < 10 

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

⊢ 5 < 10 

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

⊢ 4 < 10 

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

⊢ 3 < 10 

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

⊢ 2 < 10 

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

⊢ 1 < 10 

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

⊢ 0 ≠ 2 

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

⊢ 1 ≠ 2 

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

⊢ 1 ≤ 2 

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

⊢ (2 ∈ ℂ
∧ 2 ≠ 0) 

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

⊢ (2 ∈ ℝ
∧ 2 ≠ 0) 

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

⊢ 1 ≤ 3 

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

⊢ (1 · 1) = 1 

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

⊢ (1 / 2) ∈
ℝ 

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

⊢ (1 / 2) ∈
ℂ 

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

⊢ 0 < (1 / 2) 

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

⊢ (1 / 2) < 1 

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

⊢ (1 − (1 / 2)) = (1 / 2) 

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

⊢ ((1 / 8) · (4 / 3)) = (1 /
6) 

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

⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 / 3)) 

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

⊢ (i · 0) = 0 

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

⊢ (2 · i) ∈ ℂ 

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

⊢ i # 0 

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

⊢ (2 · i) # 0 

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

⊢ (2 · i) ≠ 0 

3.4.5 Simple number properties


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

⊢ (A ∈ ℂ → (A / 2) ∈
ℂ) 

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

⊢ (A ∈ ℝ → (A / 2) ∈
ℝ) 

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

⊢ (A ∈ ℂ → ((A / 2) = 0 ↔ A = 0)) 

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

⊢ (A ∈ ℂ → ((A / 2) + (A /
2)) = A) 

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

⊢ (A ∈ ℝ → (0 < A ↔ 0 < (A / 2))) 

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

⊢ (A ∈ ℝ → (0 < A ↔ (A /
2) < A)) 

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

⊢ (A ∈ ℝ → (0 ≤ A ↔ 0 ≤ (A / 2))) 

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

⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → (((A + B) / 2) ∈ ℂ
∧ ((A
− B) / 2) ∈ ℂ)) 

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

⊢ ((A ∈ ℂ ∧
B ∈
ℂ) → ((((A + B) / 2) + ((A
− B) / 2)) = A ∧ (((A + B) / 2)
− ((A − B) / 2)) = B)) 

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

⊢ ((A ∈ ℝ ∧
B ∈
ℝ ∧ 𝐶 ∈
ℝ) → ((A < (𝐶 / 2) ∧ B < (𝐶 / 2)) → (A + B) <
𝐶)) 

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

⊢ (((A ∈ ℝ ∧
B ∈
ℝ) ∧ (2 < A ∧ 2 <
B)) → (A + B) <
(A · B)) 

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

⊢ ¬ ∃x ∈ ℝ (0 < x ∧ ¬ ∃y ∈ ℝ (0 < y ∧ y < x)) 

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

⊢ ((A ∈ ℝ ∧
B ∈
ℝ) → (A < B ↔ A <
((A + B) / 2))) 