Type  Label  Description 
Statement 

Theorem  2p1e3 7801 
2 + 1 = 3. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (2 + 1) = 3 

Theorem  1p2e3 7802 
1 + 2 = 3 (common case). (Contributed by David A. Wheeler,
8Dec2018.)

⊢ (1 + 2) = 3 

Theorem  3p1e4 7803 
3 + 1 = 4. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (3 + 1) = 4 

Theorem  4p1e5 7804 
4 + 1 = 5. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (4 + 1) = 5 

Theorem  5p1e6 7805 
5 + 1 = 6. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (5 + 1) = 6 

Theorem  6p1e7 7806 
6 + 1 = 7. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (6 + 1) = 7 

Theorem  7p1e8 7807 
7 + 1 = 8. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (7 + 1) = 8 

Theorem  8p1e9 7808 
8 + 1 = 9. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (8 + 1) = 9 

Theorem  9p1e10 7809 
9 + 1 = 10. (Contributed by Mario Carneiro, 18Apr2015.)

⊢ (9 + 1) = 10 

Theorem  3p2e5 7810 
3 + 2 = 5. (Contributed by NM, 11May2004.)

⊢ (3 + 2) = 5 

Theorem  3p3e6 7811 
3 + 3 = 6. (Contributed by NM, 11May2004.)

⊢ (3 + 3) = 6 

Theorem  4p2e6 7812 
4 + 2 = 6. (Contributed by NM, 11May2004.)

⊢ (4 + 2) = 6 

Theorem  4p3e7 7813 
4 + 3 = 7. (Contributed by NM, 11May2004.)

⊢ (4 + 3) = 7 

Theorem  4p4e8 7814 
4 + 4 = 8. (Contributed by NM, 11May2004.)

⊢ (4 + 4) = 8 

Theorem  5p2e7 7815 
5 + 2 = 7. (Contributed by NM, 11May2004.)

⊢ (5 + 2) = 7 

Theorem  5p3e8 7816 
5 + 3 = 8. (Contributed by NM, 11May2004.)

⊢ (5 + 3) = 8 

Theorem  5p4e9 7817 
5 + 4 = 9. (Contributed by NM, 11May2004.)

⊢ (5 + 4) = 9 

Theorem  5p5e10 7818 
5 + 5 = 10. (Contributed by NM, 5Feb2007.)

⊢ (5 + 5) = 10 

Theorem  6p2e8 7819 
6 + 2 = 8. (Contributed by NM, 11May2004.)

⊢ (6 + 2) = 8 

Theorem  6p3e9 7820 
6 + 3 = 9. (Contributed by NM, 11May2004.)

⊢ (6 + 3) = 9 

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

⊢ (6 + 4) = 10 

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

⊢ (7 + 2) = 9 

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

⊢ (7 + 3) = 10 

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

⊢ (8 + 2) = 10 

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

⊢ (1 · 1) = 1 

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

⊢ (2 · 1) = 2 

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

⊢ (2 · 2) = 4 

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

⊢ (3 · 1) = 3 

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

⊢ (3 · 2) = 6 

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

⊢ (3 · 3) = 9 

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

⊢ (4 · 2) = 8 

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

⊢ (5 · 2) = 10 

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

⊢ (2 · 0) = 0 

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

⊢ (4 / 2) = 2 

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

⊢ 2 ∈
ℕ 

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

⊢ 3 ∈
ℕ 

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

⊢ 4 ∈
ℕ 

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

⊢ 5 ∈
ℕ 

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

⊢ 6 ∈
ℕ 

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

⊢ 7 ∈
ℕ 

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

⊢ 8 ∈
ℕ 

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

⊢ 9 ∈
ℕ 

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

⊢ 10 ∈
ℕ 

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

⊢ 1 < 2 

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

⊢ 2 < 3 

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

⊢ 1 < 3 

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

⊢ 3 < 4 

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

⊢ 2 < 4 

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

⊢ 1 < 4 

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

⊢ 4 < 5 

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

⊢ 3 < 5 

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

⊢ 2 < 5 

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

⊢ 1 < 5 

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

⊢ 5 < 6 

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

⊢ 4 < 6 

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

⊢ 3 < 6 

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

⊢ 2 < 6 

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

⊢ 1 < 6 

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

⊢ 6 < 7 

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

⊢ 5 < 7 

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

⊢ 4 < 7 

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

⊢ 3 < 7 

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

⊢ 2 < 7 

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

⊢ 1 < 7 

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

⊢ 7 < 8 

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

⊢ 6 < 8 

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

⊢ 5 < 8 

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

⊢ 4 < 8 

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

⊢ 3 < 8 

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

⊢ 2 < 8 

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

⊢ 1 < 8 

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

⊢ 8 < 9 

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

⊢ 7 < 9 

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

⊢ 6 < 9 

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

⊢ 5 < 9 

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

⊢ 4 < 9 

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

⊢ 3 < 9 

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

⊢ 2 < 9 

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

⊢ 1 < 9 

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

⊢ 9 < 10 

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

⊢ 8 < 10 

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

⊢ 7 < 10 

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

⊢ 6 < 10 

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

⊢ 5 < 10 

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

⊢ 4 < 10 

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

⊢ 3 < 10 

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

⊢ 2 < 10 

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

⊢ 1 < 10 

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

⊢ 0 ≠ 2 

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

⊢ 1 ≠ 2 

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

⊢ 1 ≤ 2 

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

⊢ (2 ∈ ℂ
∧ 2 ≠ 0) 

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

⊢ (2 ∈ ℝ
∧ 2 ≠ 0) 

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

⊢ 1 ≤ 3 

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

⊢ (1 · 1) = 1 

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

⊢ (1 / 2) ∈
ℝ 

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

⊢ (1 / 2) ∈
ℂ 

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

⊢ 0 < (1 / 2) 

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

⊢ (1 / 2) < 1 

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

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