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
Definition	df-nn 12201	Define the set of positive integers. Some authors, especially in analysis books, call these the natural numbers, whereas other authors choose to include 0 in their definition of natural numbers. Note that ℕ is a subset of complex numbers (nnsscn 12205), in contrast to the more elementary ordinal natural numbers ω, df-om 7836). See nnind 12218 for the principle of mathematical induction. See df-n0 12472 for the set of nonnegative integers ℕ0. See dfn2 12484 for ℕ defined in terms of ℕ0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9586 in certain proofs. For a more conventional and intuitive definition ("the smallest set of reals containing 1 as well as the successor of every member") see dfnn3 12214 (or its slight variant dfnn2 12213). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
Theorem	nnexALT 12202	Alternate proof of nnex 12206, more direct, that makes use of ax-rep 5221. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℕ ∈ V
Theorem	peano5nni 12203*	Peano's inductive postulate. Theorem I.36 (principle of mathematical induction) of [Apostol] p. 34. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((1 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → ℕ ⊆ 𝐴)
Theorem	nnssre 12204	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 12205	The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12204 and ax-resscn 11120 at the cost of using more axioms. (Contributed by NM, 2-Aug-2004.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ ℕ ⊆ ℂ
Theorem	nnex 12206	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 12207	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Theorem	nncn 12208	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Theorem	nnrei 12209	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℝ
Theorem	nncni 12210	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	1nn 12211	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 1 ∈ ℕ
Theorem	peano2nn 12212	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
Theorem	dfnn2 12213*	Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 12201 replaced it. This definition requires the axiom of infinity to ensure it has the properties we expect. (Contributed by Jeff Hankins, 12-Sep-2013.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	dfnn3 12214*	Alternate definition of the set of positive integers. Definition of positive integers in [Apostol] p. 22. (Contributed by NM, 3-Jul-2005.)
⊢ ℕ = ∩ {𝑥 ∣ (𝑥 ⊆ ℝ ∧ 1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	nnred 12215	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	nncnd 12216	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	peano2nnd 12217	Peano postulate: a successor of a positive integer is a positive integer. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℕ)
5.4.2  Principle of mathematical induction
Theorem	nnind 12218*	Principle of Mathematical Induction (inference schema). The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. See nnaddcl 12223 for an example of its use. See nn0ind 12658 for induction on nonnegative integers and uzind 12655, uzind4 12897 for induction on an arbitrary upper set of integers. See indstr 12907 for strong induction. See also nnindALT 12219. This is an alternative for Metamath 100 proof #74. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nnindALT 12219*	Principle of Mathematical Induction (inference schema). The last four hypotheses give us the substitution instances we need; the first two are the induction step and the basis. This ALT version of nnind 12218 has a different hypothesis order. It may be easier to use with the Metamath program Proof Assistant, because "MM-PA> ASSIGN LAST" will be applied to the substitution instances first. We may eventually use this one as the official version. You may use either version. After the proof is complete, the ALT version can be changed to the non-ALT version with "MM-PA> MINIMIZE_WITH nnind / MAYGROW";. (Contributed by NM, 7-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nnindd 12220*	Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ (𝑥 = 1 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝜂)
Theorem	nn1m1nn 12221	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈ ℕ))
Theorem	nn1suc 12222*	If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → 𝜒)    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜃)
Theorem	nnaddcl 12223	Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcl 12224	Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11127 and ax-mulass 11129. (Revised by Steven Nguyen, 24-Sep-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nnmulcli 12225	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℕ
Theorem	nnadd1com 12226	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 12227	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11359. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 12228	Version of addcomli 11365 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnmtmip 12229	"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 11616, 𝐴 and 𝐵 are complex numbers because of nncn 12208, and (𝐴 · 𝐵) ∈ ℕ because of nnmulcl 12224. This also holds for positive reals, see rpmtmip 13009. Note that the opposites -𝐴 and -𝐵 of the positive integers 𝐴 and 𝐵 are negative integers. (Contributed by AV, 23-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (-𝐴 · -𝐵) ∈ ℕ)
Theorem	nn2ge 12230*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥))
Theorem	nnge1 12231	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
Theorem	nngt1ne1 12232	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1))
Theorem	nnle1eq1 12233	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 12234	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
Theorem	nnnlt1 12235	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1)
Theorem	nnnle0 12236	A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0)
Theorem	nnne0 12237	A positive integer is nonzero. See nnne0ALT 12241 for a shorter proof using ax-pre-mulgt0 11140. This proof avoids 0lt1 11699, and thus ax-pre-mulgt0 11140, by splitting ax-1ne0 11132 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11140. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nnneneg 12238	No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴)
Theorem	0nnn 12239	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11140. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ ¬ 0 ∈ ℕ
Theorem	0nnnALT 12240	Alternate proof of 0nnn 12239, which requires ax-pre-mulgt0 11140 but is not based on nnne0 12237 (and which can therefore be used in nnne0ALT 12241). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0ALT 12241	Alternate version of nnne0 12237. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12242	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12243	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12244	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12245	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12246	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12247	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12248	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12249*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12250	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 12251	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12252	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12253	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12254	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 12255	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 12256	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 12257	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	1t1e1ALT 12258	Alternate proof of 1t1e1 12369 using a different set of axioms (add ax-mulrcl 11126, ax-i2m1 11131, ax-1ne0 11132, ax-rrecex 11135 and remove ax-resscn 11120, ax-mulcom 11127, ax-mulass 11129, ax-distr 11130). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	nnadddir 12259	Right-distributivity for natural numbers without ax-mulcom 11127. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 12260	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11127. Since (𝐴 · 1) is 𝐴 by ax-1rid 11133, this is equivalent to remullid 42991 for natural numbers, but using fewer axioms (avoiding ax-resscn 11120, ax-addass 11128, ax-mulass 11129, ax-rnegex 11134, ax-pre-lttri 11137, ax-pre-lttrn 11138, ax-pre-ltadd 11139). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 12261	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 11070 through df-9 12277), 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 11070 and df-1 11071). With the decimal constructor df-dec 12679, it is possible to easily express larger integers in base 10. See deccl 12693 and the theorems that follow it. See also 4001prm 17157 (4001 is prime) and the proof of bpos 27327. 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 16196. 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 12262	Extend class notation to include the number 2.
class 2
Syntax	c3 12263	Extend class notation to include the number 3.
class 3
Syntax	c4 12264	Extend class notation to include the number 4.
class 4
Syntax	c5 12265	Extend class notation to include the number 5.
class 5
Syntax	c6 12266	Extend class notation to include the number 6.
class 6
Syntax	c7 12267	Extend class notation to include the number 7.
class 7
Syntax	c8 12268	Extend class notation to include the number 8.
class 8
Syntax	c9 12269	Extend class notation to include the number 9.
class 9
Definition	df-2 12270	Define the number 2. (Contributed by NM, 27-May-1999.)
⊢ 2 = (1 + 1)
Definition	df-3 12271	Define the number 3. (Contributed by NM, 27-May-1999.)
⊢ 3 = (2 + 1)
Definition	df-4 12272	Define the number 4. (Contributed by NM, 27-May-1999.)
⊢ 4 = (3 + 1)
Definition	df-5 12273	Define the number 5. (Contributed by NM, 27-May-1999.)
⊢ 5 = (4 + 1)
Definition	df-6 12274	Define the number 6. (Contributed by NM, 27-May-1999.)
⊢ 6 = (5 + 1)
Definition	df-7 12275	Define the number 7. (Contributed by NM, 27-May-1999.)
⊢ 7 = (6 + 1)
Definition	df-8 12276	Define the number 8. (Contributed by NM, 27-May-1999.)
⊢ 8 = (7 + 1)
Definition	df-9 12277	Define the number 9. (Contributed by NM, 27-May-1999.)
⊢ 9 = (8 + 1)
Theorem	1eltp012 12278	1 is an element of {0, 1, 2}. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ 1 ∈ {0, 1, 2}
Theorem	0ne1 12279	Zero is different from one (the commuted form is Axiom ax-1ne0 11132). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 0 ≠ 1
Theorem	1m1e0 12280	One minus one equals zero. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ (1 − 1) = 0
Theorem	2nn 12281	2 is a positive integer. (Contributed by NM, 20-Aug-2001.)
⊢ 2 ∈ ℕ
Theorem	2re 12282	The number 2 is real. (Contributed by NM, 27-May-1999.)
⊢ 2 ∈ ℝ
Theorem	2cn 12283	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 12284	Alternate proof of 2cn 12283. Shorter but uses more axioms. Similar proofs are possible for 3cn 12289, ... , 9cn 12308. (Contributed by NM, 30-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 2 ∈ ℂ
Theorem	2ex 12285	The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 2 ∈ V
Theorem	2cnd 12286	The number 2 is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 2 ∈ ℂ)
Theorem	3nn 12287	3 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 3 ∈ ℕ
Theorem	3re 12288	The number 3 is real. (Contributed by NM, 27-May-1999.)
⊢ 3 ∈ ℝ
Theorem	3cn 12289	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 12290	The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ 3 ∈ V
Theorem	4nn 12291	4 is a positive integer. (Contributed by NM, 8-Jan-2006.)
⊢ 4 ∈ ℕ
Theorem	4re 12292	The number 4 is real. (Contributed by NM, 27-May-1999.)
⊢ 4 ∈ ℝ
Theorem	4cn 12293	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 12294	5 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 5 ∈ ℕ
Theorem	5re 12295	The number 5 is real. (Contributed by NM, 27-May-1999.)
⊢ 5 ∈ ℝ
Theorem	5cn 12296	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 12297	6 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 6 ∈ ℕ
Theorem	6re 12298	The number 6 is real. (Contributed by NM, 27-May-1999.)
⊢ 6 ∈ ℝ
Theorem	6cn 12299	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 12300	7 is a positive integer. (Contributed by Mario Carneiro, 15-Sep-2013.)
⊢ 7 ∈ ℕ