P. 78 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnaddcld 7701	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A + B) ∈ ℕ)
Theorem	nnmulcld 7702	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℕ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A · B) ∈ ℕ)
Theorem	nndivred 7703	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (φ → A ∈ ℝ)    &   ⊢ (φ → B ∈ ℕ)    ⇒   ⊢ (φ → (A / B) ∈ ℝ)
3.4.3  Decimal representation of numbers Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 6678 and df-1 6679). Only the digits 0 through 9 (df-0 6678 through df-9 7720) and the number 10 (df-10 7721) are explicitly defined. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12.
Syntax	c2 7704	Extend class notation to include the number 2.
class 2
Syntax	c3 7705	Extend class notation to include the number 3.
class 3
Syntax	c4 7706	Extend class notation to include the number 4.
class 4
Syntax	c5 7707	Extend class notation to include the number 5.
class 5
Syntax	c6 7708	Extend class notation to include the number 6.
class 6
Syntax	c7 7709	Extend class notation to include the number 7.
class 7
Syntax	c8 7710	Extend class notation to include the number 8.
class 8
Syntax	c9 7711	Extend class notation to include the number 9.
class 9
Syntax	c10 7712	Extend class notation to include the number 10.
class 10
Definition	df-2 7713	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 7714	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 7715	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 7716	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 7717	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 7718	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 7719	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 7720	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Definition	df-10 7721	Define the number 10. See remarks under df-2 7713. (Contributed by NM, 5-Feb-2007.)
⊢ 10 = (9 + 1)
Theorem	0ne1 7722	0 ≠ 1 (common case). See aso 1ap0 7334. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1ne0 7723	1 ≠ 0. See aso 1ap0 7334. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 1 ≠ 0
Theorem	1m1e0 7724	(1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2re 7725	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 7726	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
⊢ 2 ∈ ℂ
Theorem	2ex 7727	2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 7728	2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (φ → 2 ∈ ℂ)
Theorem	3re 7729	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 7730	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
⊢ 3 ∈ ℂ
Theorem	3ex 7731	3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4re 7732	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 7733	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 4 ∈ ℂ
Theorem	5re 7734	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 7735	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 7736	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 7737	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 7738	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 7739	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 7740	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 7741	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 7742	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 7743	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	10re 7744	The number 10 is real. (Contributed by NM, 5-Feb-2007.)
⊢ 10 ∈ ℝ
Theorem	0le0 7745	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 7746	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 7747	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 7748	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2ap0 7749	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 2 # 0
Theorem	3pos 7750	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 7751	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 7752	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 7753	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 7754	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 7755	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 7756	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 7757	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 7758	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
Theorem	10pos 7759	The number 10 is positive. (Contributed by NM, 5-Feb-2007.)
⊢ 0 < 10
3.4.4  Some properties of specific numbers This includes adding two pairs of values 1..10 (where the right is less than the left) and where the left is less than the right for the values 1..10.
Theorem	neg1cn 7760	-1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 7761	-1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 7762	-1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 7763	-1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	neg1ap0 7764	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ -1 # 0
Theorem	negneg1e1 7765	--1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 7766	1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 7767	0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 7768	1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 7769	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	1p0e1 7770	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 7771	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 7772	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 7794. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 7773	1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 7774	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.)
⊢ (3 − 1) = 2
Theorem	2p2e4 7775	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.)
⊢ (2 + 2) = 4
Theorem	2times 7776	Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
⊢ (A ∈ ℂ → (2 · A) = (A + A))
Theorem	times2 7777	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (A ∈ ℂ → (A · 2) = (A + A))
Theorem	2timesi 7778	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (2 · A) = (A + A)
Theorem	times2i 7779	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ A ∈ ℂ    ⇒   ⊢ (A · 2) = (A + A)
Theorem	2div2e1 7780	2 divided by 2 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 7781	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 7782	1 + 2 = 3 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 7783	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 7784	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 7785	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 7786	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 7787	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 7788	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	9p1e10 7789	9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (9 + 1) = 10
Theorem	3p2e5 7790	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 7791	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 7792	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6
Theorem	4p3e7 7793	4 + 3 = 7. (Contributed by NM, 11-May-2004.)
⊢ (4 + 3) = 7
Theorem	4p4e8 7794	4 + 4 = 8. (Contributed by NM, 11-May-2004.)
⊢ (4 + 4) = 8
Theorem	5p2e7 7795	5 + 2 = 7. (Contributed by NM, 11-May-2004.)
⊢ (5 + 2) = 7
Theorem	5p3e8 7796	5 + 3 = 8. (Contributed by NM, 11-May-2004.)
⊢ (5 + 3) = 8
Theorem	5p4e9 7797	5 + 4 = 9. (Contributed by NM, 11-May-2004.)
⊢ (5 + 4) = 9
Theorem	5p5e10 7798	5 + 5 = 10. (Contributed by NM, 5-Feb-2007.)
⊢ (5 + 5) = 10
Theorem	6p2e8 7799	6 + 2 = 8. (Contributed by NM, 11-May-2004.)
⊢ (6 + 2) = 8
Theorem	6p3e9 7800	6 + 3 = 9. (Contributed by NM, 11-May-2004.)
⊢ (6 + 3) = 9