P. 109 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gruun 10801	A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	gruxp 10802	A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	grumap 10803	A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	gruixp 10804*	A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruiin 10805*	A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruf 10806	A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈)
Theorem	gruen 10807	A Grothendieck universe contains all subsets of itself that are equipotent to an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ (𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴)) → 𝐴 ∈ 𝑈)
Theorem	gruwun 10808	A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni)
Theorem	intgru 10809	The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ)
Theorem	ingru 10810*	The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran 𝑦 ∈ 𝐴))) → (𝑈 ∈ Univ → (𝑈 ∩ 𝐴) ∈ Univ))
Theorem	wfgru 10811	The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ)
Theorem	grudomon 10812	Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵)) → 𝐴 ∈ 𝑈)
Theorem	gruina 10813	If a Grothendieck universe 𝑈 is nonempty, then the height of the ordinals in 𝑈 is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
Theorem	grur1a 10814	A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈)
Theorem	grur1 10815	A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))
Theorem	grutsk1 10816	Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10778.) (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ)
Theorem	grutsk 10817	Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥}
4.2  ZFC Set Theory plus the Tarski-Grothendieck Axiom
4.2.1  Introduce the Tarski-Grothendieck Axiom
Axiom	ax-groth 10818*	The Tarski-Grothendieck Axiom. For every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics". This version of the axiom is used by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html). Unlike the ZFC axioms, this axiom is very long when expressed in terms of primitive symbols (see grothprim 10829). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth5 10819*	The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
Theorem	axgroth2 10820*	Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
4.2.2  Derive the Power Set, Infinity and Choice Axioms
Theorem	grothpw 10821*	Derive the Axiom of Power Sets ax-pow 5364 from the Tarski-Grothendieck axiom ax-groth 10818. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10818. Note that ax-pow 5364 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	grothpwex 10822	Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10818. Note that ax-pow 5364 is not used by the proof. Use axpweq 5349 to obtain ax-pow 5364. Use pwex 5379 or pwexg 5377 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ 𝒫 𝑥 ∈ V
Theorem	axgroth6 10823*	The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set 𝑥, there exists a set 𝑦 containing 𝑥, the subsets of the members of 𝑦, the power sets of the members of 𝑦, and the subsets of 𝑦 of cardinality less than that of 𝑦. (Contributed by NM, 21-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦))
Theorem	grothomex 10824	The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9638). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ ω ∈ V
Theorem	grothac 10825	The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10464). This can be put in a more conventional form via ween 10030 and dfac8 10130. Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10130). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ dom card = V
Theorem	axgroth3 10826*	Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10430 is used to derive this version. (Contributed by NM, 26-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth4 10827*	Alternate version of the Tarski-Grothendieck Axiom. ax-ac 10454 is used to derive this version. (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	grothprimlem 10828*	Lemma for grothprim 10829. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.)
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
Theorem	grothprim 10829*	The Tarski-Grothendieck Axiom ax-groth 10818 expanded into set theory primitives using 163 symbols (allowing the defined symbols ∧, ∨, ↔, and ∃). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
Theorem	grothtsk 10830	The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.)
⊢ ∪ Tarski = V
Theorem	inaprc 10831	An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ Inacc ∉ V
4.2.3  Tarski map function
Syntax	ctskm 10832	Extend class definition to include the map whose value is the smallest Tarski class.
class tarskiMap
Definition	df-tskm 10833*	A function that maps a set 𝑥 to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.)
⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})
Theorem	tskmval 10834*	Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥})
Theorem	tskmid 10835	The set 𝐴 is an element of the smallest Tarski class that contains 𝐴. CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (tarskiMap‘𝐴))
Theorem	tskmcl 10836	A Tarski class that contains 𝐴 is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (tarskiMap‘𝐴) ∈ Tarski
Theorem	sstskm 10837*	Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥)))
Theorem	eltskm 10838*	Belonging to (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ∈ 𝑥)))
PART 5  REAL AND COMPLEX NUMBERS This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 11167). After that, we derive their basic properties, various operations like addition (df-add 11121) and sine (df-sin 16013), and subsets such as the integers (df-z 12559) and natural numbers (df-nn 12213).
5.1  Construction and axiomatization of real and complex numbers
5.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 10839	The set of positive integers, which is the set of natural numbers ω with 0 removed. Note: This is the start of the Dedekind-cut construction of real and complex numbers. The last lemma of the construction is mulcnsrec 11139. The actual set of Dedekind cuts is defined by df-np 10976.
class N
Syntax	cpli 10840	Positive integer addition.
class +N
Syntax	cmi 10841	Positive integer multiplication.
class ·N
Syntax	clti 10842	Positive integer ordering relation.
class <N
Syntax	cplpq 10843	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 10844	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 10845	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 10846	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 10847	Set of positive fractions.
class Q
Syntax	c1q 10848	The positive fraction constant 1.
class 1Q
Syntax	cerq 10849	Positive fraction equivalence class.
class [Q]
Syntax	cplq 10850	Positive fraction addition.
class +Q
Syntax	cmq 10851	Positive fraction multiplication.
class ·Q
Syntax	crq 10852	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10853	Positive fraction ordering relation.
class <Q
Syntax	cnp 10854	Set of positive reals.
class P
Syntax	c1p 10855	Positive real constant 1.
class 1P
Syntax	cpp 10856	Positive real addition.
class +P
Syntax	cmp 10857	Positive real multiplication.
class ·P
Syntax	cltp 10858	Positive real ordering relation.
class <P
Syntax	cer 10859	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10860	Set of signed reals.
class R
Syntax	c0r 10861	The signed real constant 0.
class 0R
Syntax	c1r 10862	The signed real constant 1.
class 1R
Syntax	cm1r 10863	The signed real constant -1.
class -1R
Syntax	cplr 10864	Signed real addition.
class +R
Syntax	cmr 10865	Signed real multiplication.
class ·R
Syntax	cltr 10866	Signed real ordering relation.
class <R
Definition	df-ni 10867	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11116, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10868	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11116, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ +N = ( +o ↾ (N × N))
Definition	df-mi 10869	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11116, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ·N = ( ·o ↾ (N × N))
Definition	df-lti 10870	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11116, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.)
⊢ <N = ( E ∩ (N × N))
Theorem	elni 10871	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10872	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
Theorem	pinn 10873	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
Theorem	pion 10874	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ On)
Theorem	piord 10875	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → Ord 𝐴)
Theorem	niex 10876	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N ∈ V
Theorem	0npi 10877	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ N
Theorem	1pi 10878	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1o ∈ N
Theorem	addpiord 10879	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵))
Theorem	mulpiord 10880	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵))
Theorem	mulidpi 10881	1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → (𝐴 ·N 1o) = 𝐴)
Theorem	ltpiord 10882	Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	ltsopi 10883	Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ <N Or N
Theorem	ltrelpi 10884	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ <N ⊆ (N × N)
Theorem	dmaddpi 10885	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom +N = (N × N)
Theorem	dmmulpi 10886	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom ·N = (N × N)
Theorem	addclpi 10887	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N)
Theorem	mulclpi 10888	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N)
Theorem	addcompi 10889	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴)
Theorem	addasspi 10890	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶))
Theorem	mulcompi 10891	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴)
Theorem	mulasspi 10892	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶))
Theorem	distrpi 10893	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶))
Theorem	addcanpi 10894	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpi 10895	Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 ·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	addnidpi 10896	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 10897*	Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +N 𝑥) = 𝐵))
Theorem	ltapi 10898	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
Theorem	ltmpi 10899	Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))
Theorem	1lt2pi 10900	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ 1o <N (1o +N 1o)