Home | Intuitionistic Logic Explorer Theorem List (p. 68 of 110) | < 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 | mulcomnq0 6701 | Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.) |
⊢ ((𝐴 ∈ Q_{0} ∧ 𝐵 ∈ Q_{0}) → (𝐴 ·_{Q0} 𝐵) = (𝐵 ·_{Q0} 𝐴)) | ||
Theorem | addassnq0lemcl 6702 | A natural number closure law. Lemma for addassnq0 6703. (Contributed by Jim Kingdon, 3-Dec-2019.) |
⊢ (((𝐼 ∈ ω ∧ 𝐽 ∈ N) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ N)) → (((𝐼 ·_{𝑜} 𝐿) +_{𝑜} (𝐽 ·_{𝑜} 𝐾)) ∈ ω ∧ (𝐽 ·_{𝑜} 𝐿) ∈ N)) | ||
Theorem | addassnq0 6703 | Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.) |
⊢ ((𝐴 ∈ Q_{0} ∧ 𝐵 ∈ Q_{0} ∧ 𝐶 ∈ Q_{0}) → ((𝐴 +_{Q0} 𝐵) +_{Q0} 𝐶) = (𝐴 +_{Q0} (𝐵 +_{Q0} 𝐶))) | ||
Theorem | distnq0r 6704 | Multiplication of non-negative fractions is distributive. Version of distrnq0 6700 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.) |
⊢ ((𝐴 ∈ Q_{0} ∧ 𝐵 ∈ Q_{0} ∧ 𝐶 ∈ Q_{0}) → ((𝐵 +_{Q0} 𝐶) ·_{Q0} 𝐴) = ((𝐵 ·_{Q0} 𝐴) +_{Q0} (𝐶 ·_{Q0} 𝐴))) | ||
Theorem | addpinq1 6705 | Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ N → [⟨(𝐴 +_{N} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} = ([⟨𝐴, 1_{𝑜}⟩] ~_{Q} +_{Q} 1_{Q})) | ||
Theorem | nq02m 6706 | Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.) |
⊢ (𝐴 ∈ Q_{0} → ([⟨2_{𝑜}, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝐴) = (𝐴 +_{Q0} 𝐴)) | ||
Definition | df-inp 6707* |
Define the set of positive reals. A "Dedekind cut" is a partition of
the positive rational numbers into two classes such that all the numbers
of one class are less than all the numbers of the other.
Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers. A Dedekind cut is an ordered pair of a lower set 𝑙 and an upper set 𝑢 which is inhabited (∃𝑞 ∈ Q𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q𝑟 ∈ 𝑢), rounded (∀𝑞 ∈ Q(𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q(𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ 𝑙)) and likewise for 𝑢), disjoint (∀𝑞 ∈ Q¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)) and located (∀𝑞 ∈ Q∀𝑟 ∈ Q(𝑞 <_{Q} 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts. (Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.) |
⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))} | ||
Definition | df-i1p 6708* | Define the positive real constant 1. 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, 25-Sep-2019.) |
⊢ 1_{P} = ⟨{𝑙 ∣ 𝑙 <_{Q} 1_{Q}}, {𝑢 ∣ 1_{Q} <_{Q} 𝑢}⟩ | ||
Definition | df-iplp 6709* |
Define addition on positive reals. From Section 11.2.1 of [HoTT], p.
(varies). We write this definition to closely resemble the definition
in HoTT although some of the conditions are redundant (for example,
𝑟
∈ (1^{st} ‘𝑥) implies 𝑟 ∈ Q)
and can be simplified as
shown at genpdf 6749.
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, 26-Sep-2019.) |
⊢ +_{P} = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1^{st} ‘𝑥) ∧ 𝑠 ∈ (1^{st} ‘𝑦) ∧ 𝑞 = (𝑟 +_{Q} 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2^{nd} ‘𝑥) ∧ 𝑠 ∈ (2^{nd} ‘𝑦) ∧ 𝑞 = (𝑟 +_{Q} 𝑠))}⟩) | ||
Definition | df-imp 6710* |
Define multiplication on positive reals. Here we use a simple
definition which is similar to df-iplp 6709 or the definition of
multiplication on positive reals in Metamath Proof Explorer. This is as
opposed to the more complicated definition of multiplication given in
Section 11.2.1 of [HoTT], p. (varies),
which appears to be motivated by
handling negative numbers or handling modified Dedekind cuts in which
locatedness is omitted.
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, 29-Sep-2019.) |
⊢ ·_{P} = (𝑥 ∈ P, 𝑦 ∈ P ↦ ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (1^{st} ‘𝑥) ∧ 𝑠 ∈ (1^{st} ‘𝑦) ∧ 𝑞 = (𝑟 ·_{Q} 𝑠))}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ (2^{nd} ‘𝑥) ∧ 𝑠 ∈ (2^{nd} ‘𝑦) ∧ 𝑞 = (𝑟 ·_{Q} 𝑠))}⟩) | ||
Definition | df-iltp 6711* |
Define ordering on positive reals. We define 𝑥<_{P}
𝑦 if there is a
positive fraction 𝑞 which is an element of the upper cut
of 𝑥
and the lower cut of 𝑦. From the definition of < in
Section 11.2.1
of [HoTT], p. (varies).
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, 29-Sep-2019.) |
⊢ <_{P} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd} ‘𝑥) ∧ 𝑞 ∈ (1^{st} ‘𝑦)))} | ||
Theorem | npsspw 6712 | Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ P ⊆ (𝒫 Q × 𝒫 Q) | ||
Theorem | preqlu 6713 | Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴 = 𝐵 ↔ ((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd} ‘𝐴) = (2^{nd} ‘𝐵)))) | ||
Theorem | npex 6714 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) |
⊢ P ∈ V | ||
Theorem | elinp 6715* | Membership in positive reals. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P ↔ (((𝐿 ⊆ Q ∧ 𝑈 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝐿 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑈)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝐿 ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ 𝐿)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑈 ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ 𝑈))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝐿 ∧ 𝑞 ∈ 𝑈) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ 𝐿 ∨ 𝑟 ∈ 𝑈))))) | ||
Theorem | prop 6716 | A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (𝐴 ∈ P → ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ P) | ||
Theorem | elnp1st2nd 6717* | Membership in positive reals, using 1^{st} and 2^{nd} to refer to the lower and upper cut. (Contributed by Jim Kingdon, 3-Oct-2019.) |
⊢ (𝐴 ∈ P ↔ ((𝐴 ∈ (𝒫 Q × 𝒫 Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ (1^{st} ‘𝐴) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2^{nd} ‘𝐴))) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ (1^{st} ‘𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ (1^{st} ‘𝐴))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2^{nd} ‘𝐴) ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ (2^{nd} ‘𝐴)))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1^{st} ‘𝐴) ∧ 𝑞 ∈ (2^{nd} ‘𝐴)) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ (1^{st} ‘𝐴) ∨ 𝑟 ∈ (2^{nd} ‘𝐴)))))) | ||
Theorem | prml 6718* | A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝐿) | ||
Theorem | prmu 6719* | A positive real's upper cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝑈) | ||
Theorem | prssnql 6720 | The lower cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → 𝐿 ⊆ Q) | ||
Theorem | prssnqu 6721 | The upper cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → 𝑈 ⊆ Q) | ||
Theorem | elprnql 6722 | An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q) | ||
Theorem | elprnqu 6723 | An element of a positive real's upper cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → 𝐵 ∈ Q) | ||
Theorem | 0npr 6724 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) |
⊢ ¬ ∅ ∈ P | ||
Theorem | prcdnql 6725 | A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <_{Q} 𝐵 → 𝐶 ∈ 𝐿)) | ||
Theorem | prcunqu 6726 | An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <_{Q} 𝐵 → 𝐵 ∈ 𝑈)) | ||
Theorem | prubl 6727 | A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 ∈ Q) → (¬ 𝐶 ∈ 𝐿 → 𝐵 <_{Q} 𝐶)) | ||
Theorem | prltlu 6728 | An element of a lower cut is less than an element of the corresponding upper cut. (Contributed by Jim Kingdon, 15-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿 ∧ 𝐶 ∈ 𝑈) → 𝐵 <_{Q} 𝐶) | ||
Theorem | prnmaxl 6729* | A lower cut has no largest member. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝐵 <_{Q} 𝑥) | ||
Theorem | prnminu 6730* | An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 𝑥 <_{Q} 𝐵) | ||
Theorem | prnmaddl 6731* | A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ Q (𝐵 +_{Q} 𝑥) ∈ 𝐿) | ||
Theorem | prloc 6732 | A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <_{Q} 𝐵) → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)) | ||
Theorem | prdisj 6733 | A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ Q) → ¬ (𝐴 ∈ 𝐿 ∧ 𝐴 ∈ 𝑈)) | ||
Theorem | prarloclemlt 6734 | Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +_{Q} ([⟨(𝑦 +_{𝑜} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) <_{Q} (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃))) | ||
Theorem | prarloclemlo 6735* | Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +_{Q} ([⟨(𝑦 +_{𝑜} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝐿 → (((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} suc 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)))) | ||
Theorem | prarloclemup 6736 | Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈 → (((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} suc 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)))) | ||
Theorem | prarloclem3step 6737* | Induction step for prarloclem3 6738. (Contributed by Jim Kingdon, 9-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} suc 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem3 6738* | Contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 27-Oct-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑋 ∈ ω ∧ 𝑃 ∈ Q) ∧ ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑋), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{𝑜} 2_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem4 6739* | A slight rearrangement of prarloclem3 6738. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 4-Nov-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ 𝑃 ∈ Q) → (∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑥), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{𝑜} 2_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈))) | ||
Theorem | prarloclemn 6740* | Subtracting two from a positive integer. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 5-Nov-2019.) |
⊢ ((𝑁 ∈ N ∧ 1_{𝑜} <_{N} 𝑁) → ∃𝑥 ∈ ω (2_{𝑜} +_{𝑜} 𝑥) = 𝑁) | ||
Theorem | prarloclem5 6741* | A substitution of zero for 𝑦 and 𝑁 minus two for 𝑥. Lemma for prarloc 6744. (Contributed by Jim Kingdon, 4-Nov-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1_{𝑜} <_{N} 𝑁) ∧ (𝐴 +_{Q} ([⟨𝑁, 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{𝑜} 2_{𝑜}) +_{𝑜} 𝑥), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem 6742* | A special case of Lemma 6.16 from [BauerTaylor], p. 32. Given evenly spaced rational numbers from 𝐴 to 𝐴 +_{Q} (𝑁 ·_{Q} 𝑃) (which are in the lower and upper cuts, respectively, of a real number), there are a pair of numbers, two positions apart in the even spacing, which straddle the cut. (Contributed by Jim Kingdon, 22-Oct-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1_{𝑜} <_{N} 𝑁) ∧ (𝐴 +_{Q} ([⟨𝑁, 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{𝑜} 2_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclemcalc 6743 | Some calculations for prarloc 6744. (Contributed by Jim Kingdon, 26-Oct-2019.) |
⊢ (((𝐴 = (𝑋 +_{Q0} ([⟨𝑀, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑄)) ∧ 𝐵 = (𝑋 +_{Q} ([⟨(𝑀 +_{𝑜} 2_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑄))) ∧ ((𝑄 ∈ Q ∧ (𝑄 +_{Q} 𝑄) <_{Q} 𝑃) ∧ (𝑋 ∈ Q ∧ 𝑀 ∈ ω))) → 𝐵 <_{Q} (𝐴 +_{Q} 𝑃)) | ||
Theorem | prarloc 6744* |
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 6745 instead. (Contributed by Jim Kingdon, 22-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_{Q} (𝑎 +_{Q} 𝑃)) | ||
Theorem | prarloc2 6745* | A Dedekind cut is arithmetically located. This is a variation of prarloc 6744 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 6746 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) |
⊢ <_{P} ⊆ (P × P) | ||
Theorem | ltdfpr 6747* | More convenient form of df-iltp 6711. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<_{P} 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd} ‘𝐴) ∧ 𝑞 ∈ (1^{st} ‘𝐵)))) | ||
Theorem | genpdflem 6748* | Simplification of upper or lower cut expression. Lemma for genpdf 6749. (Contributed by Jim Kingdon, 30-Sep-2019.) |
⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q) ⇒ ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)}) | ||
Theorem | genpdf 6749* | 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 6750* | 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 6751* | 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 6752* | 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 6753* | 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 6754* | 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 6755* | 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 6756* | 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 6757* | 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 6758* | 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 6759* | 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 6760* | 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 6761* | 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 6762* | 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 6763* | 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 6764* | 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 6765* | Associativity of lower cuts. Lemma for genpassg 6767. (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 6766* | Associativity of upper cuts. Lemma for genpassg 6767. (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 6767* | 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 6768 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} 𝑆 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝐿)) | ||
Theorem | addnqprulem 6769 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <_{Q} 𝑋 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝑈)) | ||
Theorem | addnqprl 6770 | 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 6771 | 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 6772 | Lemma for addlocpr 6777. 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 6773 | Lemma for addlocpr 6777. 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 6774 | Lemma for addlocpr 6777. 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 6775 | Lemma for addlocpr 6777. 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 6776 | Lemma for addlocpr 6777. 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 6777* | 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 6744 to both 𝐴 and 𝐵, and uses nqtri3or 6637 rather than prloc 6732 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 6778 | 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 6779* | 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 6780* | 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 6781 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom +_{P} = (P × P) | ||
Theorem | dmmp 6782 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom ·_{P} = (P × P) | ||
Theorem | nqprm 6783* | A cut produced from a rational is inhabited. Lemma for nqprlu 6788. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprrnd 6784* | A cut produced from a rational is rounded. Lemma for nqprlu 6788. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})))) | ||
Theorem | nqprdisj 6785* | A cut produced from a rational is disjoint. Lemma for nqprlu 6788. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprloc 6786* | A cut produced from a rational is located. Lemma for nqprlu 6788. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥}))) | ||
Theorem | nqprxx 6787* | 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 6788* | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | recnnpr 6789* | 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 6790 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∈ V | ||
Theorem | gtnqex 6791 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ∈ V | ||
Theorem | nqprl 6792* | 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 6793* | 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 6794* | 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 6795 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ 1_{P} ∈ P | ||
Theorem | 1prl 6796 | 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 6797 | 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 6798* | Lemma for addnqpr 6802. 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 6799* | Lemma for addnqpr 6802. 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 6800* | Lemma for addnqpr 6802. 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} 𝑢}⟩))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |