Home | Intuitionistic Logic Explorer Theorem List (p. 67 of 102) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prarloc 6601* |
A Dedekind cut is arithmetically located. Part of Proposition 11.15 of
[BauerTaylor], p. 52, slightly
modified. It states that given a
tolerance 𝑃, there are elements of the lower and
upper cut which
are within that tolerance of each other.
Usually, proofs will be shorter if they use prarloc2 6602 instead. (Contributed by Jim Kingdon, 22-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_{Q} (𝑎 +_{Q} 𝑃)) | ||
Theorem | prarloc2 6602* | A Dedekind cut is arithmetically located. This is a variation of prarloc 6601 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance 𝑃, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 (𝑎 +_{Q} 𝑃) ∈ 𝑈) | ||
Theorem | ltrelpr 6603 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) |
⊢ <_{P} ⊆ (P × P) | ||
Theorem | ltdfpr 6604* | More convenient form of df-iltp 6568. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<_{P} 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd} ‘𝐴) ∧ 𝑞 ∈ (1^{st} ‘𝐵)))) | ||
Theorem | genpdflem 6605* | Simplification of upper or lower cut expression. Lemma for genpdf 6606. (Contributed by Jim Kingdon, 30-Sep-2019.) |
⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q) ⇒ ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)}) | ||
Theorem | genpdf 6606* | Simplified definition of addition or multiplication on positive reals. (Contributed by Jim Kingdon, 30-Sep-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1^{st} ‘𝑤) ∧ 𝑠 ∈ (1^{st} ‘𝑣) ∧ 𝑞 = (𝑟𝐺𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2^{nd} ‘𝑤) ∧ 𝑠 ∈ (2^{nd} ‘𝑣) ∧ 𝑞 = (𝑟𝐺𝑠))}⟩) ⇒ ⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st} ‘𝑤)∃𝑠 ∈ (1^{st} ‘𝑣)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd} ‘𝑤)∃𝑠 ∈ (2^{nd} ‘𝑣)𝑞 = (𝑟𝐺𝑠)}⟩) | ||
Theorem | genipv 6607* | Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^{st} ‘𝐴)∃𝑠 ∈ (1^{st} ‘𝐵)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^{nd} ‘𝐴)∃𝑠 ∈ (2^{nd} ‘𝐵)𝑞 = (𝑟𝐺𝑠)}⟩) | ||
Theorem | genplt2i 6608* | Operating on both sides of two inequalities, when the operation is consistent with <_{Q}. (Contributed by Jim Kingdon, 6-Oct-2019.) |
⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ ((𝐴 <_{Q} 𝐵 ∧ 𝐶 <_{Q} 𝐷) → (𝐴𝐺𝐶) <_{Q} (𝐵𝐺𝐷)) | ||
Theorem | genpelxp 6609* | Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴𝐹𝐵) ∈ (𝒫 Q × 𝒫 Q)) | ||
Theorem | genpelvl 6610* | Membership in lower cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐶 ∈ (1^{st} ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (1^{st} ‘𝐴)∃ℎ ∈ (1^{st} ‘𝐵)𝐶 = (𝑔𝐺ℎ))) | ||
Theorem | genpelvu 6611* | Membership in upper cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 15-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐶 ∈ (2^{nd} ‘(𝐴𝐹𝐵)) ↔ ∃𝑔 ∈ (2^{nd} ‘𝐴)∃ℎ ∈ (2^{nd} ‘𝐵)𝐶 = (𝑔𝐺ℎ))) | ||
Theorem | genpprecll 6612* | Pre-closure law for general operation on lower cuts. (Contributed by Jim Kingdon, 2-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐶 ∈ (1^{st} ‘𝐴) ∧ 𝐷 ∈ (1^{st} ‘𝐵)) → (𝐶𝐺𝐷) ∈ (1^{st} ‘(𝐴𝐹𝐵)))) | ||
Theorem | genppreclu 6613* | Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ((𝐶 ∈ (2^{nd} ‘𝐴) ∧ 𝐷 ∈ (2^{nd} ‘𝐵)) → (𝐶𝐺𝐷) ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) | ||
Theorem | genipdm 6614* | Domain of general operation on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ dom 𝐹 = (P × P) | ||
Theorem | genpml 6615* | The lower cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (1^{st} ‘(𝐴𝐹𝐵))) | ||
Theorem | genpmu 6616* | The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∃𝑞 ∈ Q 𝑞 ∈ (2^{nd} ‘(𝐴𝐹𝐵))) | ||
Theorem | genpcdl 6617* | Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1^{st} ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1^{st} ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <_{Q} (𝑔𝐺ℎ) → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (1^{st} ‘(𝐴𝐹𝐵)) → (𝑥 <_{Q} 𝑓 → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵))))) | ||
Theorem | genpcuu 6618* | Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2^{nd} ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2^{nd} ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔𝐺ℎ) <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝑓 ∈ (2^{nd} ‘(𝐴𝐹𝐵)) → (𝑓 <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵))))) | ||
Theorem | genprndl 6619* | The lower cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) & ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (1^{st} ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (1^{st} ‘𝐵))) ∧ 𝑥 ∈ Q) → (𝑥 <_{Q} (𝑔𝐺ℎ) → 𝑥 ∈ (1^{st} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q (𝑞 ∈ (1^{st} ‘(𝐴𝐹𝐵)) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘(𝐴𝐹𝐵))))) | ||
Theorem | genprndu 6620* | The upper cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) & ⊢ ((((𝐴 ∈ P ∧ 𝑔 ∈ (2^{nd} ‘𝐴)) ∧ (𝐵 ∈ P ∧ ℎ ∈ (2^{nd} ‘𝐵))) ∧ 𝑥 ∈ Q) → ((𝑔𝐺ℎ) <_{Q} 𝑥 → 𝑥 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑟 ∈ Q (𝑟 ∈ (2^{nd} ‘(𝐴𝐹𝐵)) ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘(𝐴𝐹𝐵))))) | ||
Theorem | genpdisj 6621* | The lower and upper cuts produced by addition or multiplication on positive reals are disjoint. (Contributed by Jim Kingdon, 15-Oct-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑥 <_{Q} 𝑦 ↔ (𝑧𝐺𝑥) <_{Q} (𝑧𝐺𝑦))) & ⊢ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) → (𝑥𝐺𝑦) = (𝑦𝐺𝑥)) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^{st} ‘(𝐴𝐹𝐵)) ∧ 𝑞 ∈ (2^{nd} ‘(𝐴𝐹𝐵)))) | ||
Theorem | genpassl 6622* | Associativity of lower cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P × P) & ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^{st} ‘((𝐴𝐹𝐵)𝐹𝐶)) = (1^{st} ‘(𝐴𝐹(𝐵𝐹𝐶)))) | ||
Theorem | genpassu 6623* | Associativity of upper cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P × P) & ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2^{nd} ‘((𝐴𝐹𝐵)𝐹𝐶)) = (2^{nd} ‘(𝐴𝐹(𝐵𝐹𝐶)))) | ||
Theorem | genpassg 6624* | Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (1^{st} ‘𝑤) ∧ 𝑧 ∈ (1^{st} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q ∃𝑧 ∈ Q (𝑦 ∈ (2^{nd} ‘𝑤) ∧ 𝑧 ∈ (2^{nd} ‘𝑣) ∧ 𝑥 = (𝑦𝐺𝑧))}⟩) & ⊢ ((𝑦 ∈ Q ∧ 𝑧 ∈ Q) → (𝑦𝐺𝑧) ∈ Q) & ⊢ dom 𝐹 = (P × P) & ⊢ ((𝑓 ∈ P ∧ 𝑔 ∈ P) → (𝑓𝐹𝑔) ∈ P) & ⊢ ((𝑓 ∈ Q ∧ 𝑔 ∈ Q ∧ ℎ ∈ Q) → ((𝑓𝐺𝑔)𝐺ℎ) = (𝑓𝐺(𝑔𝐺ℎ))) ⇒ ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴𝐹𝐵)𝐹𝐶) = (𝐴𝐹(𝐵𝐹𝐶))) | ||
Theorem | addnqprllem 6625 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} 𝑆 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝐿)) | ||
Theorem | addnqprulem 6626 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <_{Q} 𝑋 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝑈)) | ||
Theorem | addnqprl 6627 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) |
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1^{st} ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1^{st} ‘𝐵))) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} (𝐺 +_{Q} 𝐻) → 𝑋 ∈ (1^{st} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addnqpru 6628 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) |
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2^{nd} ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (2^{nd} ‘𝐵))) ∧ 𝑋 ∈ Q) → ((𝐺 +_{Q} 𝐻) <_{Q} 𝑋 → 𝑋 ∈ (2^{nd} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addlocprlemlt 6629 | Lemma for addlocpr 6634. The 𝑄 <_{Q} (𝐷 +_{Q} 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <_{Q} 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +_{Q} (𝑃 +_{Q} 𝑃)) = 𝑅) & ⊢ (𝜑 → 𝐷 ∈ (1^{st} ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2^{nd} ‘𝐴)) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1^{st} ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2^{nd} ‘𝐵)) & ⊢ (𝜑 → 𝑇 <_{Q} (𝐸 +_{Q} 𝑃)) ⇒ ⊢ (𝜑 → (𝑄 <_{Q} (𝐷 +_{Q} 𝐸) → 𝑄 ∈ (1^{st} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addlocprlemeqgt 6630 | Lemma for addlocpr 6634. This is a step used in both the 𝑄 = (𝐷 +_{Q} 𝐸) and (𝐷 +_{Q} 𝐸) <_{Q} 𝑄 cases. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <_{Q} 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +_{Q} (𝑃 +_{Q} 𝑃)) = 𝑅) & ⊢ (𝜑 → 𝐷 ∈ (1^{st} ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2^{nd} ‘𝐴)) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1^{st} ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2^{nd} ‘𝐵)) & ⊢ (𝜑 → 𝑇 <_{Q} (𝐸 +_{Q} 𝑃)) ⇒ ⊢ (𝜑 → (𝑈 +_{Q} 𝑇) <_{Q} ((𝐷 +_{Q} 𝐸) +_{Q} (𝑃 +_{Q} 𝑃))) | ||
Theorem | addlocprlemeq 6631 | Lemma for addlocpr 6634. The 𝑄 = (𝐷 +_{Q} 𝐸) case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <_{Q} 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +_{Q} (𝑃 +_{Q} 𝑃)) = 𝑅) & ⊢ (𝜑 → 𝐷 ∈ (1^{st} ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2^{nd} ‘𝐴)) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1^{st} ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2^{nd} ‘𝐵)) & ⊢ (𝜑 → 𝑇 <_{Q} (𝐸 +_{Q} 𝑃)) ⇒ ⊢ (𝜑 → (𝑄 = (𝐷 +_{Q} 𝐸) → 𝑅 ∈ (2^{nd} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addlocprlemgt 6632 | Lemma for addlocpr 6634. The (𝐷 +_{Q} 𝐸) <_{Q} 𝑄 case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <_{Q} 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +_{Q} (𝑃 +_{Q} 𝑃)) = 𝑅) & ⊢ (𝜑 → 𝐷 ∈ (1^{st} ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2^{nd} ‘𝐴)) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1^{st} ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2^{nd} ‘𝐵)) & ⊢ (𝜑 → 𝑇 <_{Q} (𝐸 +_{Q} 𝑃)) ⇒ ⊢ (𝜑 → ((𝐷 +_{Q} 𝐸) <_{Q} 𝑄 → 𝑅 ∈ (2^{nd} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addlocprlem 6633 | Lemma for addlocpr 6634. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ P) & ⊢ (𝜑 → 𝐵 ∈ P) & ⊢ (𝜑 → 𝑄 <_{Q} 𝑅) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → (𝑄 +_{Q} (𝑃 +_{Q} 𝑃)) = 𝑅) & ⊢ (𝜑 → 𝐷 ∈ (1^{st} ‘𝐴)) & ⊢ (𝜑 → 𝑈 ∈ (2^{nd} ‘𝐴)) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → 𝐸 ∈ (1^{st} ‘𝐵)) & ⊢ (𝜑 → 𝑇 ∈ (2^{nd} ‘𝐵)) & ⊢ (𝜑 → 𝑇 <_{Q} (𝐸 +_{Q} 𝑃)) ⇒ ⊢ (𝜑 → (𝑄 ∈ (1^{st} ‘(𝐴 +_{P} 𝐵)) ∨ 𝑅 ∈ (2^{nd} ‘(𝐴 +_{P} 𝐵)))) | ||
Theorem | addlocpr 6634* | Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6601 to both 𝐴 and 𝐵, and uses nqtri3or 6494 rather than prloc 6589 to decide whether 𝑞 is too big to be in the lower cut of 𝐴 +_{P} 𝐵 (and deduce that if it is, then 𝑟 must be in the upper cut). What the two proofs have in common is that they take the difference between 𝑞 and 𝑟 to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ (1^{st} ‘(𝐴 +_{P} 𝐵)) ∨ 𝑟 ∈ (2^{nd} ‘(𝐴 +_{P} 𝐵))))) | ||
Theorem | addclpr 6635 | Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +_{P} 𝐵) ∈ P) | ||
Theorem | plpvlu 6636* | Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +_{P} 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦 +_{Q} 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦 +_{Q} 𝑧)}⟩) | ||
Theorem | mpvlu 6637* | Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_{P} 𝐵) = ⟨{𝑥 ∈ Q ∣ ∃𝑦 ∈ (1^{st} ‘𝐴)∃𝑧 ∈ (1^{st} ‘𝐵)𝑥 = (𝑦 ·_{Q} 𝑧)}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ (2^{nd} ‘𝐴)∃𝑧 ∈ (2^{nd} ‘𝐵)𝑥 = (𝑦 ·_{Q} 𝑧)}⟩) | ||
Theorem | dmplp 6638 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom +_{P} = (P × P) | ||
Theorem | dmmp 6639 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom ·_{P} = (P × P) | ||
Theorem | nqprm 6640* | A cut produced from a rational is inhabited. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprrnd 6641* | A cut produced from a rational is rounded. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})))) | ||
Theorem | nqprdisj 6642* | A cut produced from a rational is disjoint. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprloc 6643* | A cut produced from a rational is located. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥}))) | ||
Theorem | nqprxx 6644* | The canonical embedding of the rationals into the reals, expressed with the same variable for the lower and upper cuts. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ⟨{𝑥 ∣ 𝑥 <_{Q} 𝐴}, {𝑥 ∣ 𝐴 <_{Q} 𝑥}⟩ ∈ P) | ||
Theorem | nqprlu 6645* | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | recnnpr 6646* | The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.) |
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝐴, 1_{𝑜}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝐴, 1_{𝑜}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | ltnqex 6647 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∈ V | ||
Theorem | gtnqex 6648 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ∈ V | ||
Theorem | nqprl 6649* | Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by <_{P}. (Contributed by Jim Kingdon, 8-Jul-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) → (𝐴 ∈ (1^{st} ‘𝐵) ↔ ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P} 𝐵)) | ||
Theorem | nqpru 6650* | Comparing a fraction to a real can be done by whether it is an element of the upper cut, or by <_{P}. (Contributed by Jim Kingdon, 29-Nov-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ P) → (𝐴 ∈ (2^{nd} ‘𝐵) ↔ 𝐵<_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩)) | ||
Theorem | nnprlu 6651* | The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐴, 1_{𝑜}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐴, 1_{𝑜}⟩] ~_{Q} <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | 1pr 6652 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ 1_{P} ∈ P | ||
Theorem | 1prl 6653 | The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ (1^{st} ‘1_{P}) = {𝑥 ∣ 𝑥 <_{Q} 1_{Q}} | ||
Theorem | 1pru 6654 | The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ (2^{nd} ‘1_{P}) = {𝑥 ∣ 1_{Q} <_{Q} 𝑥} | ||
Theorem | addnqprlemrl 6655* | Lemma for addnqpr 6659. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆ (1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵) <_{Q} 𝑢}⟩)) | ||
Theorem | addnqprlemru 6656* | Lemma for addnqpr 6659. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆ (2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵) <_{Q} 𝑢}⟩)) | ||
Theorem | addnqprlemfl 6657* | Lemma for addnqpr 6659. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵) <_{Q} 𝑢}⟩) ⊆ (1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) | ||
Theorem | addnqprlemfu 6658* | Lemma for addnqpr 6659. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵) <_{Q} 𝑢}⟩) ⊆ (2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) | ||
Theorem | addnqpr 6659* | Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 𝐵)}, {𝑢 ∣ (𝐴 +_{Q} 𝐵) <_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) | ||
Theorem | addnqpr1 6660* | Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6659. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 1_{Q})}, {𝑢 ∣ (𝐴 +_{Q} 1_{Q}) <_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} 1_{P})) | ||
Theorem | appdivnq 6661* | Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where 𝐴 and 𝐵 are positive, as well as 𝐶). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ ((𝐴 <_{Q} 𝐵 ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝐴 <_{Q} (𝑚 ·_{Q} 𝐶) ∧ (𝑚 ·_{Q} 𝐶) <_{Q} 𝐵)) | ||
Theorem | appdiv0nq 6662* | Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6661 in which 𝐴 is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.) |
⊢ ((𝐵 ∈ Q ∧ 𝐶 ∈ Q) → ∃𝑚 ∈ Q (𝑚 ·_{Q} 𝐶) <_{Q} 𝐵) | ||
Theorem | prmuloclemcalc 6663 | Calculations for prmuloc 6664. (Contributed by Jim Kingdon, 9-Dec-2019.) |
⊢ (𝜑 → 𝑅 <_{Q} 𝑈) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → (𝐴 +_{Q} 𝑋) = 𝐵) & ⊢ (𝜑 → (𝑃 ·_{Q} 𝐵) <_{Q} (𝑅 ·_{Q} 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Q) & ⊢ (𝜑 → 𝐵 ∈ Q) & ⊢ (𝜑 → 𝐷 ∈ Q) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → 𝑋 ∈ Q) ⇒ ⊢ (𝜑 → (𝑈 ·_{Q} 𝐴) <_{Q} (𝐷 ·_{Q} 𝐵)) | ||
Theorem | prmuloc 6664* | Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <_{Q} 𝐵) → ∃𝑑 ∈ Q ∃𝑢 ∈ Q (𝑑 ∈ 𝐿 ∧ 𝑢 ∈ 𝑈 ∧ (𝑢 ·_{Q} 𝐴) <_{Q} (𝑑 ·_{Q} 𝐵))) | ||
Theorem | prmuloc2 6665* | Positive reals are multiplicatively located. This is a variation of prmuloc 6664 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio 𝐵, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 1_{Q} <_{Q} 𝐵) → ∃𝑥 ∈ 𝐿 (𝑥 ·_{Q} 𝐵) ∈ 𝑈) | ||
Theorem | mulnqprl 6666 | Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) |
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (1^{st} ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1^{st} ‘𝐵))) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} (𝐺 ·_{Q} 𝐻) → 𝑋 ∈ (1^{st} ‘(𝐴 ·_{P} 𝐵)))) | ||
Theorem | mulnqpru 6667 | Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) |
⊢ ((((𝐴 ∈ P ∧ 𝐺 ∈ (2^{nd} ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (2^{nd} ‘𝐵))) ∧ 𝑋 ∈ Q) → ((𝐺 ·_{Q} 𝐻) <_{Q} 𝑋 → 𝑋 ∈ (2^{nd} ‘(𝐴 ·_{P} 𝐵)))) | ||
Theorem | mullocprlem 6668 | Calculations for mullocpr 6669. (Contributed by Jim Kingdon, 10-Dec-2019.) |
⊢ (𝜑 → (𝐴 ∈ P ∧ 𝐵 ∈ P)) & ⊢ (𝜑 → (𝑈 ·_{Q} 𝑄) <_{Q} (𝐸 ·_{Q} (𝐷 ·_{Q} 𝑈))) & ⊢ (𝜑 → (𝐸 ·_{Q} (𝐷 ·_{Q} 𝑈)) <_{Q} (𝑇 ·_{Q} (𝐷 ·_{Q} 𝑈))) & ⊢ (𝜑 → (𝑇 ·_{Q} (𝐷 ·_{Q} 𝑈)) <_{Q} (𝐷 ·_{Q} 𝑅)) & ⊢ (𝜑 → (𝑄 ∈ Q ∧ 𝑅 ∈ Q)) & ⊢ (𝜑 → (𝐷 ∈ Q ∧ 𝑈 ∈ Q)) & ⊢ (𝜑 → (𝐷 ∈ (1^{st} ‘𝐴) ∧ 𝑈 ∈ (2^{nd} ‘𝐴))) & ⊢ (𝜑 → (𝐸 ∈ Q ∧ 𝑇 ∈ Q)) ⇒ ⊢ (𝜑 → (𝑄 ∈ (1^{st} ‘(𝐴 ·_{P} 𝐵)) ∨ 𝑅 ∈ (2^{nd} ‘(𝐴 ·_{P} 𝐵)))) | ||
Theorem | mullocpr 6669* | Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both 𝐴 and 𝐵 are positive, not just 𝐴). (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ (1^{st} ‘(𝐴 ·_{P} 𝐵)) ∨ 𝑟 ∈ (2^{nd} ‘(𝐴 ·_{P} 𝐵))))) | ||
Theorem | mulclpr 6670 | Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_{P} 𝐵) ∈ P) | ||
Theorem | mulnqprlemrl 6671* | Lemma for mulnqpr 6675. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆ (1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 ·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵) <_{Q} 𝑢}⟩)) | ||
Theorem | mulnqprlemru 6672* | Lemma for mulnqpr 6675. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) ⊆ (2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 ·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵) <_{Q} 𝑢}⟩)) | ||
Theorem | mulnqprlemfl 6673* | Lemma for mulnqpr 6675. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (1^{st} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 ·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵) <_{Q} 𝑢}⟩) ⊆ (1^{st} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) | ||
Theorem | mulnqprlemfu 6674* | Lemma for mulnqpr 6675. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (2^{nd} ‘⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 ·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵) <_{Q} 𝑢}⟩) ⊆ (2^{nd} ‘(⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩))) | ||
Theorem | mulnqpr 6675* | Multiplication of fractions embedded into positive reals. One can either multiply the fractions as fractions, or embed them into positive reals and multiply them as positive reals, and get the same result. (Contributed by Jim Kingdon, 18-Jul-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → ⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 ·_{Q} 𝐵)}, {𝑢 ∣ (𝐴 ·_{Q} 𝐵) <_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ·_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) | ||
Theorem | addcomprg 6676 | Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 +_{P} 𝐵) = (𝐵 +_{P} 𝐴)) | ||
Theorem | addassprg 6677 | Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +_{P} 𝐵) +_{P} 𝐶) = (𝐴 +_{P} (𝐵 +_{P} 𝐶))) | ||
Theorem | mulcomprg 6678 | Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 ·_{P} 𝐵) = (𝐵 ·_{P} 𝐴)) | ||
Theorem | mulassprg 6679 | Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 ·_{P} 𝐵) ·_{P} 𝐶) = (𝐴 ·_{P} (𝐵 ·_{P} 𝐶))) | ||
Theorem | distrlem1prl 6680 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^{st} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶))) ⊆ (1^{st} ‘((𝐴 ·_{P} 𝐵) +_{P} (𝐴 ·_{P} 𝐶)))) | ||
Theorem | distrlem1pru 6681 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2^{nd} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶))) ⊆ (2^{nd} ‘((𝐴 ·_{P} 𝐵) +_{P} (𝐴 ·_{P} 𝐶)))) | ||
Theorem | distrlem4prl 6682* | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ (1^{st} ‘𝐴) ∧ 𝑦 ∈ (1^{st} ‘𝐵)) ∧ (𝑓 ∈ (1^{st} ‘𝐴) ∧ 𝑧 ∈ (1^{st} ‘𝐶)))) → ((𝑥 ·_{Q} 𝑦) +_{Q} (𝑓 ·_{Q} 𝑧)) ∈ (1^{st} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶)))) | ||
Theorem | distrlem4pru 6683* | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ ((𝑥 ∈ (2^{nd} ‘𝐴) ∧ 𝑦 ∈ (2^{nd} ‘𝐵)) ∧ (𝑓 ∈ (2^{nd} ‘𝐴) ∧ 𝑧 ∈ (2^{nd} ‘𝐶)))) → ((𝑥 ·_{Q} 𝑦) +_{Q} (𝑓 ·_{Q} 𝑧)) ∈ (2^{nd} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶)))) | ||
Theorem | distrlem5prl 6684 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (1^{st} ‘((𝐴 ·_{P} 𝐵) +_{P} (𝐴 ·_{P} 𝐶))) ⊆ (1^{st} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶)))) | ||
Theorem | distrlem5pru 6685 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (2^{nd} ‘((𝐴 ·_{P} 𝐵) +_{P} (𝐴 ·_{P} 𝐶))) ⊆ (2^{nd} ‘(𝐴 ·_{P} (𝐵 +_{P} 𝐶)))) | ||
Theorem | distrprg 6686 | Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴 ·_{P} (𝐵 +_{P} 𝐶)) = ((𝐴 ·_{P} 𝐵) +_{P} (𝐴 ·_{P} 𝐶))) | ||
Theorem | ltprordil 6687 | If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.) |
⊢ (𝐴<_{P} 𝐵 → (1^{st} ‘𝐴) ⊆ (1^{st} ‘𝐵)) | ||
Theorem | 1idprl 6688 | Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ (𝐴 ∈ P → (1^{st} ‘(𝐴 ·_{P} 1_{P})) = (1^{st} ‘𝐴)) | ||
Theorem | 1idpru 6689 | Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ (𝐴 ∈ P → (2^{nd} ‘(𝐴 ·_{P} 1_{P})) = (2^{nd} ‘𝐴)) | ||
Theorem | 1idpr 6690 | 1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.) |
⊢ (𝐴 ∈ P → (𝐴 ·_{P} 1_{P}) = 𝐴) | ||
Theorem | ltnqpr 6691* | We can order fractions via <_{Q} or <_{P}. (Contributed by Jim Kingdon, 19-Jun-2021.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <_{Q} 𝐵 ↔ ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩)) | ||
Theorem | ltnqpri 6692* | We can order fractions via <_{Q} or <_{P}. (Contributed by Jim Kingdon, 8-Jan-2021.) |
⊢ (𝐴 <_{Q} 𝐵 → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩) | ||
Theorem | ltpopr 6693 | Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6694. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ <_{P} Po P | ||
Theorem | ltsopr 6694 | Positive real 'less than' is a weak linear order (in the sense of df-iso 4034). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.) |
⊢ <_{P} Or P | ||
Theorem | ltaddpr 6695 | The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → 𝐴<_{P} (𝐴 +_{P} 𝐵)) | ||
Theorem | ltexprlemell 6696* | Element in lower cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st} ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (2^{nd} ‘𝐵))}⟩ ⇒ ⊢ (𝑞 ∈ (1^{st} ‘𝐶) ↔ (𝑞 ∈ Q ∧ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑞) ∈ (1^{st} ‘𝐵)))) | ||
Theorem | ltexprlemelu 6697* | Element in upper cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st} ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (2^{nd} ‘𝐵))}⟩ ⇒ ⊢ (𝑟 ∈ (2^{nd} ‘𝐶) ↔ (𝑟 ∈ Q ∧ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑟) ∈ (2^{nd} ‘𝐵)))) | ||
Theorem | ltexprlemm 6698* | Our constructed difference is inhabited. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st} ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (2^{nd} ‘𝐵))}⟩ ⇒ ⊢ (𝐴<_{P} 𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1^{st} ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^{nd} ‘𝐶))) | ||
Theorem | ltexprlemopl 6699* | The lower cut of our constructed difference is open. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st} ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (2^{nd} ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1^{st} ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶))) | ||
Theorem | ltexprlemlol 6700* | The lower cut of our constructed difference is lower. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2^{nd} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (1^{st} ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1^{st} ‘𝐴) ∧ (𝑦 +_{Q} 𝑥) ∈ (2^{nd} ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<_{P} 𝐵 ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐶)) → 𝑞 ∈ (1^{st} ‘𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |