P. 78 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7701-7800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	distrpig 7701	Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)))
Theorem	addcanpig 7702	Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpig 7703	Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 ·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	addnidpig 7704	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 7705*	Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +N 𝑥) = 𝐵))
Theorem	ltapig 7706	Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
Theorem	ltmpig 7707	Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))
Theorem	1lt2pi 7708	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
⊢ 1o <N (1o +N 1o)
Theorem	nlt1pig 7709	No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
⊢ (𝐴 ∈ N → ¬ 𝐴 <N 1o)
Theorem	indpi 7710*	Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ N → 𝜏)
Theorem	nnppipi 7711	A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → (𝐴 +o 𝐵) ∈ N)
Definition	df-plpq 7712*	Define pre-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. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition +Q (df-plqqs 7717) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 7715). (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.)
⊢ +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st ‘𝑥) ·N (2nd ‘𝑦)) +N ((1st ‘𝑦) ·N (2nd ‘𝑥))), ((2nd ‘𝑥) ·N (2nd ‘𝑦))⟩)
Definition	df-mpq 7713*	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 7714*	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 7715*	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 7716	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 7717*	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 7718*	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 7719	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 7720*	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 7721*	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 7722*	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 7723*	Alternate definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
⊢ ·pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·N 𝑢), (𝑣 ·N 𝑓)⟩))}
Theorem	enqbreq 7724	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 7725	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 7726	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 7727	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 7728	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
⊢ ~Q ∈ V
Theorem	enqdc 7729	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → DECID ⟨𝐴, 𝐵⟩ ~Q ⟨𝐶, 𝐷⟩)
Theorem	enqdc1 7730	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ 𝐶 ∈ (N × N)) → DECID ⟨𝐴, 𝐵⟩ ~Q 𝐶)
Theorem	nqex 7731	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
⊢ Q ∈ V
Theorem	0nnq 7732	The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
⊢ ¬ ∅ ∈ Q
Theorem	ltrelnq 7733	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 7734	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
⊢ 1Q ∈ Q
Theorem	addcmpblnq 7735	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 7736	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 7737	Lemma for addpipqqs 7738. (Contributed by Jim Kingdon, 11-Sep-2019.)
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → ⟨((𝐴 ·N 𝐷) +N (𝐵 ·N 𝐶)), (𝐵 ·N 𝐷)⟩ ∈ (N × N))
Theorem	addpipqqs 7738	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 7739	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 7740	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 7741	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 7742	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 7743	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q)
Theorem	mulclnq 7744	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) ∈ Q)
Theorem	dmaddpqlem 7745*	Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 7747. (Contributed by Jim Kingdon, 15-Sep-2019.)
⊢ (𝑥 ∈ Q → ∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q )
Theorem	nqpi 7746*	Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 7745 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑤∃𝑣((𝑤 ∈ N ∧ 𝑣 ∈ N) ∧ 𝐴 = [⟨𝑤, 𝑣⟩] ~Q ))
Theorem	dmaddpq 7747	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
⊢ dom +Q = (Q × Q)
Theorem	dmmulpq 7748	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
⊢ dom ·Q = (Q × Q)
Theorem	addcomnqg 7749	Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))
Theorem	addassnqg 7750	Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 +Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q 𝐶)))
Theorem	mulcomnqg 7751	Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴))
Theorem	mulassnqg 7752	Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ((𝐴 ·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵 ·Q 𝐶)))
Theorem	mulcanenq 7753	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 7754	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → [⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩] ~Q = [⟨𝐵, 𝐶⟩] ~Q )
Theorem	distrnqg 7755	Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))
Theorem	1qec 7756	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
⊢ (𝐴 ∈ N → 1Q = [⟨𝐴, 𝐴⟩] ~Q )
Theorem	mulidnq 7757	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴)
Theorem	recexnq 7758*	Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑦(𝑦 ∈ Q ∧ (𝐴 ·Q 𝑦) = 1Q))
Theorem	recmulnqg 7759	Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Theorem	recclnq 7760	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ Q)
Theorem	recidnq 7761	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 7762	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
⊢ (𝐴 ∈ Q → (*Q‘(*Q‘𝐴)) = 𝐴)
Theorem	rec1nq 7763	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ (*Q‘1Q) = 1Q
Theorem	nqtri3or 7764	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴))
Theorem	ltdcnq 7765	Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → DECID 𝐴 <Q 𝐵)
Theorem	ltsonq 7766	'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 7767	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <Q 𝐴)))
Theorem	ltanqg 7768	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 7769	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 7770	Ordering property of addition for positive fractions. One direction of ltanqg 7768. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵))
Theorem	ltmnqi 7771	Ordering property of multiplication for positive fractions. One direction of ltmnqg 7769. (Contributed by Jim Kingdon, 9-Dec-2019.)
⊢ ((𝐴 <Q 𝐵 ∧ 𝐶 ∈ Q) → (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))
Theorem	lt2addnq 7772	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 7773	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 7774	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 7775	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 7776*	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 7777*	Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
⊢ (𝐴 <Q 𝐵 → ∃𝑥 ∈ Q (𝐴 +Q 𝑥) = 𝐵)
Theorem	halfnqq 7778*	One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) = 𝐴)
Theorem	halfnq 7779*	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 7780*	There is no smallest positive fraction. (Contributed by Jim Kingdon, 24-Sep-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q 𝑥 <Q 𝐴)
Theorem	nsmallnq 7781*	There is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ (𝐴 ∈ Q → ∃𝑥 𝑥 <Q 𝐴)
Theorem	subhalfnqq 7782*	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 7778). (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ Q (𝑥 +Q 𝑥) <Q 𝐴)
Theorem	ltbtwnnqq 7783*	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 7784*	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 7785*	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 7786*	A version of the Archimedean property. This variation is "stronger" than archnqq 7785 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 7787*	Like prarloclemarch 7786 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 7871. (Contributed by Jim Kingdon, 25-Nov-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑥 ∈ N (1o <N 𝑥 ∧ 𝐴 <Q (𝐵 +Q ([⟨𝑥, 1o⟩] ~Q ·Q 𝐶))))
Theorem	ltrnqg 7788	Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 7789. (Contributed by Jim Kingdon, 29-Dec-2019.)
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ (*Q‘𝐵) <Q (*Q‘𝐴)))
Theorem	ltrnqi 7789	Ordering property of reciprocal for positive fractions. For the converse, see ltrnqg 7788. (Contributed by Jim Kingdon, 24-Sep-2019.)
⊢ (𝐴 <Q 𝐵 → (*Q‘𝐵) <Q (*Q‘𝐴))
Theorem	nnnq 7790	The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
⊢ (𝐴 ∈ N → [⟨𝐴, 1o⟩] ~Q ∈ Q)
Theorem	ltnnnq 7791	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 7792*	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 7793	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 7794	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 7795*	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 7796*	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 7797*	Multiplication on nonnegative fractions. This definition is similar to df-mq0 7796 but expands Q0. (Contributed by Jim Kingdon, 22-Nov-2019.)
⊢ ·Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨(𝑤 ·o 𝑢), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Theorem	dfplq0qs 7798*	Addition on nonnegative fractions. This definition is similar to df-plq0 7795 but expands Q0. (Contributed by Jim Kingdon, 24-Nov-2019.)
⊢ +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑓) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑓)⟩] ~Q0 ))}
Theorem	enq0enq 7799	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 7800	The equivalence relation for nonnegative fractions is symmetric. Lemma for enq0er 7803. (Contributed by Jim Kingdon, 14-Nov-2019.)
⊢ (𝑓 ~Q0 𝑔 → 𝑔 ~Q0 𝑓)