 Home Intuitionistic Logic ExplorerTheorem List (p. 65 of 100) < 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 - 6401-6500   *Has distinct variable group(s)
TypeLabelDescription
Statement

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremltexpi 6416* 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 6417 Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))

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

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

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

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

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

Definitiondf-plpq 6423* 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 6428) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 6426). (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 6424* 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 6425* 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 6426* 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 6427 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 6428* 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 6429* 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 6430 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 6431* 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 6432* 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 6433* Alternative definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
+pQ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·N 𝑓) +N (𝑣 ·N 𝑢)), (𝑣 ·N 𝑓)⟩))}

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

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

Theoremenqbreq2 6436 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 6437 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 6438 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 6439 The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
~Q ∈ V

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

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

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

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

Theoremltrelnq 6444 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 6445 The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
1QQ

((((𝐴N𝐵N) ∧ (𝐶N𝐷N)) ∧ ((𝐹N𝐺N) ∧ (𝑅N𝑆N))) → (((𝐴 ·N 𝐷) = (𝐵 ·N 𝐶) ∧ (𝐹 ·N 𝑆) = (𝐺 ·N 𝑅)) → ⟨((𝐴 ·N 𝐺) +N (𝐵 ·N 𝐹)), (𝐵 ·N 𝐺)⟩ ~Q ⟨((𝐶 ·N 𝑆) +N (𝐷 ·N 𝑅)), (𝐷 ·N 𝑆)⟩))

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

(((𝐴N𝐵N) ∧ (𝐶N𝐷N)) → ⟨((𝐴 ·N 𝐷) +N (𝐵 ·N 𝐶)), (𝐵 ·N 𝐷)⟩ ∈ (N × N))

Theoremaddpipqqs 6449 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 6450 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 6451 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 6452 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 6453 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 6454 Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) ∈ Q)

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

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

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

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

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

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

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

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

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

Theoremmulcanenq 6464 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 6465 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
((𝐴N𝐵N𝐶N) → [⟨(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)⟩] ~Q = [⟨𝐵, 𝐶⟩] ~Q )

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

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

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

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

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

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

Theoremrecidnq 6472 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 6473 Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
(𝐴Q → (*Q‘(*Q𝐴)) = 𝐴)

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

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

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

Theoremltsonq 6477 '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

Theoremnqtric 6478 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
((𝐴Q𝐵Q) → (𝐴 <Q 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 <Q 𝐴)))

Theoremltanqg 6479 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 𝐵)))

Theoremltmnqg 6480 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 𝐵)))

Theoremltanqi 6481 Ordering property of addition for positive fractions. One direction of ltanqg 6479. (Contributed by Jim Kingdon, 9-Dec-2019.)
((𝐴 <Q 𝐵𝐶Q) → (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵))

Theoremltmnqi 6482 Ordering property of multiplication for positive fractions. One direction of ltmnqg 6480. (Contributed by Jim Kingdon, 9-Dec-2019.)
((𝐴 <Q 𝐵𝐶Q) → (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))

Theoremlt2addnq 6483 Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
(((𝐴Q𝐵Q) ∧ (𝐶Q𝐷Q)) → ((𝐴 <Q 𝐵𝐶 <Q 𝐷) → (𝐴 +Q 𝐶) <Q (𝐵 +Q 𝐷)))

Theoremlt2mulnq 6484 Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.)
(((𝐴Q𝐵Q) ∧ (𝐶Q𝐷Q)) → ((𝐴 <Q 𝐵𝐶 <Q 𝐷) → (𝐴 ·Q 𝐶) <Q (𝐵 ·Q 𝐷)))

Theorem1lt2nq 6485 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)

Theoremltaddnq 6486 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 𝐵))

Theoremltexnqq 6487* 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 𝑥) = 𝐵))

Theoremltexnqi 6488* Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
(𝐴 <Q 𝐵 → ∃𝑥Q (𝐴 +Q 𝑥) = 𝐵)

Theoremhalfnqq 6489* One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)
(𝐴Q → ∃𝑥Q (𝑥 +Q 𝑥) = 𝐴)

Theoremhalfnq 6490* 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 𝑥) = 𝐴)

Theoremnsmallnqq 6491* There is no smallest positive fraction. (Contributed by Jim Kingdon, 24-Sep-2019.)
(𝐴Q → ∃𝑥Q 𝑥 <Q 𝐴)

Theoremnsmallnq 6492* There is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.)
(𝐴Q → ∃𝑥 𝑥 <Q 𝐴)

Theoremsubhalfnqq 6493* 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 6489). (Contributed by Jim Kingdon, 25-Nov-2019.)
(𝐴Q → ∃𝑥Q (𝑥 +Q 𝑥) <Q 𝐴)

Theoremltbtwnnqq 6494* 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 𝐵))

Theoremltbtwnnq 6495* 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 𝐵))

Theoremarchnqq 6496* 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 [⟨𝑥, 1𝑜⟩] ~Q )

Theoremprarloclemarch 6497* A version of the Archimedean property. This variation is "stronger" than archnqq 6496 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 ([⟨𝑥, 1𝑜⟩] ~Q ·Q 𝐵))

Theoremprarloclemarch2 6498* Like prarloclemarch 6497 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 6582. (Contributed by Jim Kingdon, 25-Nov-2019.)
((𝐴Q𝐵Q𝐶Q) → ∃𝑥N (1𝑜 <N 𝑥𝐴 <Q (𝐵 +Q ([⟨𝑥, 1𝑜⟩] ~Q ·Q 𝐶))))

Theoremltrnqg 6499 Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6500. (Contributed by Jim Kingdon, 29-Dec-2019.)
((𝐴Q𝐵Q) → (𝐴 <Q 𝐵 ↔ (*Q𝐵) <Q (*Q𝐴)))

Theoremltrnqi 6500 Ordering property of reciprocal for positive fractions. For the converse, see ltrnqg 6499. (Contributed by Jim Kingdon, 24-Sep-2019.)
(𝐴 <Q 𝐵 → (*Q𝐵) <Q (*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-9995
 Copyright terms: Public domain < Previous  Next >