P. 123 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12201-12300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnmtmip 12201	"Minus times minus is plus, The reason for this we need not discuss." (W. H. Auden, as quoted in M. Guillen "Bridges to Infinity", p. 64, see also Metamath Book, section 1.1.1, p. 5) This statement, formalized to "The product of two negative integers is a positive integer", is proved by the following theorem, therefore it actually need not be discussed anymore. "The reason for this" is that (-𝐴 · -𝐵) = (𝐴 · 𝐵) for all complex numbers 𝐴 and 𝐵 because of mul2neg 11587, 𝐴 and 𝐵 are complex numbers because of nncn 12180, and (𝐴 · 𝐵) ∈ ℕ because of nnmulcl 12196. This also holds for positive reals, see rpmtmip 12966. Note that the opposites -𝐴 and -𝐵 of the positive integers 𝐴 and 𝐵 are negative integers. (Contributed by AV, 23-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (-𝐴 · -𝐵) ∈ ℕ)
Theorem	nn2ge 12202*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥))
Theorem	nnge1 12203	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
Theorem	nngt1ne1 12204	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1))
Theorem	nnle1eq1 12205	A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005.)
⊢ (𝐴 ∈ ℕ → (𝐴 ≤ 1 ↔ 𝐴 = 1))
Theorem	nngt0 12206	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
Theorem	nnnlt1 12207	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1)
Theorem	nnnle0 12208	A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0)
Theorem	nnne0 12209	A positive integer is nonzero. See nnne0ALT 12213 for a shorter proof using ax-pre-mulgt0 11113. This proof avoids 0lt1 11670, and thus ax-pre-mulgt0 11113, by splitting ax-1ne0 11105 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11113. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nnneneg 12210	No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴)
Theorem	0nnn 12211	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11113. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ ¬ 0 ∈ ℕ
Theorem	0nnnALT 12212	Alternate proof of 0nnn 12211, which requires ax-pre-mulgt0 11113 but is not based on nnne0 12209 (and which can therefore be used in nnne0ALT 12213). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0ALT 12213	Alternate version of nnne0 12209. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12214	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12215	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12216	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12217	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12218	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12219	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12220	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12221*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12222	Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ)
Theorem	nnge1d 12223	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12224	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12225	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12226	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 12227	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 12228	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 12229	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	1t1e1ALT 12230	Alternate proof of 1t1e1 12336 using a different set of axioms (add ax-mulrcl 11099, ax-i2m1 11104, ax-1ne0 11105, ax-rrecex 11108 and remove ax-resscn 11093, ax-mulcom 11100, ax-mulass 11102, ax-distr 11103). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	nnadddir 12231	Right-distributivity for natural numbers without ax-mulcom 11100. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 12232	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11100. Since (𝐴 · 1) is 𝐴 by ax-1rid 11106, this is equivalent to remullid 42912 for natural numbers, but using fewer axioms (avoiding ax-resscn 11093, ax-addass 11101, ax-mulass 11102, ax-rnegex 11107, ax-pre-lttri 11110, ax-pre-lttrn 11111, ax-pre-ltadd 11112). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 12233	Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
5.4.3  Decimal representation of numbers The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 11043 through df-9 12249), 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 11043 and df-1 11044). With the decimal constructor df-dec 12643, it is possible to easily express larger integers in base 10. See deccl 12657 and the theorems that follow it. See also 4001prm 17113 (4001 is prime) and the proof of bpos 27281. Note that the decimal constructor builds on the definitions in this section. Note: The number 10 will 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 16153. 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 12234	Extend class notation to include the number 2.
class 2
Syntax	c3 12235	Extend class notation to include the number 3.
class 3
Syntax	c4 12236	Extend class notation to include the number 4.
class 4
Syntax	c5 12237	Extend class notation to include the number 5.
class 5
Syntax	c6 12238	Extend class notation to include the number 6.
class 6
Syntax	c7 12239	Extend class notation to include the number 7.
class 7
Syntax	c8 12240	Extend class notation to include the number 8.
class 8
Syntax	c9 12241	Extend class notation to include the number 9.
class 9
Definition	df-2 12242	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 12243	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 12244	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 12245	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 12246	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 12247	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 12248	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 12249	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	0ne1 12250	Zero is different from one (the commuted form is Axiom ax-1ne0 11105). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1m1e0 12251	One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2nn 12252	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	2re 12253	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 12254	The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 2 ∈ ℂ
Theorem	2cnALT 12255	Alternate proof of 2cn 12254. Shorter but uses more axioms. Similar proofs are possible for 3cn 12260, ... , 9cn 12279. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 2 ∈ ℂ
Theorem	2ex 12256	The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 12257	The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3nn 12258	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	3re 12259	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 12260	The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 3 ∈ ℂ
Theorem	3ex 12261	The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4nn 12262	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	4re 12263	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 12264	The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 4 ∈ ℂ
Theorem	5nn 12265	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	5re 12266	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 12267	The number 5 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 5 ∈ ℂ
Theorem	6nn 12268	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	6re 12269	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 12270	The number 6 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 6 ∈ ℂ
Theorem	7nn 12271	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	7re 12272	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 12273	The number 7 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 7 ∈ ℂ
Theorem	8nn 12274	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	8re 12275	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 12276	The number 8 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 8 ∈ ℂ
Theorem	9nn 12277	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	9re 12278	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 12279	The number 9 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 9 ∈ ℂ
Theorem	0le0 12280	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 12281	The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ 0 ≤ 2
Theorem	2pos 12282	The number 2 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 2
Theorem	2ne0 12283	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	3pos 12284	The number 3 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 3
Theorem	3ne0 12285	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 12286	The number 4 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 4
Theorem	4ne0 12287	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 12288	The number 5 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 5
Theorem	6pos 12289	The number 6 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 6
Theorem	7pos 12290	The number 7 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 7
Theorem	8pos 12291	The number 8 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 8
Theorem	9pos 12292	The number 9 is positive. (Contributed by NM, 27-May-1999.)
⊢ 0 < 9
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	1pneg1e0 12293	1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 12294	0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 12295	1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 12296	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 12297	Function value at 𝑁 + 1 with 𝑁 replaced by 0. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.)
⊢ (𝑁 = 0 → (𝐹‘(𝑁 + 1)) = (𝐹‘1))
Theorem	1p0e1 12298	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 12299	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 12300	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12329. (Contributed by David A. Wheeler, 4-Jan-2017.)
⊢ (2 − 1) = 1