P. 124 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12301-12400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnne0ALT 12301	Alternate version of nnne0 12297. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12302	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12303	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12304	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12305	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12306	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12307	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12308	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12309*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12310	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 12311	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12312	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12313	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12314	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 12315	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 12316	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 12317	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	1t1e1ALT 12318	Alternate proof of 1t1e1 12429 using a different set of axioms (add ax-mulrcl 11190, ax-i2m1 11195, ax-1ne0 11196, ax-rrecex 11199 and remove ax-resscn 11184, ax-mulcom 11191, ax-mulass 11193, ax-distr 11194). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	nnadddir 12319	Right-distributivity for natural numbers without ax-mulcom 11191. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 12320	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11191. Since (𝐴 · 1) is 𝐴 by ax-1rid 11197, this is equivalent to remullid 43311 for natural numbers, but using fewer axioms (avoiding ax-resscn 11184, ax-addass 11192, ax-mulass 11193, ax-rnegex 11198, ax-pre-lttri 11201, ax-pre-lttrn 11202, ax-pre-ltadd 11203). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 12321	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 11134 through df-9 12337), 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 11134 and df-1 11135). With the decimal constructor df-dec 12740, it is possible to easily express larger integers in base 10. See deccl 12754 and the theorems that follow it. See also 4001prm 17241 (4001 is prime) and the proof of bpos 27530. 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 16280. 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 12322	Extend class notation to include the number 2.
class 2
Syntax	c3 12323	Extend class notation to include the number 3.
class 3
Syntax	c4 12324	Extend class notation to include the number 4.
class 4
Syntax	c5 12325	Extend class notation to include the number 5.
class 5
Syntax	c6 12326	Extend class notation to include the number 6.
class 6
Syntax	c7 12327	Extend class notation to include the number 7.
class 7
Syntax	c8 12328	Extend class notation to include the number 8.
class 8
Syntax	c9 12329	Extend class notation to include the number 9.
class 9
Definition	df-2 12330	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 12331	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 12332	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 12333	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 12334	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 12335	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 12336	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 12337	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	1eltp012 12338	1 is an element of {0, 1, 2}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 1 ∈ {0, 1, 2}
Theorem	0ne1 12339	Zero is different from one (the commuted form is Axiom ax-1ne0 11196). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1m1e0 12340	One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2nn 12341	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	2re 12342	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 12343	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 12344	Alternate proof of 2cn 12343. Shorter but uses more axioms. Similar proofs are possible for 3cn 12349, ... , 9cn 12368. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 2 ∈ ℂ
Theorem	2ex 12345	The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 12346	The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3nn 12347	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	3re 12348	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 12349	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 12350	The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4nn 12351	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	4re 12352	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 12353	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 12354	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	5re 12355	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 12356	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 12357	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	6re 12358	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 12359	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 12360	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ
Theorem	7re 12361	The number 7 is real. (Contributed by NM, 27-May-1999.)
⊢ 7 ∈ ℝ
Theorem	7cn 12362	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 12363	8 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 8 ∈ ℕ
Theorem	8re 12364	The number 8 is real. (Contributed by NM, 27-May-1999.)
⊢ 8 ∈ ℝ
Theorem	8cn 12365	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 12366	9 is a positive integer. (Contributed by NM, 21-Oct-2012.)
⊢ 9 ∈ ℕ
Theorem	9re 12367	The number 9 is real. (Contributed by NM, 27-May-1999.)
⊢ 9 ∈ ℝ
Theorem	9cn 12368	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 12369	Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ≤ 0
Theorem	0le2 12370	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 12371	Obsolete version of 0le2 12370 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 12372	The number 2 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 2
Theorem	2posOLD 12373	Obsolete version of 2pos 12372 as of 10-Jun-2026. (Contributed by NM, 27-May-1999.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 < 2
Theorem	2ne0 12374	The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.)
⊢ 2 ≠ 0
Theorem	2thalfe1 12375	2 times one half equals 1. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 · (1 / 2)) = 1
Theorem	3pos 12376	The number 3 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 3
Theorem	3ne0 12377	The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ 3 ≠ 0
Theorem	4pos 12378	The number 4 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 4
Theorem	4ne0 12379	The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ 4 ≠ 0
Theorem	5pos 12380	The number 5 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 5
Theorem	6pos 12381	The number 6 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 6
Theorem	7pos 12382	The number 7 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 7
Theorem	8pos 12383	The number 8 is positive. (Contributed by NM, 27-May-1999.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 0 < 8
Theorem	9pos 12384	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 12385	1 + -1 is 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + -1) = 0
Theorem	0m0e0 12386	0 minus 0 equals 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (0 − 0) = 0
Theorem	1m0e1 12387	1 - 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 − 0) = 1
Theorem	0p1e1 12388	0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (0 + 1) = 1
Theorem	fv0p1e1 12389	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 12390	1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (1 + 0) = 1
Theorem	1p1e2 12391	1 + 1 = 2. (Contributed by NM, 1-Apr-2008.)
⊢ (1 + 1) = 2
Theorem	2m1e1 12392	2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12422. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
⊢ (2 − 1) = 1
Theorem	2m1e1OLD 12393	Obsolete version of 2m1e1 12392 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 12394	1 = 2 - 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 1 = (2 − 1)
Theorem	3m1e2 12395	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 12396	4 - 1 = 3. (Contributed by AV, 8-Feb-2021.) (Proof shortened by AV, 6-Sep-2021.)
⊢ (4 − 1) = 3
Theorem	5m1e4 12397	5 - 1 = 4. (Contributed by AV, 6-Sep-2021.)
⊢ (5 − 1) = 4
Theorem	6m1e5 12398	6 - 1 = 5. (Contributed by AV, 6-Sep-2021.)
⊢ (6 − 1) = 5
Theorem	7m1e6 12399	7 - 1 = 6. (Contributed by AV, 6-Sep-2021.)
⊢ (7 − 1) = 6
Theorem	8m1e7 12400	8 - 1 = 7. (Contributed by AV, 6-Sep-2021.)
⊢ (8 − 1) = 7