Home | Intuitionistic Logic Explorer Theorem List (p. 74 of 135) | < 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 | ||
Definition | df-iltp 7301* |
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 7302 | Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ P ⊆ (𝒫 Q × 𝒫 Q) | ||
Theorem | preqlu 7303 | 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 7304 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) |
⊢ P ∈ V | ||
Theorem | elinp 7305* | 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 7306 | 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 7307* | 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 7308* | A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝐿) | ||
Theorem | prmu 7309* | A positive real's upper cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.) |
⊢ (⟨𝐿, 𝑈⟩ ∈ P → ∃𝑥 ∈ Q 𝑥 ∈ 𝑈) | ||
Theorem | prssnql 7310 | 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 7311 | 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 7312 | An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → 𝐵 ∈ Q) | ||
Theorem | elprnqu 7313 | An element of a positive real's upper cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → 𝐵 ∈ Q) | ||
Theorem | 0npr 7314 | The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) |
⊢ ¬ ∅ ∈ P | ||
Theorem | prcdnql 7315 | A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → (𝐶 <_{Q} 𝐵 → 𝐶 ∈ 𝐿)) | ||
Theorem | prcunqu 7316 | An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐶 ∈ 𝑈) → (𝐶 <_{Q} 𝐵 → 𝐵 ∈ 𝑈)) | ||
Theorem | prubl 7317 | A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) ∧ 𝐶 ∈ Q) → (¬ 𝐶 ∈ 𝐿 → 𝐵 <_{Q} 𝐶)) | ||
Theorem | prltlu 7318 | 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 7319* | A lower cut has no largest member. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ 𝐿 𝐵 <_{Q} 𝑥) | ||
Theorem | prnminu 7320* | An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝑈) → ∃𝑥 ∈ 𝑈 𝑥 <_{Q} 𝐵) | ||
Theorem | prnmaddl 7321* | A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐵 ∈ 𝐿) → ∃𝑥 ∈ Q (𝐵 +_{Q} 𝑥) ∈ 𝐿) | ||
Theorem | prloc 7322 | A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 <_{Q} 𝐵) → (𝐴 ∈ 𝐿 ∨ 𝐵 ∈ 𝑈)) | ||
Theorem | prdisj 7323 | A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ Q) → ¬ (𝐴 ∈ 𝐿 ∧ 𝐴 ∈ 𝑈)) | ||
Theorem | prarloclemlt 7324 | Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → (𝐴 +_{Q} ([⟨(𝑦 +_{o} 1_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) <_{Q} (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃))) | ||
Theorem | prarloclemlo 7325* | Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +_{Q} ([⟨(𝑦 +_{o} 1_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝐿 → (((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} suc 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)))) | ||
Theorem | prarloclemup 7326 | Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ 𝑦 ∈ ω) → ((𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈 → (((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} suc 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)))) | ||
Theorem | prarloclem3step 7327* | Induction step for prarloclem3 7328. (Contributed by Jim Kingdon, 9-Nov-2019.) |
⊢ (((𝑋 ∈ ω ∧ (⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿 ∧ 𝑃 ∈ Q)) ∧ ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} suc 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) → ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem3 7328* | Contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 27-Oct-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑋 ∈ ω ∧ 𝑃 ∈ Q) ∧ ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑋), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{o} 2_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem4 7329* | A slight rearrangement of prarloclem3 7328. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 4-Nov-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ 𝑃 ∈ Q) → (∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑥), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{o} 2_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈))) | ||
Theorem | prarloclemn 7330* | Subtracting two from a positive integer. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 5-Nov-2019.) |
⊢ ((𝑁 ∈ N ∧ 1_{o} <_{N} 𝑁) → ∃𝑥 ∈ ω (2_{o} +_{o} 𝑥) = 𝑁) | ||
Theorem | prarloclem5 7331* | A substitution of zero for 𝑦 and 𝑁 minus two for 𝑥. Lemma for prarloc 7334. (Contributed by Jim Kingdon, 4-Nov-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐴 ∈ 𝐿) ∧ (𝑁 ∈ N ∧ 𝑃 ∈ Q ∧ 1_{o} <_{N} 𝑁) ∧ (𝐴 +_{Q} ([⟨𝑁, 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑥 ∈ ω ∃𝑦 ∈ ω ((𝐴 +_{Q0} ([⟨𝑦, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨((𝑦 +_{o} 2_{o}) +_{o} 𝑥), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclem 7332* | 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_{o} <_{N} 𝑁) ∧ (𝐴 +_{Q} ([⟨𝑁, 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈) → ∃𝑗 ∈ ω ((𝐴 +_{Q0} ([⟨𝑗, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑃)) ∈ 𝐿 ∧ (𝐴 +_{Q} ([⟨(𝑗 +_{o} 2_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑃)) ∈ 𝑈)) | ||
Theorem | prarloclemcalc 7333 | Some calculations for prarloc 7334. (Contributed by Jim Kingdon, 26-Oct-2019.) |
⊢ (((𝐴 = (𝑋 +_{Q0} ([⟨𝑀, 1_{o}⟩] ~_{Q0} ·_{Q0} 𝑄)) ∧ 𝐵 = (𝑋 +_{Q} ([⟨(𝑀 +_{o} 2_{o}), 1_{o}⟩] ~_{Q} ·_{Q} 𝑄))) ∧ ((𝑄 ∈ Q ∧ (𝑄 +_{Q} 𝑄) <_{Q} 𝑃) ∧ (𝑋 ∈ Q ∧ 𝑀 ∈ ω))) → 𝐵 <_{Q} (𝐴 +_{Q} 𝑃)) | ||
Theorem | prarloc 7334* |
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 7335 instead. (Contributed by Jim Kingdon, 22-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_{Q} (𝑎 +_{Q} 𝑃)) | ||
Theorem | prarloc2 7335* | A Dedekind cut is arithmetically located. This is a variation of prarloc 7334 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 7336 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) |
⊢ <_{P} ⊆ (P × P) | ||
Theorem | ltdfpr 7337* | More convenient form of df-iltp 7301. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<_{P} 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd} ‘𝐴) ∧ 𝑞 ∈ (1^{st} ‘𝐵)))) | ||
Theorem | genpdflem 7338* | Simplification of upper or lower cut expression. Lemma for genpdf 7339. (Contributed by Jim Kingdon, 30-Sep-2019.) |
⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q) ⇒ ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)}) | ||
Theorem | genpdf 7339* | 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 7340* | 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 7341* | 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 7342* | 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 7343* | 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 7344* | 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 7345* | 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 7346* | 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 7347* | 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 7348* | 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 7349* | 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 7350* | 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 7351* | 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 7352* | 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 7353* | 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 7354* | 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 7355* | Associativity of lower cuts. Lemma for genpassg 7357. (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 7356* | Associativity of upper cuts. Lemma for genpassg 7357. (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 7357* | 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 7358 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} 𝑆 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝐿)) | ||
Theorem | addnqprulem 7359 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <_{Q} 𝑋 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝑈)) | ||
Theorem | addnqprl 7360 | 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 7361 | 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 7362 | Lemma for addlocpr 7367. 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 7363 | Lemma for addlocpr 7367. 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 7364 | Lemma for addlocpr 7367. 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 7365 | Lemma for addlocpr 7367. 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 7366 | Lemma for addlocpr 7367. 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 7367* | 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 7334 to both 𝐴 and 𝐵, and uses nqtri3or 7227 rather than prloc 7322 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 7368 | 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 7369* | 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 7370* | 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 7371 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom +_{P} = (P × P) | ||
Theorem | dmmp 7372 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom ·_{P} = (P × P) | ||
Theorem | nqprm 7373* | A cut produced from a rational is inhabited. Lemma for nqprlu 7378. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprrnd 7374* | A cut produced from a rational is rounded. Lemma for nqprlu 7378. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})))) | ||
Theorem | nqprdisj 7375* | A cut produced from a rational is disjoint. Lemma for nqprlu 7378. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprloc 7376* | A cut produced from a rational is located. Lemma for nqprlu 7378. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥}))) | ||
Theorem | nqprxx 7377* | 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 7378* | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | recnnpr 7379* | The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.) |
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝐴, 1_{o}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝐴, 1_{o}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | ltnqex 7380 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∈ V | ||
Theorem | gtnqex 7381 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ∈ V | ||
Theorem | nqprl 7382* | 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 7383* | 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 7384* | The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
⊢ (𝐴 ∈ N → ⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐴, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐴, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | 1pr 7385 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ 1_{P} ∈ P | ||
Theorem | 1prl 7386 | 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 7387 | 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 7388* | Lemma for addnqpr 7392. 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 7389* | Lemma for addnqpr 7392. 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 7390* | Lemma for addnqpr 7392. 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 7391* | Lemma for addnqpr 7392. 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 7392* | 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 7393* | 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 7392. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 1_{Q})}, {𝑢 ∣ (𝐴 +_{Q} 1_{Q}) <_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} 1_{P})) | ||
Theorem | appdivnq 7394* | 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 7395* | Approximate division for positive rationals. This can be thought of as a variation of appdivnq 7394 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 7396 | Calculations for prmuloc 7397. (Contributed by Jim Kingdon, 9-Dec-2019.) |
⊢ (𝜑 → 𝑅 <_{Q} 𝑈) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → (𝐴 +_{Q} 𝑋) = 𝐵) & ⊢ (𝜑 → (𝑃 ·_{Q} 𝐵) <_{Q} (𝑅 ·_{Q} 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Q) & ⊢ (𝜑 → 𝐵 ∈ Q) & ⊢ (𝜑 → 𝐷 ∈ Q) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → 𝑋 ∈ Q) ⇒ ⊢ (𝜑 → (𝑈 ·_{Q} 𝐴) <_{Q} (𝐷 ·_{Q} 𝐵)) | ||
Theorem | prmuloc 7397* | 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 7398* | Positive reals are multiplicatively located. This is a variation of prmuloc 7397 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 7399 | 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 7400 | 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} 𝐵)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |