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	tskmcl 10801	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 10802*	Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥)))
Theorem	eltskm 10803*	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 11132). After that, we derive their basic properties, various operations like addition (df-add 11086) and sine (df-sin 16042), and subsets such as the integers (df-z 12537) and natural numbers (df-nn 12194).
5.1  Construction and axiomatization of real and complex numbers
5.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 10804	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 11104. The actual set of Dedekind cuts is defined by df-np 10941.
class N
Syntax	cpli 10805	Positive integer addition.
class +N
Syntax	cmi 10806	Positive integer multiplication.
class ·N
Syntax	clti 10807	Positive integer ordering relation.
class <N
Syntax	cplpq 10808	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 10809	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 10810	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 10811	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 10812	Set of positive fractions.
class Q
Syntax	c1q 10813	The positive fraction constant 1.
class 1Q
Syntax	cerq 10814	Positive fraction equivalence class.
class [Q]
Syntax	cplq 10815	Positive fraction addition.
class +Q
Syntax	cmq 10816	Positive fraction multiplication.
class ·Q
Syntax	crq 10817	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10818	Positive fraction ordering relation.
class <Q
Syntax	cnp 10819	Set of positive reals.
class P
Syntax	c1p 10820	Positive real constant 1.
class 1P
Syntax	cpp 10821	Positive real addition.
class +P
Syntax	cmp 10822	Positive real multiplication.
class ·P
Syntax	cltp 10823	Positive real ordering relation.
class <P
Syntax	cer 10824	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10825	Set of signed reals.
class R
Syntax	c0r 10826	The signed real constant 0.
class 0R
Syntax	c1r 10827	The signed real constant 1.
class 1R
Syntax	cm1r 10828	The signed real constant -1.
class -1R
Syntax	cplr 10829	Signed real addition.
class +R
Syntax	cmr 10830	Signed real multiplication.
class ·R
Syntax	cltr 10831	Signed real ordering relation.
class <R
Definition	df-ni 10832	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10833	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10834	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10835	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10836	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10837	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
Theorem	pinn 10838	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
Theorem	pion 10839	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ On)
Theorem	piord 10840	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → Ord 𝐴)
Theorem	niex 10841	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N ∈ V
Theorem	0npi 10842	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ N
Theorem	1pi 10843	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1o ∈ N
Theorem	addpiord 10844	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵))
Theorem	mulpiord 10845	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵))
Theorem	mulidpi 10846	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 10847	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 10848	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 10849	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 10850	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom +N = (N × N)
Theorem	dmmulpi 10851	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom ·N = (N × N)
Theorem	addclpi 10852	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N)
Theorem	mulclpi 10853	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N)
Theorem	addcompi 10854	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴)
Theorem	addasspi 10855	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶))
Theorem	mulcompi 10856	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴)
Theorem	mulasspi 10857	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶))
Theorem	distrpi 10858	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶))
Theorem	addcanpi 10859	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpi 10860	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 10861	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 10862*	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 10863	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
Theorem	ltmpi 10864	Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))
Theorem	1lt2pi 10865	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 10866	No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ ¬ 𝐴 <N 1o
Theorem	indpi 10867*	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 10868*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10874) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10871). (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 10869*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10870*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10871*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10872*	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, 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 10873	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 10890. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ [Q] = ( ~Q ∩ ((N × N) × Q))
Definition	df-plq 10874	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 24-Aug-1995.) (New usage is discouraged.)
⊢ +Q = (([Q] ∘ +pQ ) ↾ (Q × Q))
Definition	df-mq 10875	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 24-Aug-1995.) (New usage is discouraged.)
⊢ ·Q = (([Q] ∘ ·pQ ) ↾ (Q × Q))
Definition	df-1nq 10876	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1Q = ⟨1o, 1o⟩
Definition	df-rq 10877	Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by NM, 6-Mar-1996.) (New usage is discouraged.)
⊢ *Q = (◡ ·Q “ {1Q})
Definition	df-ltnq 10878	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11081, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.) (New usage is discouraged.)
⊢ <Q = ( <pQ ∩ (Q × Q))
Theorem	enqbreq 10879	Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ ~Q ⟨𝐶, 𝐷⟩ ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶)))
Theorem	enqbreq2 10880	Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ((1st ‘𝐴) ·N (2nd ‘𝐵)) = ((1st ‘𝐵) ·N (2nd ‘𝐴))))
Theorem	enqer 10881	The equivalence relation for positive fractions is an equivalence relation. Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.)
⊢ ~Q Er (N × N)
Theorem	enqex 10882	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ~Q ∈ V
Theorem	nqex 10883	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
⊢ Q ∈ V
Theorem	0nnq 10884	The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ Q
Theorem	elpqn 10885	Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N))
Theorem	ltrelnq 10886	Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
⊢ <Q ⊆ (Q × Q)
Theorem	pinq 10887	The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ⟨𝐴, 1o⟩ ∈ Q)
Theorem	1nq 10888	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ 1Q ∈ Q
Theorem	nqereu 10889*	There is a unique element of Q equivalent to each element of N × N. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴)
Theorem	nqerf 10890	Corollary of nqereu 10889: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ [Q]:(N × N)⟶Q
Theorem	nqercl 10891	Corollary of nqereu 10889: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q)
Theorem	nqerrel 10892	Any member of (N × N) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ (N × N) → 𝐴 ~Q ([Q]‘𝐴))
Theorem	nqerid 10893	Corollary of nqereu 10889: the function [Q] acts as the identity on members of Q. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴)
Theorem	enqeq 10894	Corollary of nqereu 10889: if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~Q 𝐵) → 𝐴 = 𝐵)
Theorem	nqereq 10895	The function [Q] acts as a substitute for equivalence classes, and it satisfies the fundamental requirement for equivalence representatives: the representatives are equal iff the members are equivalent. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ([Q]‘𝐴) = ([Q]‘𝐵)))
Theorem	addpipq2 10896	Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 +pQ 𝐵) = ⟨(((1st ‘𝐴) ·N (2nd ‘𝐵)) +N ((1st ‘𝐵) ·N (2nd ‘𝐴))), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
Theorem	addpipq 10897	Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ +pQ ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·N 𝐷) +N (𝐶 ·N 𝐵)), (𝐵 ·N 𝐷)⟩)
Theorem	addpqnq 10898	Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) = ([Q]‘(𝐴 +pQ 𝐵)))
Theorem	mulpipq2 10899	Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
Theorem	mulpipq 10900	Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ ·pQ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 ·N 𝐶), (𝐵 ·N 𝐷)⟩)