P. 106 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10501-10600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	intgru 10501	The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ)
Theorem	ingru 10502*	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 10503	The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ)
Theorem	grudomon 10504	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 10505	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 10506	A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈)
Theorem	grur1 10507	A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))
Theorem	grutsk1 10508	Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10470.) (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ)
Theorem	grutsk 10509	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 10510*	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 10521). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth5 10511*	The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
Theorem	axgroth2 10512*	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 10513*	Derive the Axiom of Power Sets ax-pow 5283 from the Tarski-Grothendieck axiom ax-groth 10510. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10510. Note that ax-pow 5283 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	grothpwex 10514	Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10510. Note that ax-pow 5283 is not used by the proof. Use axpweq 5282 to obtain ax-pow 5283. Use pwex 5298 or pwexg 5296 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ 𝒫 𝑥 ∈ V
Theorem	axgroth6 10515*	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 10516	The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9331). 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 10517	The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10156). This can be put in a more conventional form via ween 9722 and dfac8 9822. 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 9822). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ dom card = V
Theorem	axgroth3 10518*	Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10122 is used to derive this version. (Contributed by NM, 26-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth4 10519*	Alternate version of the Tarski-Grothendieck Axiom. ax-ac 10146 is used to derive this version. (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	grothprimlem 10520*	Lemma for grothprim 10521. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.)
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
Theorem	grothprim 10521*	The Tarski-Grothendieck Axiom ax-groth 10510 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 10522	The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.)
⊢ ∪ Tarski = V
Theorem	inaprc 10523	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 10524	Extend class definition to include the map whose value is the smallest Tarski class.
class tarskiMap
Definition	df-tskm 10525*	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 10526*	Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥})
Theorem	tskmid 10527	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 10528	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 10529*	Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥)))
Theorem	eltskm 10530*	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 10859). After that, we derive their basic properties, various operations like addition (df-add 10813) and sine (df-sin 15707), and subsets such as the integers (df-z 12250) and natural numbers (df-nn 11904).
5.1  Construction and axiomatization of real and complex numbers
5.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 10531	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 10831. The actual set of Dedekind cuts is defined by df-np 10668.
class N
Syntax	cpli 10532	Positive integer addition.
class +N
Syntax	cmi 10533	Positive integer multiplication.
class ·N
Syntax	clti 10534	Positive integer ordering relation.
class <N
Syntax	cplpq 10535	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 10536	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 10537	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 10538	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 10539	Set of positive fractions.
class Q
Syntax	c1q 10540	The positive fraction constant 1.
class 1Q
Syntax	cerq 10541	Positive fraction equivalence class.
class [Q]
Syntax	cplq 10542	Positive fraction addition.
class +Q
Syntax	cmq 10543	Positive fraction multiplication.
class ·Q
Syntax	crq 10544	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10545	Positive fraction ordering relation.
class <Q
Syntax	cnp 10546	Set of positive reals.
class P
Syntax	c1p 10547	Positive real constant 1.
class 1P
Syntax	cpp 10548	Positive real addition.
class +P
Syntax	cmp 10549	Positive real multiplication.
class ·P
Syntax	cltp 10550	Positive real ordering relation.
class <P
Syntax	cer 10551	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10552	Set of signed reals.
class R
Syntax	c0r 10553	The signed real constant 0.
class 0R
Syntax	c1r 10554	The signed real constant 1.
class 1R
Syntax	cm1r 10555	The signed real constant -1.
class -1R
Syntax	cplr 10556	Signed real addition.
class +R
Syntax	cmr 10557	Signed real multiplication.
class ·R
Syntax	cltr 10558	Signed real ordering relation.
class <R
Definition	df-ni 10559	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10560	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10808, 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 10561	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10808, 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 10562	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10808, 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 10563	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10564	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
Theorem	pinn 10565	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
Theorem	pion 10566	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ On)
Theorem	piord 10567	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → Ord 𝐴)
Theorem	niex 10568	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N ∈ V
Theorem	0npi 10569	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ N
Theorem	1pi 10570	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1o ∈ N
Theorem	addpiord 10571	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵))
Theorem	mulpiord 10572	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵))
Theorem	mulidpi 10573	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 10574	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 10575	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 10576	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 10577	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom +N = (N × N)
Theorem	dmmulpi 10578	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom ·N = (N × N)
Theorem	addclpi 10579	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N)
Theorem	mulclpi 10580	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N)
Theorem	addcompi 10581	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴)
Theorem	addasspi 10582	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶))
Theorem	mulcompi 10583	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴)
Theorem	mulasspi 10584	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶))
Theorem	distrpi 10585	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶))
Theorem	addcanpi 10586	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpi 10587	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 10588	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 10589*	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 10590	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
Theorem	ltmpi 10591	Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))
Theorem	1lt2pi 10592	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
⊢ 1o <N (1o +N 1o)
Theorem	nlt1pi 10593	No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ ¬ 𝐴 <N 1o
Theorem	indpi 10594*	Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ N → 𝜏)
Definition	df-plpq 10595*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition +Q (df-plq 10601) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10598). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 28-Aug-1995.) (New usage is discouraged.)
⊢ +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st ‘𝑥) ·N (2nd ‘𝑦)) +N ((1st ‘𝑦) ·N (2nd ‘𝑥))), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
Definition	df-mpq 10596*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 28-Aug-1995.) (New usage is discouraged.)
⊢ ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st ‘𝑥) ·N (1st ‘𝑦)), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
Definition	df-ltpq 10597*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.) (New usage is discouraged.)
⊢ <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st ‘𝑥) ·N (2nd ‘𝑦)) <N ((1st ‘𝑦) ·N (2nd ‘𝑥)))}
Definition	df-enq 10598*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. From Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
Definition	df-nq 10599*	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10808, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.) (New usage is discouraged.)
⊢ Q = {𝑥 ∈ (N × N) ∣ ∀𝑦 ∈ (N × N)(𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))}
Definition	df-erq 10600	Define a convenience function that "reduces" a fraction to lowest terms. Note that in this form, it is not obviously a function; we prove this in nqerf 10617. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ [Q] = ( ~Q ∩ ((N × N) × Q))