P. 72 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7101-7200   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-mpq 7101*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨((1st ‘𝑥) ·N (1st ‘𝑦)), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
Definition	df-ltpq 7102*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.)
⊢ <pQ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st ‘𝑥) ·N (2nd ‘𝑦)) <N ((1st ‘𝑦) ·N (2nd ‘𝑥)))}
Definition	df-enq 7103*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ ~Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))}
Definition	df-nqqs 7104	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ Q = ((N × N) / ~Q )
Definition	df-plqqs 7105*	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ +Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ +pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
Definition	df-mqqs 7106*	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ ·Q = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q ) ∧ 𝑧 = [(⟨𝑤, 𝑣⟩ ·pQ ⟨𝑢, 𝑓⟩)] ~Q ))}
Definition	df-1nqqs 7107	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers, 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.)
⊢ 1Q = [⟨1o, 1o⟩] ~Q
Definition	df-rq 7108*	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, 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 Jim Kingdon, 20-Sep-2019.)
⊢ *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
Definition	df-ltnqqs 7109*	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)
⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
Theorem	dfplpq2 7110*	Alternate definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
⊢ +pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·N 𝑓) +N (𝑣 ·N 𝑢)), (𝑣 ·N 𝑓)⟩))}
Theorem	dfmpq2 7111*	Alternate definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
⊢ ·pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·N 𝑢), (𝑣 ·N 𝑓)⟩))}
Theorem	enqbreq 7112	Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ ~Q ⟨𝐶, 𝐷⟩ ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶)))
Theorem	enqbreq2 7113	Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ((1st ‘𝐴) ·N (2nd ‘𝐵)) = ((1st ‘𝐵) ·N (2nd ‘𝐴))))
Theorem	enqer 7114	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.)
⊢ ~Q Er (N × N)
Theorem	enqeceq 7115	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ([⟨𝐴, 𝐵⟩] ~Q = [⟨𝐶, 𝐷⟩] ~Q ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶)))
Theorem	enqex 7116	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
⊢ ~Q ∈ V
Theorem	enqdc 7117	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → DECID ⟨𝐴, 𝐵⟩ ~Q ⟨𝐶, 𝐷⟩)
Theorem	enqdc1 7118	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ 𝐶 ∈ (N × N)) → DECID ⟨𝐴, 𝐵⟩ ~Q 𝐶)
Theorem	nqex 7119	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
⊢ Q ∈ V
Theorem	0nnq 7120	The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
⊢ ¬ ∅ ∈ Q
Theorem	ltrelnq 7121	Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)
⊢ <Q ⊆ (Q × Q)
Theorem	1nq 7122	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
⊢ 1Q ∈ Q
Theorem	addcmpblnq 7123	Lemma showing compatibility of addition. (Contributed by NM, 27-Aug-1995.)
⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ N ∧ 𝑆 ∈ N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩))
Theorem	mulcmpblnq 7124	Lemma showing compatibility of multiplication. (Contributed by NM, 27-Aug-1995.)
⊢ ((((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ N ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ N ∧ 𝑆 ∈ N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ⟨(𝐴 ·N 𝐹), (𝐵 ·N 𝐺)⟩ ~Q ⟨(𝐶 ·N 𝑅), (𝐷 ·N 𝑆)⟩))
Theorem	addpipqqslem 7125	Lemma for addpipqqs 7126. (Contributed by Jim Kingdon, 11-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ⟨((𝐴 ·N 𝐷) +N (𝐵 ·N 𝐶)), (𝐵 ·N 𝐷)⟩ ∈ (N × N))
Theorem	addpipqqs 7126	Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ([⟨𝐴, 𝐵⟩] ~Q +Q [⟨𝐶, 𝐷⟩] ~Q ) = [⟨((𝐴 ·N 𝐷) +N (𝐵 ·N 𝐶)), (𝐵 ·N 𝐷)⟩] ~Q )
Theorem	mulpipq2 7127	Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = ⟨((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))⟩)
Theorem	mulpipq 7128	Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ ·pQ ⟨𝐶, 𝐷⟩) = ⟨(𝐴 ·N 𝐶), (𝐵 ·N 𝐷)⟩)
Theorem	mulpipqqs 7129	Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ([⟨𝐴, 𝐵⟩] ~Q ·Q [⟨𝐶, 𝐷⟩] ~Q ) = [⟨(𝐴 ·N 𝐶), (𝐵 ·N 𝐷)⟩] ~Q )
Theorem	ordpipqqs 7130	Ordering of positive fractions in terms of positive integers. (Contributed by Jim Kingdon, 14-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ([⟨𝐴, 𝐵⟩] ~Q <Q [⟨𝐶, 𝐷⟩] ~Q ↔ (𝐴 ·N 𝐷) <N (𝐵 ·N 𝐶)))
Theorem	addclnq 7131	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q)
Theorem	mulclnq 7132	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) ∈ Q)
Theorem	dmaddpqlem 7133*	Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 7135. (Contributed by Jim Kingdon, 15-Sep-2019.)
⊢ (𝑥 ∈ Q → ∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q )
Theorem	nqpi 7134*	Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 7133 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑤∃𝑣((𝑤 ∈ N ∧ 𝑣 ∈ N) ∧ 𝐴 = [⟨𝑤, 𝑣⟩] ~Q ))
Theorem	dmaddpq 7135	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
⊢ dom +Q = (Q × Q)
Theorem	dmmulpq 7136	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
⊢ dom ·Q = (Q × Q)
Theorem	addcomnqg 7137	Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))
Theorem	addassnqg 7138	Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 +Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q 𝐶)))
Theorem	mulcomnqg 7139	Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴))
Theorem	mulassnqg 7140	Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵 ·Q 𝐶)))
Theorem	mulcanenq 7141	Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩ ~Q ⟨𝐵, 𝐶⟩)
Theorem	mulcanenqec 7142	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → [⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩] ~Q = [⟨𝐵, 𝐶⟩] ~Q )
Theorem	distrnqg 7143	Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
Theorem	1qec 7144	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
⊢ (𝐴 ∈ N → 1Q = [⟨𝐴, 𝐴⟩] ~Q )
Theorem	mulidnq 7145	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴)
Theorem	recexnq 7146*	Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑦(𝑦 ∈ Q ∧ (𝐴 ·Q 𝑦) = 1Q))
Theorem	recmulnqg 7147	Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Theorem	recclnq 7148	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ Q)
Theorem	recidnq 7149	A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
⊢ (𝐴 ∈ Q → (𝐴 ·Q (*Q‘𝐴)) = 1Q)
Theorem	recrecnq 7150	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
⊢ (𝐴 ∈ Q → (*Q‘(*Q‘𝐴)) = 𝐴)
Theorem	rec1nq 7151	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ (*Q‘1Q) = 1Q
Theorem	nqtri3or 7152	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴))
Theorem	ltdcnq 7153	Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → DECID 𝐴 <Q 𝐵)
Theorem	ltsonq 7154	'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
⊢ <Q Or Q
Theorem	nqtric 7155	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴)))
Theorem	ltanqg 7156	Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵)))
Theorem	ltmnqg 7157	Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵)))
Theorem	ltanqi 7158	Ordering property of addition for positive fractions. One direction of ltanqg 7156. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵))
Theorem	ltmnqi 7159	Ordering property of multiplication for positive fractions. One direction of ltmnqg 7157. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))
Theorem	lt2addnq 7160	Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧ (𝐶 ∈ Q ∧ 𝐷 ∈ Q)) → ((𝐴 <Q 𝐵 ∧ 𝐶 <Q 𝐷) → (𝐴 +Q 𝐶) <Q (𝐵 +Q 𝐷)))
Theorem	lt2mulnq 7161	Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.)
⊢ (((𝐴 ∈ Q ∧ 𝐵 ∈ Q) ∧ (𝐶 ∈ Q ∧ 𝐷 ∈ Q)) → ((𝐴 <Q 𝐵 ∧ 𝐶 <Q 𝐷) → (𝐴 ·Q 𝐶) <Q (𝐵 ·Q 𝐷)))
Theorem	1lt2nq 7162	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 1Q <Q (1Q +Q 1Q)
Theorem	ltaddnq 7163	The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 <Q (𝐴 +Q 𝐵))
Theorem	ltexnqq 7164*	Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by Jim Kingdon, 23-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵))
Theorem	ltexnqi 7165*	Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
⊢ (𝐴 <Q 𝐵 → ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵)
Theorem	halfnqq 7166*	One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝐴)
Theorem	halfnq 7167*	One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 16-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ (𝐴 ∈ Q → ∃𝑥(𝑥 +Q 𝑥) = 𝐴)
Theorem	nsmallnqq 7168*	There is no smallest positive fraction. (Contributed by Jim Kingdon, 24-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q 𝑥 <Q 𝐴)
Theorem	nsmallnq 7169*	There is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ (𝐴 ∈ Q → ∃𝑥 𝑥 <Q 𝐴)
Theorem	subhalfnqq 7170*	There is a number which is less than half of any positive fraction. The case where 𝐴 is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 7166). (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) <Q 𝐴)
Theorem	ltbtwnnqq 7171*	There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by Jim Kingdon, 24-Sep-2019.)
⊢ (𝐴 <Q 𝐵 ↔ ∃𝑥 ∈ Q (𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))
Theorem	ltbtwnnq 7172*	There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵))
Theorem	archnqq 7173*	For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ N 𝐴 <Q [⟨𝑥, 1o⟩] ~Q )
Theorem	prarloclemarch 7174*	A version of the Archimedean property. This variation is "stronger" than archnqq 7173 in the sense that we provide an integer which is larger than a given rational 𝐴 even after being multiplied by a second rational 𝐵. (Contributed by Jim Kingdon, 30-Nov-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ∃𝑥 ∈ N 𝐴 <Q ([⟨𝑥, 1o⟩] ~Q ·Q 𝐵))
Theorem	prarloclemarch2 7175*	Like prarloclemarch 7174 but the integer must be at least two, and there is also 𝐵 added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 7259. (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑥 ∈ N (1o <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q ([⟨𝑥, 1o⟩] ~Q ·Q 𝐶))))
Theorem	ltrnqg 7176	Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 7177. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ (*Q‘𝐵) <Q (*Q‘𝐴)))
Theorem	ltrnqi 7177	Ordering property of reciprocal for positive fractions. For the converse, see ltrnqg 7176. (Contributed by Jim Kingdon, 24-Sep-2019.)
⊢ (𝐴 <Q 𝐵 → (*Q‘𝐵) <Q (*Q‘𝐴))
Theorem	nnnq 7178	The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
⊢ (𝐴 ∈ N → [⟨𝐴, 1o⟩] ~Q ∈ Q)
Theorem	ltnnnq 7179	Ordering of positive integers via <N or <Q is equivalent. (Contributed by Jim Kingdon, 3-Oct-2020.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ [⟨𝐴, 1o⟩] ~Q <Q [⟨𝐵, 1o⟩] ~Q ))
Definition	df-enq0 7180*	Define equivalence relation for nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
⊢ ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·o 𝑢) = (𝑤 ·o 𝑣)))}
Definition	df-nq0 7181	Define class of nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
⊢ Q0 = ((ω × N) / ~Q0 )
Definition	df-0nq0 7182	Define nonnegative fraction constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 5-Nov-2019.)
⊢ 0Q0 = [⟨∅, 1o⟩] ~Q0
Definition	df-plq0 7183*	Define addition on nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
⊢ +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Definition	df-mq0 7184*	Define multiplication on nonnegative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
⊢ ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ Q0 ∧ 𝑦 ∈ Q0) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Theorem	dfmq0qs 7185*	Multiplication on nonnegative fractions. This definition is similar to df-mq0 7184 but expands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.)
⊢ ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Theorem	dfplq0qs 7186*	Addition on nonnegative fractions. This definition is similar to df-plq0 7183 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Theorem	enq0enq 7187	Equivalence on positive fractions in terms of equivalence on nonnegative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.)
⊢ ~Q = ( ~Q0 ∩ ((N × N) × (N × N)))
Theorem	enq0sym 7188	The equivalence relation for nonnegative fractions is symmetric. Lemma for enq0er 7191. (Contributed by Jim Kingdon, 14-Nov-2019.)
⊢ (𝑓 ~Q0 𝑔 → 𝑔 ~Q0 𝑓)
Theorem	enq0ref 7189	The equivalence relation for nonnegative fractions is reflexive. Lemma for enq0er 7191. (Contributed by Jim Kingdon, 14-Nov-2019.)
⊢ (𝑓 ∈ (ω × N) ↔ 𝑓 ~Q0 𝑓)
Theorem	enq0tr 7190	The equivalence relation for nonnegative fractions is transitive. Lemma for enq0er 7191. (Contributed by Jim Kingdon, 14-Nov-2019.)
⊢ ((𝑓 ~Q0 𝑔 ∧ 𝑔 ~Q0 ℎ) → 𝑓 ~Q0 ℎ)
Theorem	enq0er 7191	The equivalence relation for nonnegative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.)
⊢ ~Q0 Er (ω × N)
Theorem	enq0breq 7192	Equivalence relation for nonnegative fractions in terms of natural numbers. (Contributed by NM, 27-Aug-1995.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) → (⟨𝐴, 𝐵⟩ ~Q0 ⟨𝐶, 𝐷⟩ ↔ (𝐴 ·o 𝐷) = (𝐵 ·o 𝐶)))
Theorem	enq0eceq 7193	Equivalence class equality of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) → ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ↔ (𝐴 ·o 𝐷) = (𝐵 ·o 𝐶)))
Theorem	nqnq0pi 7194	A nonnegative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q )
Theorem	enq0ex 7195	The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ ~Q0 ∈ V
Theorem	nq0ex 7196	The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ Q0 ∈ V
Theorem	nqnq0 7197	A positive fraction is a nonnegative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)
⊢ Q ⊆ Q0
Theorem	nq0nn 7198*	Decomposition of a nonnegative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ (𝐴 ∈ Q0 → ∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [⟨𝑤, 𝑣⟩] ~Q0 ))
Theorem	addcmpblnq0 7199	Lemma showing compatibility of addition on nonnegative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ ω ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ ω ∧ 𝑆 ∈ N))) → (((𝐴 ·o 𝐷) = (𝐵 ·o 𝐶) ∧ (𝐹 ·o 𝑆) = (𝐺 ·o 𝑅)) → ⟨((𝐴 ·o 𝐺) +o (𝐵 ·o 𝐹)), (𝐵 ·o 𝐺)⟩ ~Q0 ⟨((𝐶 ·o 𝑆) +o (𝐷 ·o 𝑅)), (𝐷 ·o 𝑆)⟩))
Theorem	mulcmpblnq0 7200	Lemma showing compatibility of multiplication on nonnegative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ ω ∧ 𝐷 ∈ N)) ∧ ((𝐹 ∈ ω ∧ 𝐺 ∈ N) ∧ (𝑅 ∈ ω ∧ 𝑆 ∈ N))) → (((𝐴 ·o 𝐷) = (𝐵 ·o 𝐶) ∧ (𝐹 ·o 𝑆) = (𝐺 ·o 𝑅)) → ⟨(𝐴 ·o 𝐹), (𝐵 ·o 𝐺)⟩ ~Q0 ⟨(𝐶 ·o 𝑅), (𝐷 ·o 𝑆)⟩))