 Home Intuitionistic Logic ExplorerTheorem List (p. 69 of 114) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 6801-6900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Syntaxc0r 6801 The signed real constant 0.
class 0R

Syntaxc1r 6802 The signed real constant 1.
class 1R

Syntaxcm1r 6803 The signed real constant -1.
class -1R

Syntaxcplr 6804 Signed real addition.
class +R

Syntaxcmr 6805 Signed real multiplication.
class ·R

Syntaxcltr 6806 Signed real ordering relation.
class <R

Definitiondf-ni 6807 Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.)
N = (ω ∖ {∅})

Definitiondf-pli 6808 Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
+N = ( +𝑜 ↾ (N × N))

Definitiondf-mi 6809 Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
·N = ( ·𝑜 ↾ (N × N))

Definitiondf-lti 6810 Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.)
<N = ( E ∩ (N × N))

Theoremelni 6811 Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.)
(𝐴N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))

Theorempinn 6812 A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
(𝐴N𝐴 ∈ ω)

Theorempion 6813 A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.)
(𝐴N𝐴 ∈ On)

Theorempiord 6814 A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
(𝐴N → Ord 𝐴)

Theoremniex 6815 The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)
N ∈ V

Theorem0npi 6816 The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)
¬ ∅ ∈ N

Theoremelni2 6817 Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
(𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))

Theorem1pi 6818 Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
1𝑜N

Theoremaddpiord 6819 Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.)
((𝐴N𝐵N) → (𝐴 +N 𝐵) = (𝐴 +𝑜 𝐵))

Theoremmulpiord 6820 Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)
((𝐴N𝐵N) → (𝐴 ·N 𝐵) = (𝐴 ·𝑜 𝐵))

Theoremmulidpi 6821 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.)
(𝐴N → (𝐴 ·N 1𝑜) = 𝐴)

Theoremltpiord 6822 Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))

Theoremltsopi 6823 Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
<N Or N

Theorempitric 6824 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 <N 𝐴)))

Theorempitri3or 6825 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴 = 𝐵𝐵 <N 𝐴))

Theoremltdcpi 6826 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((𝐴N𝐵N) → DECID 𝐴 <N 𝐵)

Theoremltrelpi 6827 Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)
<N ⊆ (N × N)

Theoremdmaddpi 6828 Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)
dom +N = (N × N)

Theoremdmmulpi 6829 Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)
dom ·N = (N × N)

Theoremaddclpi 6830 Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.)
((𝐴N𝐵N) → (𝐴 +N 𝐵) ∈ N)

Theoremmulclpi 6831 Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
((𝐴N𝐵N) → (𝐴 ·N 𝐵) ∈ N)

Theoremaddcompig 6832 Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((𝐴N𝐵N) → (𝐴 +N 𝐵) = (𝐵 +N 𝐴))

Theoremaddasspig 6833 Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((𝐴N𝐵N𝐶N) → ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶)))

Theoremmulcompig 6834 Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((𝐴N𝐵N) → (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴))

Theoremmulasspig 6835 Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
((𝐴N𝐵N𝐶N) → ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶)))

Theoremdistrpig 6836 Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)
((𝐴N𝐵N𝐶N) → (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)))

Theoremaddcanpig 6837 Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)
((𝐴N𝐵N𝐶N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))

Theoremmulcanpig 6838 Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)
((𝐴N𝐵N𝐶N) → ((𝐴 ·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶))

Theoremaddnidpig 6839 There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.)
((𝐴N𝐵N) → ¬ (𝐴 +N 𝐵) = 𝐴)

Theoremltexpi 6840* 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 𝑥) = 𝐵))

Theoremltapig 6841 Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))

Theoremltmpig 6842 Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵)))

Theorem1lt2pi 6843 One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
1𝑜 <N (1𝑜 +N 1𝑜)

Theoremnlt1pig 6844 No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
(𝐴N → ¬ 𝐴 <N 1𝑜)

Theoremindpi 6845* Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
(𝑥 = 1𝑜 → (𝜑𝜓))    &   (𝑥 = 𝑦 → (𝜑𝜒))    &   (𝑥 = (𝑦 +N 1𝑜) → (𝜑𝜃))    &   (𝑥 = 𝐴 → (𝜑𝜏))    &   𝜓    &   (𝑦N → (𝜒𝜃))       (𝐴N𝜏)

Theoremnnppipi 6846 A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
((𝐴 ∈ ω ∧ 𝐵N) → (𝐴 +𝑜 𝐵) ∈ N)

Definitiondf-plpq 6847* 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 6852) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 6850). (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𝑦))⟩)

Definitiondf-mpq 6848* 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𝑦))⟩)

Definitiondf-ltpq 6849* 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𝑥)))}

Definitiondf-enq 6850* 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 𝑣)))}

Definitiondf-nqqs 6851 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 )

Definitiondf-plqqs 6852* 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 ))}

Definitiondf-mqqs 6853* 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 ))}

Definitiondf-1nqqs 6854 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 = [⟨1𝑜, 1𝑜⟩] ~Q

