P. 112 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnge1d 11101	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 11102	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 11103	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 11104	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 11105	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 11106	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 11107	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
5.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 9981 through df-9 11124), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 9981 and df-1 9982). With the decimal constructor df-dec 11532, it is possible to easily express larger integers in base 10. See deccl 11550 and the theorems that follow it. See also 4001prm 15899 (4001 is prime) and the proof of bpos 25063. Note that the decimal constructor builds on the definitions in this section. Note: The symbol 10 representing the number 10 is deprecated (and will be removed in the near future). The number 10 should be represented by its digits using the decimal constructor only, i.e. by ;10. Therefore, only decimal digits are needed (as symbols) for the decimal representation of a number. Integers can also be exhibited as sums of powers of 10 (e.g. the number 103 can be expressed as ((;10↑2) + 3)) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as (7↑7) − 2. Decimals can be expressed as ratios of integers, as in cos2bnd 14962. 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 11108	Extend class notation to include the number 2.
class 2
Syntax	c3 11109	Extend class notation to include the number 3.
class 3
Syntax	c4 11110	Extend class notation to include the number 4.
class 4
Syntax	c5 11111	Extend class notation to include the number 5.
class 5
Syntax	c6 11112	Extend class notation to include the number 6.
class 6
Syntax	c7 11113	Extend class notation to include the number 7.
class 7
Syntax	c8 11114	Extend class notation to include the number 8.
class 8
Syntax	c9 11115	Extend class notation to include the number 9.
class 9
Syntax	c10 11116	Extend class notation to include the number 10.
class 10
Definition	df-2 11117	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 11118	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 11119	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 11120	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 11121	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 11122	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 11123	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 11124	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Definition	df-10OLD 11125	Define the number 10. See remarks under df-2 11117. (Contributed by NM, 5-Feb-2007.) Obsolete as of 9-Sep-2021. (New usage is discouraged.)
⊢ 10 = (9 + 1)
Theorem	0ne1 11126	0 ≠ 1; the reverse order is already proved. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1m1e0 11127	(1 − 1) = 0. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2re 11128	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 11129	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
⊢ 2 ∈ ℂ
Theorem	2ex 11130	2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 11131	2 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3re 11132	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 11133	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)
⊢ 3 ∈ ℂ
Theorem	3ex 11134	3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4re 11135	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 11136	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 4 ∈ ℂ
Theorem	5re 11137	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 11138	The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 5 ∈ ℂ
Theorem	6re 11139	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 11140	The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 6 ∈ ℂ
Theorem	7re 11141	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 11142	The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 7 ∈ ℂ
Theorem	8re 11143	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 11144	The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 8 ∈ ℂ
Theorem	9re 11145	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 11146	The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 9 ∈ ℂ
Theorem	10reOLD 11147	Obsolete version of 10re 11555 as of 8-Sep-2021. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 10 ∈ ℝ
Theorem	0le0 11148	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 11149	0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 11150	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 11151	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	3pos 11152	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 11153	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 11154	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 11155	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 11156	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 11157	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 11158	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 11159	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 11160	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
Theorem	10posOLD 11161	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) Obsolete version of 10pos 11553 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 0 < 10
5.4.4  Some properties of specific numbers This section includes specific theorems about one-digit natural numbers (membership, addition, subtraction, multiplication, division, ordering).
Theorem	neg1cn 11162	-1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 11163	-1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 11164	-1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 11165	-1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	negneg1e1 11166	--1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	1pneg1e0 11167	1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 11168	0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 11169	1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 11170	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	1p0e1 11171	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 11172	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 11173	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 11202. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1
Theorem	1e2m1 11174	1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 11175	3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (3 − 1) = 2
Theorem	4m1e3 11176	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 11177	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 11178	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 11179	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 11180	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7
Theorem	9m1e8 11181	9 - 1 = 8. (Contributed by AV, 6-Sep-2021.)
⊢ (9 − 1) = 8
Theorem	2p2e4 11182	Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: mmset.html#trivia. This proof is simple, but it depends on many other proof steps because 2 and 4 are complex numbers and thus it depends on our construction of complex numbers. The proof o2p2e4 7666 is similar but proves 2 + 2 = 4 using ordinal natural numbers (finite integers starting at 0), so that proof depends on fewer intermediate steps. (Contributed by NM, 27-May-1999.)
⊢ (2 + 2) = 4
Theorem	2times 11183	Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴))
Theorem	times2 11184	A number times 2. (Contributed by NM, 16-Oct-2007.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴))
Theorem	2timesi 11185	Two times a number. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (2 · 𝐴) = (𝐴 + 𝐴)
Theorem	times2i 11186	A number times 2. (Contributed by NM, 11-May-2004.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
Theorem	2txmxeqx 11187	Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
Theorem	2div2e1 11188	2 divided by 2 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (2 / 2) = 1
Theorem	2p1e3 11189	2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (2 + 1) = 3
Theorem	1p2e3 11190	1 + 2 = 3. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 2) = 3
Theorem	3p1e4 11191	3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (3 + 1) = 4
Theorem	4p1e5 11192	4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (4 + 1) = 5
Theorem	5p1e6 11193	5 + 1 = 6. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (5 + 1) = 6
Theorem	6p1e7 11194	6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (6 + 1) = 7
Theorem	7p1e8 11195	7 + 1 = 8. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (7 + 1) = 8
Theorem	8p1e9 11196	8 + 1 = 9. (Contributed by Mario Carneiro, 18-Apr-2015.)
⊢ (8 + 1) = 9
Theorem	9p1e10OLD 11197	9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) Obsolete version of 9p1e10 11534 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (9 + 1) = 10
Theorem	3p2e5 11198	3 + 2 = 5. (Contributed by NM, 11-May-2004.)
⊢ (3 + 2) = 5
Theorem	3p3e6 11199	3 + 3 = 6. (Contributed by NM, 11-May-2004.)
⊢ (3 + 3) = 6
Theorem	4p2e6 11200	4 + 2 = 6. (Contributed by NM, 11-May-2004.)
⊢ (4 + 2) = 6