P. 125 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12401-12500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0nnn 12401	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11304. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ ¬ 0 ∈ ℕ
Theorem	0nnnALT 12402	Alternate proof of 0nnn 12401, which requires ax-pre-mulgt0 11304 but is not based on nnne0 12399 (and which can therefore be used in nnne0ALT 12403). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0ALT 12403	Alternate version of nnne0 12399. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12404	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12405	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12406	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12407	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12408	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12409	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12410	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12411*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12412	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 12413	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12414	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12415	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12416	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 12417	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 12418	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 12419	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	1t1e1ALT 12420	Alternate proof of 1t1e1 12531 using a different set of axioms (add ax-mulrcl 11290, ax-i2m1 11295, ax-1ne0 11296, ax-rrecex 11299 and remove ax-resscn 11284, ax-mulcom 11291, ax-mulass 11293, ax-distr 11294). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	nnadddir 12421	Right-distributivity for natural numbers without ax-mulcom 11291. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 12422	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11291. Since (𝐴 · 1) is 𝐴 by ax-1rid 11297, this is equivalent to remullid 43678 for natural numbers, but using fewer axioms (avoiding ax-resscn 11284, ax-addass 11292, ax-mulass 11293, ax-rnegex 11298, ax-pre-lttri 11301, ax-pre-lttrn 11302, ax-pre-ltadd 11303). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 12423	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 11234 through df-9 12439), 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 11234 and df-1 11235). With the decimal constructor df-dec 12842, it is possible to easily express larger integers in base 10. See deccl 12856 and the theorems that follow it. See also 4001prm 17352 (4001 is prime) and the proof of bpos 27650. 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 16385. 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 12424	Extend class notation to include the number 2.
class 2
Syntax	c3 12425	Extend class notation to include the number 3.
class 3
Syntax	c4 12426	Extend class notation to include the number 4.
class 4
Syntax	c5 12427	Extend class notation to include the number 5.
class 5
Syntax	c6 12428	Extend class notation to include the number 6.
class 6
Syntax	c7 12429	Extend class notation to include the number 7.
class 7
Syntax	c8 12430	Extend class notation to include the number 8.
class 8
Syntax	c9 12431	Extend class notation to include the number 9.
class 9
Definition	df-2 12432	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 12433	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 12434	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 12435	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 12436	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 12437	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 12438	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 12439	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	1eltp012 12440	1 is an element of {0, 1, 2}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 1 ∈ {0, 1, 2}
Theorem	0ne1 12441	Zero is different from one (the commuted form is Axiom ax-1ne0 11296). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1m1e0 12442	One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2nn 12443	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	2re 12444	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 12445	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 12446	Alternate proof of 2cn 12445. Shorter but uses more axioms. Similar proofs are possible for 3cn 12451, ... , 9cn 12470. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 2 ∈ ℂ
Theorem	2ex 12447	The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 12448	The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3nn 12449	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	3re 12450	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 12451	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 12452	The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4nn 12453	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	4re 12454	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 12455	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 12456	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	5re 12457	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 12458	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 12459	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	6re 12460	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 12461	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 12462	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	7re 12463	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 12464	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 12465	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	8re 12466	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 12467	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 12468	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	9re 12469	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 12470	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 12471	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 12472	The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 ≤ 2
Theorem	0le2OLD 12473	Obsolete version of 0le2 12472 as of 10-Jun-2026. (Contributed by David A. Wheeler, 7-Dec-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 ≤ 2
Theorem	2pos 12474	The number 2 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 2
Theorem	2posOLD 12475	Obsolete version of 2pos 12474 as of 10-Jun-2026. (Contributed by NM, 27-May-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 < 2
Theorem	2ne0 12476	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2thalfe1 12477	2 times one half equals 1. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · (1 / 2)) = 1
Theorem	3pos 12478	The number 3 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 3
Theorem	3ne0 12479	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 12480	The number 4 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 4
Theorem	4ne0 12481	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 12482	The number 5 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 5
Theorem	6pos 12483	The number 6 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 6
Theorem	7pos 12484	The number 7 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 7
Theorem	8pos 12485	The number 8 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 8
Theorem	9pos 12486	The number 9 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 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 12487	1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 12488	0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 12489	1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 12490	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 12491	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 12492	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 12493	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 12494	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12524. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 − 1) = 1
Theorem	2m1e1OLD 12495	Obsolete version of 2m1e1 12494 as of 10-Jun-2026. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (2 − 1) = 1
Theorem	1e2m1 12496	1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 12497	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 12498	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 12499	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 12500	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5