Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 114) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prarloclem4 7001* | A slight rearrangement of prarloclem3 7000. Lemma for prarloc 7006. (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 7002* | Subtracting two from a positive integer. Lemma for prarloc 7006. (Contributed by Jim Kingdon, 5-Nov-2019.) |
⊢ ((𝑁 ∈ N ∧ 1_{𝑜} <_{N} 𝑁) → ∃𝑥 ∈ ω (2_{𝑜} +_{𝑜} 𝑥) = 𝑁) | ||
Theorem | prarloclem5 7003* | A substitution of zero for 𝑦 and 𝑁 minus two for 𝑥. Lemma for prarloc 7006. (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 7004* | 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 7005 | Some calculations for prarloc 7006. (Contributed by Jim Kingdon, 26-Oct-2019.) |
⊢ (((𝐴 = (𝑋 +_{Q0} ([⟨𝑀, 1_{𝑜}⟩] ~_{Q0} ·_{Q0} 𝑄)) ∧ 𝐵 = (𝑋 +_{Q} ([⟨(𝑀 +_{𝑜} 2_{𝑜}), 1_{𝑜}⟩] ~_{Q} ·_{Q} 𝑄))) ∧ ((𝑄 ∈ Q ∧ (𝑄 +_{Q} 𝑄) <_{Q} 𝑃) ∧ (𝑋 ∈ Q ∧ 𝑀 ∈ ω))) → 𝐵 <_{Q} (𝐴 +_{Q} 𝑃)) | ||
Theorem | prarloc 7006* |
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 7007 instead. (Contributed by Jim Kingdon, 22-Oct-2019.) |
⊢ ((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝑃 ∈ Q) → ∃𝑎 ∈ 𝐿 ∃𝑏 ∈ 𝑈 𝑏 <_{Q} (𝑎 +_{Q} 𝑃)) | ||
Theorem | prarloc2 7007* | A Dedekind cut is arithmetically located. This is a variation of prarloc 7006 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 7008 | Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) |
⊢ <_{P} ⊆ (P × P) | ||
Theorem | ltdfpr 7009* | More convenient form of df-iltp 6973. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<_{P} 𝐵 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2^{nd} ‘𝐴) ∧ 𝑞 ∈ (1^{st} ‘𝐵)))) | ||
Theorem | genpdflem 7010* | Simplification of upper or lower cut expression. Lemma for genpdf 7011. (Contributed by Jim Kingdon, 30-Sep-2019.) |
⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q) ⇒ ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)}) | ||
Theorem | genpdf 7011* | 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 7012* | 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 7013* | 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 7014* | 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 7015* | 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 7016* | 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 7017* | 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 7018* | 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 7019* | 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 7020* | 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 7021* | 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 7022* | 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 7023* | 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 7024* | 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 7025* | 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 7026* | 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 7027* | Associativity of lower cuts. Lemma for genpassg 7029. (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 7028* | Associativity of upper cuts. Lemma for genpassg 7029. (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 7029* | 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 7030 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝐿) ∧ 𝑋 ∈ Q) → (𝑋 <_{Q} 𝑆 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝐿)) | ||
Theorem | addnqprulem 7031 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
⊢ (((⟨𝐿, 𝑈⟩ ∈ P ∧ 𝐺 ∈ 𝑈) ∧ 𝑋 ∈ Q) → (𝑆 <_{Q} 𝑋 → ((𝑋 ·_{Q} (*_{Q}‘𝑆)) ·_{Q} 𝐺) ∈ 𝑈)) | ||
Theorem | addnqprl 7032 | 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 7033 | 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 7034 | Lemma for addlocpr 7039. 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 7035 | Lemma for addlocpr 7039. 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 7036 | Lemma for addlocpr 7039. 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 7037 | Lemma for addlocpr 7039. 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 7038 | Lemma for addlocpr 7039. 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 7039* | 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 7006 to both 𝐴 and 𝐵, and uses nqtri3or 6899 rather than prloc 6994 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 7040 | 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 7041* | 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 7042* | 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 7043 | Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom +_{P} = (P × P) | ||
Theorem | dmmp 7044 | Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) |
⊢ dom ·_{P} = (P × P) | ||
Theorem | nqprm 7045* | A cut produced from a rational is inhabited. Lemma for nqprlu 7050. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∃𝑞 ∈ Q 𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ ∃𝑟 ∈ Q 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprrnd 7046* | A cut produced from a rational is rounded. Lemma for nqprlu 7050. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → (∀𝑞 ∈ Q (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ↔ ∃𝑟 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑟 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴})) ∧ ∀𝑟 ∈ Q (𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ↔ ∃𝑞 ∈ Q (𝑞 <_{Q} 𝑟 ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})))) | ||
Theorem | nqprdisj 7047* | A cut produced from a rational is disjoint. Lemma for nqprlu 7050. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ¬ (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∧ 𝑞 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥})) | ||
Theorem | nqprloc 7048* | A cut produced from a rational is located. Lemma for nqprlu 7050. (Contributed by Jim Kingdon, 8-Dec-2019.) |
⊢ (𝐴 ∈ Q → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <_{Q} 𝑟 → (𝑞 ∈ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∨ 𝑟 ∈ {𝑥 ∣ 𝐴 <_{Q} 𝑥}))) | ||
Theorem | nqprxx 7049* | 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 7050* | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ ∈ P) | ||
Theorem | recnnpr 7051* | 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 7052 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝑥 <_{Q} 𝐴} ∈ V | ||
Theorem | gtnqex 7053 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ {𝑥 ∣ 𝐴 <_{Q} 𝑥} ∈ V | ||
Theorem | nqprl 7054* | 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 7055* | 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 7056* | 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 7057 | The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ 1_{P} ∈ P | ||
Theorem | 1prl 7058 | 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 7059 | 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 7060* | Lemma for addnqpr 7064. 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 7061* | Lemma for addnqpr 7064. 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 7062* | Lemma for addnqpr 7064. 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 7063* | Lemma for addnqpr 7064. 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 7064* | 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 7065* | 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 7064. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (𝐴 ∈ Q → ⟨{𝑙 ∣ 𝑙 <_{Q} (𝐴 +_{Q} 1_{Q})}, {𝑢 ∣ (𝐴 +_{Q} 1_{Q}) <_{Q} 𝑢}⟩ = (⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩ +_{P} 1_{P})) | ||
Theorem | appdivnq 7066* | 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 7067* | Approximate division for positive rationals. This can be thought of as a variation of appdivnq 7066 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 7068 | Calculations for prmuloc 7069. (Contributed by Jim Kingdon, 9-Dec-2019.) |
⊢ (𝜑 → 𝑅 <_{Q} 𝑈) & ⊢ (𝜑 → 𝑈 <_{Q} (𝐷 +_{Q} 𝑃)) & ⊢ (𝜑 → (𝐴 +_{Q} 𝑋) = 𝐵) & ⊢ (𝜑 → (𝑃 ·_{Q} 𝐵) <_{Q} (𝑅 ·_{Q} 𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Q) & ⊢ (𝜑 → 𝐵 ∈ Q) & ⊢ (𝜑 → 𝐷 ∈ Q) & ⊢ (𝜑 → 𝑃 ∈ Q) & ⊢ (𝜑 → 𝑋 ∈ Q) ⇒ ⊢ (𝜑 → (𝑈 ·_{Q} 𝐴) <_{Q} (𝐷 ·_{Q} 𝐵)) | ||
Theorem | prmuloc 7069* | 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 7070* | Positive reals are multiplicatively located. This is a variation of prmuloc 7069 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 7071 | 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 7072 | 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 7073 | Calculations for mullocpr 7074. (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 7074* | 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 7075 | 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 7076* | Lemma for mulnqpr 7080. 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 7077* | Lemma for mulnqpr 7080. 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 7078* | Lemma for mulnqpr 7080. 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 7079* | Lemma for mulnqpr 7080. 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 7080* | 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 7081 | 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 7082 | 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 7083 | 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 7084 | 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 7085 | 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 7086 | 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 7087* | 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 7088* | 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 7089 | 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 7090 | 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 7091 | 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 7092 | 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 7093 | Lemma for 1idpr 7095. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ (𝐴 ∈ P → (1^{st} ‘(𝐴 ·_{P} 1_{P})) = (1^{st} ‘𝐴)) | ||
Theorem | 1idpru 7094 | Lemma for 1idpr 7095. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ (𝐴 ∈ P → (2^{nd} ‘(𝐴 ·_{P} 1_{P})) = (2^{nd} ‘𝐴)) | ||
Theorem | 1idpr 7095 | 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 7096* | 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 7097* | We can order fractions via <_{Q} or <_{P}. (Contributed by Jim Kingdon, 8-Jan-2021.) |
⊢ (𝐴 <_{Q} 𝐵 → ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐴}, {𝑢 ∣ 𝐴 <_{Q} 𝑢}⟩<_{P} ⟨{𝑙 ∣ 𝑙 <_{Q} 𝐵}, {𝑢 ∣ 𝐵 <_{Q} 𝑢}⟩) | ||
Theorem | ltpopr 7098 | 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 7099. (Contributed by Jim Kingdon, 15-Dec-2019.) |
⊢ <_{P} Po P | ||
Theorem | ltsopr 7099 | Positive real 'less than' is a weak linear order (in the sense of df-iso 4098). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.) |
⊢ <_{P} Or P | ||
Theorem | ltaddpr 7100 | 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} 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |