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	supfirege 12201	The supremum of a finite set of real numbers is greater than or equal to all the real numbers of the set. (Contributed by AV, 1-Oct-2019.)
⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑆 = sup(𝐵, ℝ, < ))    ⇒   ⊢ (𝜑 → 𝐶 ≤ 𝑆)
5.3.9  Imaginary and complex number properties
Theorem	neg1cn 12202	-1 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ -1 ∈ ℂ
Theorem	neg1rr 12203	-1 is a real number. (Contributed by David A. Wheeler, 5-Dec-2018.)
⊢ -1 ∈ ℝ
Theorem	neg1ne0 12204	-1 is nonzero. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 ≠ 0
Theorem	neg1lt0 12205	-1 is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ -1 < 0
Theorem	negneg1e1 12206	--1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ --1 = 1
Theorem	inelr 12207	The imaginary unit i is not a real number. (Contributed by NM, 6-May-1999.)
⊢ ¬ i ∈ ℝ
Theorem	rimul 12208	A real number times the imaginary unit is real only if the number is 0. (Contributed by NM, 28-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ (i · 𝐴) ∈ ℝ) → 𝐴 = 0)
Theorem	cru 12209	The representation of complex numbers in terms of real and imaginary parts is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) = (𝐶 + (i · 𝐷)) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	crne0 12210	The real representation of complex numbers is nonzero iff one of its terms is nonzero. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ (𝐴 + (i · 𝐵)) ≠ 0))
Theorem	creur 12211*	The real part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	creui 12212*	The imaginary part of a complex number is unique. Proposition 10-1.3 of [Gleason] p. 130. (Contributed by NM, 9-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → ∃!𝑦 ∈ ℝ ∃𝑥 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	cju 12213*	The complex conjugate of a complex number is unique. (Contributed by Mario Carneiro, 6-Nov-2013.)
⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))
5.3.10  Function operation analogue theorems
Theorem	ofsubeq0 12214	Function analogue of subeq0 11483. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → ((𝐹 ∘f − 𝐺) = (𝐴 × {0}) ↔ 𝐹 = 𝐺))
Theorem	ofnegsub 12215	Function analogue of negsub 11505. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ) → (𝐹 ∘f + ((𝐴 × {-1}) ∘f · 𝐺)) = (𝐹 ∘f − 𝐺))
Theorem	ofsubge0 12216	Function analogue of subge0 11726. (Contributed by Mario Carneiro, 24-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ) → ((𝐴 × {0}) ∘r ≤ (𝐹 ∘f − 𝐺) ↔ 𝐺 ∘r ≤ 𝐹))
5.3.11  Indicator Functions According to Wikipedia (https://en.wikipedia.org/wiki/Indicator_function, "Indicator function", 11-Apr-2026): "In mathematics, an indicator function or a characteristic function of a subset of a set is a function that maps elements of the subset to one, and all other elements to zero. That is, if 𝐴 is a subset of some set 𝑋, then the indicator function of 𝐴 is the function 𝟭A defined by 𝟭A ( x ) = 1 if 𝑥 ∈ 𝐴, and 𝟭A ( x ) = 0 otherwise." See also definition in [Lang2] p. 3: "The characteristic function of a subset S' of S is the function 𝜒 such that 𝜒(x) = 1 if 𝑥 ∈ 𝑆' and 𝜒(x) = 0 if 𝑥 ∉ 𝑆'".
Syntax	cind 12217	Extend class notation with the indicator function generator.
class 𝟭
Definition	df-ind 12218*	Define the indicator function generator. It generates an indicator function ((𝟭‘𝑂)‘𝐴) for a given domain 𝑂 and a given subset 𝐴 of the domain, see indval 12220. In contrast to the definitions and notations in Wikipedia and [Lang2] p. 3, the domain and the subset are always mentioned explicitly. (Contributed by Thierry Arnoux, 20-Jan-2017.)
⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indv 12219*	Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indval 12220*	Value of the indicator function generator for a set 𝐴 and a domain 𝑂, i.e., an indicator function for a given domain 𝑂 and a given subset 𝐴 of the domain. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0)))
Theorem	indval0 12221	The indicator function generator does not generate a (meaningful) indicator function for a class which is not a subset of the domain. (Contributed by AV, 11-Apr-2026.)
⊢ (¬ 𝐴 ⊆ 𝑂 → ((𝟭‘𝑂)‘𝐴) = ∅)
Theorem	indval2 12222	Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0})))
Theorem	indf 12223	An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1})
Theorem	indfval 12224	Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0))
Theorem	fvindre 12225	The range of the indicator function is a subset of ℝ. (Contributed by AV, 10-Apr-2026.)
⊢ (((𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂) ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) ∈ ℝ)
Theorem	ind1 12226	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1)
Theorem	ind0 12227	Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0)
Theorem	ind1a 12228	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴))
Theorem	indconst0 12229	Indicator of the empty set. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂)‘∅) = (𝑂 × {0}))
Theorem	indconst1 12230	Indicator of the whole set. (Contributed by Thierry Arnoux, 25-Jan-2026.)
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂)‘𝑂) = (𝑂 × {1}))
Theorem	indpi1 12231	Preimage of the singleton {1} by the indicator function. See i1f1lem 25827. (Contributed by Thierry Arnoux, 21-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴)
5.4  Integer sets
5.4.1  Positive integers (as a subset of complex numbers)
Syntax	cn 12232	Extend class notation to include the class of positive integers.
class ℕ
Definition	df-nn 12233	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 12237), in contrast to the more elementary ordinal natural numbers ω, df-om 7862). See nnind 12250 for the principle of mathematical induction. See df-n0 12504 for the set of nonnegative integers ℕ0. See dfn2 12516 for ℕ defined in terms of ℕ0. This is a technical definition that helps us avoid the Axiom of Infinity ax-inf2 9609 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 12246 (or its slight variant dfnn2 12245). (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
Theorem	nnexALT 12234	Alternate proof of nnex 12238, more direct, that makes use of ax-rep 5237. (Contributed by Mario Carneiro, 3-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℕ ∈ V
Theorem	peano5nni 12235*	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 12236	The positive integers are a subset of the reals. (Contributed by NM, 10-Jan-1997.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ ℕ ⊆ ℝ
Theorem	nnsscn 12237	The positive integers are a subset of the complex numbers. Remark: this could also be proven from nnssre 12236 and ax-resscn 11156 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 12238	The set of positive integers exists. (Contributed by NM, 3-Oct-1999.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ℕ ∈ V
Theorem	nnre 12239	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
Theorem	nncn 12240	A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)
Theorem	nnrei 12241	A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ ℝ
Theorem	nncni 12242	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 12243	Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ 1 ∈ ℕ
Theorem	peano2nn 12244	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 12245*	Alternate definition of the set of positive integers. This was our original definition, before the current df-nn 12233 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 12246*	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 12247	A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	nncnd 12248	A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	peano2nnd 12249	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 12250*	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 12255 for an example of its use. See nn0ind 12690 for induction on nonnegative integers and uzind 12687, uzind4 12929 for induction on an arbitrary upper set of integers. See indstr 12939 for strong induction. See also nnindALT 12251. 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 12251*	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 12250 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 12252*	Principle of Mathematical Induction (inference schema) on integers, a deduction version. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ (𝑥 = 1 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝜂)
Theorem	nn1m1nn 12253	Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ (𝐴 − 1) ∈ ℕ))
Theorem	nn1suc 12254*	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 12255	Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcl 12256	Closure of multiplication of positive integers. (Contributed by NM, 12-Jan-1997.) Remove dependency on ax-mulcom 11163 and ax-mulass 11165. (Revised by Steven Nguyen, 24-Sep-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nnmulcli 12257	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℕ
Theorem	nnadd1com 12258	Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴))
Theorem	nnaddcom 12259	Addition is commutative for natural numbers. Uses fewer axioms than addcom 11395. (Contributed by Steven Nguyen, 9-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	nnaddcomli 12260	Version of addcomli 11401 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ (𝐴 + 𝐵) = 𝐶    ⇒   ⊢ (𝐵 + 𝐴) = 𝐶
Theorem	nnmtmip 12261	"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 11652, 𝐴 and 𝐵 are complex numbers because of nncn 12240, and (𝐴 · 𝐵) ∈ ℕ because of nnmulcl 12256. This also holds for positive reals, see rpmtmip 13041. Note that the opposites -𝐴 and -𝐵 of the positive integers 𝐴 and 𝐵 are negative integers. (Contributed by AV, 23-Dec-2022.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (-𝐴 · -𝐵) ∈ ℕ)
Theorem	nn2ge 12262*	There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥))
Theorem	nnge1 12263	A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
Theorem	nngt1ne1 12264	A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.)
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1))
Theorem	nnle1eq1 12265	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 12266	A positive integer is positive. (Contributed by NM, 26-Sep-1999.)
⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
Theorem	nnnlt1 12267	A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1)
Theorem	nnnle0 12268	A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020.)
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 ≤ 0)
Theorem	nnne0 12269	A positive integer is nonzero. See nnne0ALT 12273 for a shorter proof using ax-pre-mulgt0 11176. This proof avoids 0lt1 11735, and thus ax-pre-mulgt0 11176, by splitting ax-1ne0 11168 into the two separate cases 0 < 1 and 1 < 0. (Contributed by NM, 27-Sep-1999.) Remove dependency on ax-pre-mulgt0 11176. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nnneneg 12270	No positive integer is equal to its negation. (Contributed by AV, 20-Jun-2023.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ -𝐴)
Theorem	0nnn 12271	Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) Remove dependency on ax-pre-mulgt0 11176. (Revised by Steven Nguyen, 30-Jan-2023.)
⊢ ¬ 0 ∈ ℕ
Theorem	0nnnALT 12272	Alternate proof of 0nnn 12271, which requires ax-pre-mulgt0 11176 but is not based on nnne0 12269 (and which can therefore be used in nnne0ALT 12273). (Contributed by NM, 25-Aug-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 0 ∈ ℕ
Theorem	nnne0ALT 12273	Alternate version of nnne0 12269. A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0)
Theorem	nngt0i 12274	A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 0 < 𝐴
Theorem	nnne0i 12275	A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ≠ 0
Theorem	nndivre 12276	The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ)
Theorem	nnrecre 12277	The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.)
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ)
Theorem	nnrecgt0 12278	The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.)
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴))
Theorem	nnsub 12279	Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ))
Theorem	nnsubi 12280	Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)
Theorem	nndiv 12281*	Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ))
Theorem	nndivtr 12282	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 12283	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 1 ≤ 𝐴)
Theorem	nngt0d 12284	A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	nnne0d 12285	A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	nnrecred 12286	The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	nnaddcld 12287	Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ)
Theorem	nnmulcld 12288	Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Theorem	nndivred 12289	A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	1t1e1ALT 12290	Alternate proof of 1t1e1 12401 using a different set of axioms (add ax-mulrcl 11162, ax-i2m1 11167, ax-1ne0 11168, ax-rrecex 11171 and remove ax-resscn 11156, ax-mulcom 11163, ax-mulass 11165, ax-distr 11166). (Contributed by Steven Nguyen, 20-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (1 · 1) = 1
Theorem	nnadddir 12291	Right-distributivity for natural numbers without ax-mulcom 11163. (Contributed by SN, 5-Feb-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	nnmul1com 12292	Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11163. Since (𝐴 · 1) is 𝐴 by ax-1rid 11169, this is equivalent to remullid 43163 for natural numbers, but using fewer axioms (avoiding ax-resscn 11156, ax-addass 11164, ax-mulass 11165, ax-rnegex 11170, ax-pre-lttri 11173, ax-pre-lttrn 11174, ax-pre-ltadd 11175). (Contributed by SN, 5-Feb-2024.)
⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1))
Theorem	nnmulcom 12293	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 11106 through df-9 12309), 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 11106 and df-1 11107). With the decimal constructor df-dec 12711, it is possible to easily express larger integers in base 10. See deccl 12725 and the theorems that follow it. See also 4001prm 17204 (4001 is prime) and the proof of bpos 27433. 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 16243. 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 12294	Extend class notation to include the number 2.
class 2
Syntax	c3 12295	Extend class notation to include the number 3.
class 3
Syntax	c4 12296	Extend class notation to include the number 4.
class 4
Syntax	c5 12297	Extend class notation to include the number 5.
class 5
Syntax	c6 12298	Extend class notation to include the number 6.
class 6
Syntax	c7 12299	Extend class notation to include the number 7.
class 7
Syntax	c8 12300	Extend class notation to include the number 8.
class 8