Definitiondf-rq 6855* 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)}

Definitiondf-ltnqqs 6856* 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 𝑣)))}

Theoremdfplpq2 6857* Alternate definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
+pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·N 𝑓) +N (𝑣 ·N 𝑢)), (𝑣 ·N 𝑓)⟩))}

Theoremdfmpq2 6858* Alternate definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
·pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 ·N 𝑢), (𝑣 ·N 𝑓)⟩))}

Theoremenqbreq 6859 Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.)
(((𝐴N𝐵N) ∧ (𝐶N𝐷N)) → (⟨𝐴, 𝐵⟩ ~Q𝐶, 𝐷⟩ ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶)))

Theoremenqbreq2 6860 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𝐴))))

Theoremenqer 6861 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)

Theoremenqeceq 6862 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 𝐶)))

Theoremenqex 6863 The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
~Q ∈ V

Theoremenqdc 6864 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(((𝐴N𝐵N) ∧ (𝐶N𝐷N)) → DECID𝐴, 𝐵⟩ ~Q𝐶, 𝐷⟩)

Theoremenqdc1 6865 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(((𝐴N𝐵N) ∧ 𝐶 ∈ (N × N)) → DECID𝐴, 𝐵⟩ ~Q 𝐶)

Theoremnqex 6866 The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
Q ∈ V

Theorem0nnq 6867 The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
¬ ∅ ∈ Q

Theoremltrelnq 6868 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)

Theorem1nq 6869 The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
1QQ

Theoremaddcmpblnq 6870 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 𝑆)⟩))

Theoremmulcmpblnq 6871 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 𝑆)⟩))

Theoremaddpipqqslem 6872 Lemma for addpipqqs 6873. (Contributed by Jim Kingdon, 11-Sep-2019.)
(((𝐴N𝐵N) ∧ (𝐶N𝐷N)) → ⟨((𝐴 ·N 𝐷) +N (𝐵 ·N 𝐶)), (𝐵 ·N 𝐷)⟩ ∈ (N × N))

Theoremaddpipqqs 6873 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 )

Theoremmulpipq2 6874 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𝐵))⟩)

Theoremmulpipq 6875 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 𝐷)⟩)

Theoremmulpipqqs 6876 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 )

Theoremordpipqqs 6877 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 𝐶)))

Theoremaddclnq 6878 Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)

Theoremmulclnq 6879 Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
((𝐴Q𝐵Q) → (𝐴 ·Q 𝐵) ∈ Q)

Theoremdmaddpqlem 6880* Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 6882. (Contributed by Jim Kingdon, 15-Sep-2019.)
(𝑥Q → ∃𝑤𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q )

Theoremnqpi 6881* Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 6880 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
(𝐴Q → ∃𝑤𝑣((𝑤N𝑣N) ∧ 𝐴 = [⟨𝑤, 𝑣⟩] ~Q ))

Theoremdmaddpq 6882 Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
dom +Q = (Q × Q)

Theoremdmmulpq 6883 Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
dom ·Q = (Q × Q)

Theoremaddcomnqg 6884 Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴))

Theoremaddassnqg 6885 Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
((𝐴Q𝐵Q𝐶Q) → ((𝐴 +Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q 𝐶)))

Theoremmulcomnqg 6886 Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
((𝐴Q𝐵Q) → (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴))

Theoremmulassnqg 6887 Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
((𝐴Q𝐵Q𝐶Q) → ((𝐴 ·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵 ·Q 𝐶)))

Theoremmulcanenq 6888 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𝐵, 𝐶⟩)

Theoremmulcanenqec 6889 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
((𝐴N𝐵N𝐶N) → [⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩] ~Q = [⟨𝐵, 𝐶⟩] ~Q )

Theoremdistrnqg 6890 Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
((𝐴Q𝐵Q𝐶Q) → (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)))

Theorem1qec 6891 The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
(𝐴N → 1Q = [⟨𝐴, 𝐴⟩] ~Q )

Theoremmulidnq 6892 Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
(𝐴Q → (𝐴 ·Q 1Q) = 𝐴)

Theoremrecexnq 6893* Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
(𝐴Q → ∃𝑦(𝑦Q ∧ (𝐴 ·Q 𝑦) = 1Q))

Theoremrecmulnqg 6894 Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
((𝐴Q𝐵Q) → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Theoremrecclnq 6895 Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
(𝐴Q → (*Q𝐴) ∈ Q)

Theoremrecidnq 6896 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)

Theoremrecrecnq 6897 Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
(𝐴Q → (*Q‘(*Q𝐴)) = 𝐴)

Theoremrec1nq 6898 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
(*Q‘1Q) = 1Q

Theoremnqtri3or 6899 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
((𝐴Q𝐵Q) → (𝐴 <Q 𝐵𝐴 = 𝐵𝐵 <Q 𝐴))

Theoremltdcnq 6900 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
((𝐴Q𝐵Q) → DECID 𝐴 <Q 𝐵)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11363
 Copyright terms: Public domain < Previous  Next >