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
Syntax	cmq 10801	Positive fraction multiplication.
class ·Q
Syntax	crq 10802	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10803	Positive fraction ordering relation.
class <Q
Syntax	cnp 10804	Set of positive reals.
class P
Syntax	c1p 10805	Positive real constant 1.
class 1P
Syntax	cpp 10806	Positive real addition.
class +P
Syntax	cmp 10807	Positive real multiplication.
class ·P
Syntax	cltp 10808	Positive real ordering relation.
class <P
Syntax	cer 10809	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10810	Set of signed reals.
class R
Syntax	c0r 10811	The signed real constant 0.
class 0R
Syntax	c1r 10812	The signed real constant 1.
class 1R
Syntax	cm1r 10813	The signed real constant -1.
class -1R
Syntax	cplr 10814	Signed real addition.
class +R
Syntax	cmr 10815	Signed real multiplication.
class ·R
Syntax	cltr 10816	Signed real ordering relation.
class <R
Definition	df-ni 10817	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11066, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10818	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10819	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10820	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10821	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10822	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
Theorem	pinn 10823	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
Theorem	pion 10824	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ On)
Theorem	piord 10825	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → Ord 𝐴)
Theorem	niex 10826	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N ∈ V
Theorem	0npi 10827	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ N
Theorem	1pi 10828	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1o ∈ N
Theorem	addpiord 10829	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵))
Theorem	mulpiord 10830	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵))
Theorem	mulidpi 10831	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 10832	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 10833	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 10834	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 10835	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom +N = (N × N)
Theorem	dmmulpi 10836	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom ·N = (N × N)
Theorem	addclpi 10837	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N)
Theorem	mulclpi 10838	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N)
Theorem	addcompi 10839	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴)
Theorem	addasspi 10840	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶))
Theorem	mulcompi 10841	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴)
Theorem	mulasspi 10842	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶))
Theorem	distrpi 10843	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶))
Theorem	addcanpi 10844	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpi 10845	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 10846	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 10847*	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 10848	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
Theorem	ltmpi 10849	Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))
Theorem	1lt2pi 10850	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 10851	No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ ¬ 𝐴 <N 1o
Theorem	indpi 10852*	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 10853*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10859) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10856). (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 10854*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10855*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10856*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10857*	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10858	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 10875. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ [Q] = ( ~Q ∩ ((N × N) × Q))
Definition	df-plq 10859	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10860	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10861	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10862	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 11066, 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 10863	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11066, 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 10864	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 10865	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 10866	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 10867	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ~Q ∈ V
Theorem	nqex 10868	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 10869	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 10870	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 10871	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 10872	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 10873	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 10874*	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 10875	Corollary of nqereu 10874: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ [Q]:(N × N)⟶Q
Theorem	nqercl 10876	Corollary of nqereu 10874: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q)
Theorem	nqerrel 10877	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 10878	Corollary of nqereu 10874: 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 10879	Corollary of nqereu 10874: 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 10880	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 10881	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 10882	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 10883	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 10884	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 10885	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 𝐷)⟩)
Theorem	mulpqnq 10886	Multiplication 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	ordpipq 10887	Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ (⟨𝐴, 𝐵⟩ <pQ ⟨𝐶, 𝐷⟩ ↔ (𝐴 ·N 𝐷) <N (𝐶 ·N 𝐵))
Theorem	ordpinq 10888	Ordering of positive fractions in terms of positive integers. (Contributed by NM, 13-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ((1st ‘𝐴) ·N (2nd ‘𝐵)) <N ((1st ‘𝐵) ·N (2nd ‘𝐴))))
Theorem	addpqf 10889	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ +pQ :((N × N) × (N × N))⟶(N × N)
Theorem	addclnq 10890	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q)
Theorem	mulpqf 10891	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ·pQ :((N × N) × (N × N))⟶(N × N)
Theorem	mulclnq 10892	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) ∈ Q)
Theorem	addnqf 10893	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ +Q :(Q × Q)⟶Q
Theorem	mulnqf 10894	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ ·Q :(Q × Q)⟶Q
Theorem	addcompq 10895	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 +pQ 𝐵) = (𝐵 +pQ 𝐴)
Theorem	addcomnq 10896	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴)
Theorem	mulcompq 10897	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ·pQ 𝐵) = (𝐵 ·pQ 𝐴)
Theorem	mulcomnq 10898	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
⊢ (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴)
Theorem	adderpqlem 10899	Lemma for adderpq 10901. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶)))
Theorem	mulerpqlem 10900	Lemma for mulerpq 10902. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶)))