![]() |
Intuitionistic Logic Explorer Theorem List (p. 77 of 150) | < 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 | ltexprlemm 7601* | Our constructed difference is inhabited. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐶) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemopl 7602* | The lower cut of our constructed difference is open. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐶)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) | ||
Theorem | ltexprlemlol 7603* | The lower cut of our constructed difference is lower. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶)) → 𝑞 ∈ (1st ‘𝐶))) | ||
Theorem | ltexprlemopu 7604* | The upper cut of our constructed difference is open. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemupu 7605* | The upper cut of our constructed difference is upper. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemrnd 7606* | Our constructed difference is rounded. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐶) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐶))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐶) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))))) | ||
Theorem | ltexprlemdisj 7607* | Our constructed difference is disjoint. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemloc 7608* | Our constructed difference is located. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))) | ||
Theorem | ltexprlempr 7609* | Our constructed difference is a positive real. Lemma for ltexpri 7614. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → 𝐶 ∈ P) | ||
Theorem | ltexprlemfl 7610* | Lemma for ltexpri 7614. One direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (1st ‘(𝐴 +P 𝐶)) ⊆ (1st ‘𝐵)) | ||
Theorem | ltexprlemrl 7611* | Lemma for ltexpri 7614. Reverse direction of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (1st ‘𝐵) ⊆ (1st ‘(𝐴 +P 𝐶))) | ||
Theorem | ltexprlemfu 7612* | Lemma for ltexpri 7614. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (2nd ‘(𝐴 +P 𝐶)) ⊆ (2nd ‘𝐵)) | ||
Theorem | ltexprlemru 7613* | Lemma for ltexpri 7614. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = ⟨{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}⟩ ⇒ ⊢ (𝐴<P 𝐵 → (2nd ‘𝐵) ⊆ (2nd ‘(𝐴 +P 𝐶))) | ||
Theorem | ltexpri 7614* | Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
⊢ (𝐴<P 𝐵 → ∃𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵) | ||
Theorem | addcanprleml 7615 | Lemma for addcanprg 7617. (Contributed by Jim Kingdon, 25-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st ‘𝐵) ⊆ (1st ‘𝐶)) | ||
Theorem | addcanprlemu 7616 | Lemma for addcanprg 7617. (Contributed by Jim Kingdon, 25-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (2nd ‘𝐵) ⊆ (2nd ‘𝐶)) | ||
Theorem | addcanprg 7617 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐴 +P 𝐵) = (𝐴 +P 𝐶) → 𝐵 = 𝐶)) | ||
Theorem | lteupri 7618* | The difference from ltexpri 7614 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
⊢ (𝐴<P 𝐵 → ∃!𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵) | ||
Theorem | ltaprlem 7619 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) |
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))) | ||
Theorem | ltaprg 7620 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → (𝐴<P 𝐵 ↔ (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))) | ||
Theorem | prplnqu 7621* | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) |
⊢ (𝜑 → 𝑋 ∈ P) & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝐴 ∈ (2nd ‘(𝑋 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ (2nd ‘𝑋)(𝑦 +Q 𝑄) = 𝐴) | ||
Theorem | addextpr 7622 | Strong extensionality of addition (ordering version). This is similar to addext 8569 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ((𝐴 +P 𝐵)<P (𝐶 +P 𝐷) → (𝐴<P 𝐶 ∨ 𝐵<P 𝐷))) | ||
Theorem | recexprlemell 7623* | Membership in the lower cut of 𝐵. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐶 ∈ (1st ‘𝐵) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))) | ||
Theorem | recexprlemelu 7624* | Membership in the upper cut of 𝐵. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐶 ∈ (2nd ‘𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))) | ||
Theorem | recexprlemm 7625* | 𝐵 is inhabited. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐵) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemopl 7626* | The lower cut of 𝐵 is open. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐵)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵))) | ||
Theorem | recexprlemlol 7627* | The lower cut of 𝐵 is lower. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵)) → 𝑞 ∈ (1st ‘𝐵))) | ||
Theorem | recexprlemopu 7628* | The upper cut of 𝐵 is open. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐵)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemupu 7629* | The upper cut of 𝐵 is upper. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)) → 𝑟 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemrnd 7630* | 𝐵 is rounded. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (∀𝑞 ∈ Q (𝑞 ∈ (1st ‘𝐵) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))))) | ||
Theorem | recexprlemdisj 7631* | 𝐵 is disjoint. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐵) ∧ 𝑞 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemloc 7632* | 𝐵 is located. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐵) ∨ 𝑟 ∈ (2nd ‘𝐵)))) | ||
Theorem | recexprlempr 7633* | 𝐵 is a positive real. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → 𝐵 ∈ P) | ||
Theorem | recexprlem1ssl 7634* | The lower cut of one is a subset of the lower cut of 𝐴 ·P 𝐵. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵))) | ||
Theorem | recexprlem1ssu 7635* | The upper cut of one is a subset of the upper cut of 𝐴 ·P 𝐵. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵))) | ||
Theorem | recexprlemss1l 7636* | The lower cut of 𝐴 ·P 𝐵 is a subset of the lower cut of one. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (1st ‘(𝐴 ·P 𝐵)) ⊆ (1st ‘1P)) | ||
Theorem | recexprlemss1u 7637* | The upper cut of 𝐴 ·P 𝐵 is a subset of the upper cut of one. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (2nd ‘(𝐴 ·P 𝐵)) ⊆ (2nd ‘1P)) | ||
Theorem | recexprlemex 7638* | 𝐵 is the reciprocal of 𝐴. Lemma for recexpr 7639. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩ ⇒ ⊢ (𝐴 ∈ P → (𝐴 ·P 𝐵) = 1P) | ||
Theorem | recexpr 7639* | The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) |
⊢ (𝐴 ∈ P → ∃𝑥 ∈ P (𝐴 ·P 𝑥) = 1P) | ||
Theorem | aptiprleml 7640 | Lemma for aptipr 7642. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (1st ‘𝐴) ⊆ (1st ‘𝐵)) | ||
Theorem | aptiprlemu 7641 | Lemma for aptipr 7642. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (2nd ‘𝐵) ⊆ (2nd ‘𝐴)) | ||
Theorem | aptipr 7642 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ (𝐴<P 𝐵 ∨ 𝐵<P 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | ltmprr 7643 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐶 ·P 𝐴)<P (𝐶 ·P 𝐵) → 𝐴<P 𝐵)) | ||
Theorem | archpr 7644* | For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer 𝑥 is embedded into the reals as described at nnprlu 7554. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝐴 ∈ P → ∃𝑥 ∈ N 𝐴<P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩] ~Q <Q 𝑢}⟩) | ||
Theorem | caucvgprlemcanl 7645* | Lemma for cauappcvgprlemladdrl 7658. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
⊢ (𝜑 → 𝐿 ∈ P) & ⊢ (𝜑 → 𝑆 ∈ Q) & ⊢ (𝜑 → 𝑅 ∈ Q) & ⊢ (𝜑 → 𝑄 ∈ Q) ⇒ ⊢ (𝜑 → ((𝑅 +Q 𝑄) ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q 𝑄)}, {𝑢 ∣ (𝑆 +Q 𝑄) <Q 𝑢}⟩)) ↔ 𝑅 ∈ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)))) | ||
Theorem | cauappcvgprlemm 7646* | Lemma for cauappcvgpr 7663. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿))) | ||
Theorem | cauappcvgprlemopl 7647* | Lemma for cauappcvgpr 7663. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 ∈ (1st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) | ||
Theorem | cauappcvgprlemlol 7648* | Lemma for cauappcvgpr 7663. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) | ||
Theorem | cauappcvgprlemopu 7649* | Lemma for cauappcvgpr 7663. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑟 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
Theorem | cauappcvgprlemupu 7650* | Lemma for cauappcvgpr 7663. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿)) → 𝑟 ∈ (2nd ‘𝐿)) | ||
Theorem | cauappcvgprlemrnd 7651* | Lemma for cauappcvgpr 7663. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → (∀𝑠 ∈ Q (𝑠 ∈ (1st ‘𝐿) ↔ ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐿) ↔ ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))))) | ||
Theorem | cauappcvgprlemdisj 7652* | Lemma for cauappcvgpr 7663. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
Theorem | cauappcvgprlemloc 7653* | Lemma for cauappcvgpr 7663. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑟 ∈ Q (𝑠 <Q 𝑟 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑟 ∈ (2nd ‘𝐿)))) | ||
Theorem | cauappcvgprlemcl 7654* | Lemma for cauappcvgpr 7663. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → 𝐿 ∈ P) | ||
Theorem | cauappcvgprlemladdfu 7655* | Lemma for cauappcvgprlemladd 7659. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ⊆ (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩)) | ||
Theorem | cauappcvgprlemladdfl 7656* | Lemma for cauappcvgprlemladd 7659. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ⊆ (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩)) | ||
Theorem | cauappcvgprlemladdru 7657* | Lemma for cauappcvgprlemladd 7659. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (2nd ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩) ⊆ (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) | ||
Theorem | cauappcvgprlemladdrl 7658* | Lemma for cauappcvgprlemladd 7659. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (1st ‘⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩) ⊆ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) | ||
Theorem | cauappcvgprlemladd 7659* | Lemma for cauappcvgpr 7663. This takes 𝐿 and offsets it by the positive fraction 𝑆. (Contributed by Jim Kingdon, 23-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩) = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q ((𝐹‘𝑞) +Q 𝑆)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q (((𝐹‘𝑞) +Q 𝑞) +Q 𝑆) <Q 𝑢}⟩) | ||
Theorem | cauappcvgprlem1 7660* | Lemma for cauappcvgpr 7663. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝑅 ∈ Q) ⇒ ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑄)}, {𝑢 ∣ (𝐹‘𝑄) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑄 +Q 𝑅)}, {𝑢 ∣ (𝑄 +Q 𝑅) <Q 𝑢}⟩)) | ||
Theorem | cauappcvgprlem2 7661* | Lemma for cauappcvgpr 7663. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝑅 ∈ Q) ⇒ ⊢ (𝜑 → 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑄) +Q (𝑄 +Q 𝑅))}, {𝑢 ∣ ((𝐹‘𝑄) +Q (𝑄 +Q 𝑅)) <Q 𝑢}⟩) | ||
Theorem | cauappcvgprlemlim 7662* | Lemma for cauappcvgpr 7663. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑞 ∈ Q (𝑙 +Q 𝑞) <Q (𝐹‘𝑞)}, {𝑢 ∈ Q ∣ ∃𝑞 ∈ Q ((𝐹‘𝑞) +Q 𝑞) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩)) | ||
Theorem | cauappcvgpr 7663* |
A Cauchy approximation has a limit. A Cauchy approximation, here
𝐹, is similar to a Cauchy sequence but
is indexed by the desired
tolerance (that is, how close together terms needs to be) rather than
by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p.
(varies) with a few differences such as that we are proving the
existence of a limit without anything about how fast it converges
(that is, mere existence instead of existence, in HoTT terms), and
that the codomain of 𝐹 is Q rather than P. We also
specify that every term needs to be larger than a fraction 𝐴, to
avoid the case where we have positive terms which "converge"
to zero
(which is not a positive real).
This proof (including its lemmas) is similar to the proofs of caucvgpr 7683 and caucvgprpr 7713 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
⊢ (𝜑 → 𝐹:Q⟶Q) & ⊢ (𝜑 → ∀𝑝 ∈ Q ∀𝑞 ∈ Q ((𝐹‘𝑝) <Q ((𝐹‘𝑞) +Q (𝑝 +Q 𝑞)) ∧ (𝐹‘𝑞) <Q ((𝐹‘𝑝) +Q (𝑝 +Q 𝑞)))) & ⊢ (𝜑 → ∀𝑝 ∈ Q 𝐴 <Q (𝐹‘𝑝)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ P ∀𝑞 ∈ Q ∀𝑟 ∈ Q (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑞)}, {𝑢 ∣ (𝐹‘𝑞) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙 ∣ 𝑙 <Q (𝑞 +Q 𝑟)}, {𝑢 ∣ (𝑞 +Q 𝑟) <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟))}, {𝑢 ∣ ((𝐹‘𝑞) +Q (𝑞 +Q 𝑟)) <Q 𝑢}⟩)) | ||
Theorem | archrecnq 7664* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝐴 ∈ Q → ∃𝑗 ∈ N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴) | ||
Theorem | archrecpr 7665* | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
⊢ (𝐴 ∈ P → ∃𝑗 ∈ N ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑗, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝐴) | ||
Theorem | caucvgprlemk 7666 | Lemma for caucvgpr 7683. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
⊢ (𝜑 → 𝐽 <N 𝐾) & ⊢ (𝜑 → (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄) ⇒ ⊢ (𝜑 → (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q 𝑄) | ||
Theorem | caucvgprlemnkj 7667* | Lemma for caucvgpr 7683. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → 𝐾 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → ¬ ((𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q 𝑆)) | ||
Theorem | caucvgprlemnbj 7668* | Lemma for caucvgpr 7683. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → 𝐵 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) ⇒ ⊢ (𝜑 → ¬ (((𝐹‘𝐵) +Q (*Q‘[⟨𝐵, 1o⟩] ~Q )) +Q (*Q‘[⟨𝐽, 1o⟩] ~Q )) <Q (𝐹‘𝐽)) | ||
Theorem | caucvgprlemm 7669* | Lemma for caucvgpr 7683. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐿))) | ||
Theorem | caucvgprlemopl 7670* | Lemma for caucvgpr 7683. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 ∈ (1st ‘𝐿)) → ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) | ||
Theorem | caucvgprlemlol 7671* | Lemma for caucvgpr 7683. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) | ||
Theorem | caucvgprlemopu 7672* | Lemma for caucvgpr 7683. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑟 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
Theorem | caucvgprlemupu 7673* | Lemma for caucvgpr 7683. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿)) → 𝑟 ∈ (2nd ‘𝐿)) | ||
Theorem | caucvgprlemrnd 7674* | Lemma for caucvgpr 7683. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → (∀𝑠 ∈ Q (𝑠 ∈ (1st ‘𝐿) ↔ ∃𝑟 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐿))) ∧ ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐿) ↔ ∃𝑠 ∈ Q (𝑠 <Q 𝑟 ∧ 𝑠 ∈ (2nd ‘𝐿))))) | ||
Theorem | caucvgprlemdisj 7675* | Lemma for caucvgpr 7683. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑠 ∈ Q ¬ (𝑠 ∈ (1st ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) | ||
Theorem | caucvgprlemloc 7676* | Lemma for caucvgpr 7683. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑠 ∈ Q ∀𝑟 ∈ Q (𝑠 <Q 𝑟 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑟 ∈ (2nd ‘𝐿)))) | ||
Theorem | caucvgprlemcl 7677* | Lemma for caucvgpr 7683. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → 𝐿 ∈ P) | ||
Theorem | caucvgprlemladdfu 7678* | Lemma for caucvgpr 7683. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → (2nd ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩)) ⊆ {𝑢 ∈ Q ∣ ∃𝑗 ∈ N (((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) +Q 𝑆) <Q 𝑢}) | ||
Theorem | caucvgprlemladdrl 7679* | Lemma for caucvgpr 7683. Adding 𝑆 after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → {𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q ((𝐹‘𝑗) +Q 𝑆)} ⊆ (1st ‘(𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑆}, {𝑢 ∣ 𝑆 <Q 𝑢}⟩))) | ||
Theorem | caucvgprlem1 7680* | Lemma for caucvgpr 7683. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝐽 <N 𝐾) & ⊢ (𝜑 → (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄) ⇒ ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝐾)}, {𝑢 ∣ (𝐹‘𝐾) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑄}, {𝑢 ∣ 𝑄 <Q 𝑢}⟩)) | ||
Theorem | caucvgprlem2 7681* | Lemma for caucvgpr 7683. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ & ⊢ (𝜑 → 𝑄 ∈ Q) & ⊢ (𝜑 → 𝐽 <N 𝐾) & ⊢ (𝜑 → (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑄) ⇒ ⊢ (𝜑 → 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝐾) +Q 𝑄)}, {𝑢 ∣ ((𝐹‘𝐾) +Q 𝑄) <Q 𝑢}⟩) | ||
Theorem | caucvgprlemlim 7682* | Lemma for caucvgpr 7683. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑗 ∈ N (𝑙 +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q (𝐹‘𝑗)}, {𝑢 ∈ Q ∣ ∃𝑗 ∈ N ((𝐹‘𝑗) +Q (*Q‘[⟨𝑗, 1o⟩] ~Q )) <Q 𝑢}⟩ ⇒ ⊢ (𝜑 → ∀𝑥 ∈ Q ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}⟩<P (𝐿 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}⟩) ∧ 𝐿<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q 𝑢}⟩))) | ||
Theorem | caucvgpr 7683* |
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
1 / 𝑛 of the nth term (it should later be
able to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a fraction 𝐴, to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This proof (including its lemmas) is similar to the proofs of cauappcvgpr 7663 and caucvgprpr 7713. Reading cauappcvgpr 7663 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
⊢ (𝜑 → 𝐹:N⟶Q) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <Q ((𝐹‘𝑘) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q )) ∧ (𝐹‘𝑘) <Q ((𝐹‘𝑛) +Q (*Q‘[⟨𝑛, 1o⟩] ~Q ))))) & ⊢ (𝜑 → ∀𝑗 ∈ N 𝐴 <Q (𝐹‘𝑗)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ P ∀𝑥 ∈ Q ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → (⟨{𝑙 ∣ 𝑙 <Q (𝐹‘𝑘)}, {𝑢 ∣ (𝐹‘𝑘) <Q 𝑢}⟩<P (𝑦 +P ⟨{𝑙 ∣ 𝑙 <Q 𝑥}, {𝑢 ∣ 𝑥 <Q 𝑢}⟩) ∧ 𝑦<P ⟨{𝑙 ∣ 𝑙 <Q ((𝐹‘𝑘) +Q 𝑥)}, {𝑢 ∣ ((𝐹‘𝑘) +Q 𝑥) <Q 𝑢}⟩))) | ||
Theorem | caucvgprprlemk 7684* | Lemma for caucvgprpr 7713. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
⊢ (𝜑 → 𝐽 <N 𝐾) & ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝑄) ⇒ ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐾, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐾, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝑄) | ||
Theorem | caucvgprprlemloccalc 7685* | Lemma for caucvgprpr 7713. Rearranging some expressions for caucvgprprlemloc 7704. (Contributed by Jim Kingdon, 8-Feb-2021.) |
⊢ (𝜑 → 𝑆 <Q 𝑇) & ⊢ (𝜑 → 𝑌 ∈ Q) & ⊢ (𝜑 → (𝑆 +Q 𝑌) = 𝑇) & ⊢ (𝜑 → 𝑋 ∈ Q) & ⊢ (𝜑 → (𝑋 +Q 𝑋) <Q 𝑌) & ⊢ (𝜑 → 𝑀 ∈ N) & ⊢ (𝜑 → (*Q‘[⟨𝑀, 1o⟩] ~Q ) <Q 𝑋) ⇒ ⊢ (𝜑 → (⟨{𝑙 ∣ 𝑙 <Q (𝑆 +Q (*Q‘[⟨𝑀, 1o⟩] ~Q ))}, {𝑢 ∣ (𝑆 +Q (*Q‘[⟨𝑀, 1o⟩] ~Q )) <Q 𝑢}⟩ +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑀, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑀, 1o⟩] ~Q ) <Q 𝑢}⟩)<P ⟨{𝑙 ∣ 𝑙 <Q 𝑇}, {𝑢 ∣ 𝑇 <Q 𝑢}⟩) | ||
Theorem | caucvgprprlemell 7686* | Lemma for caucvgprpr 7713. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ (𝑋 ∈ (1st ‘𝐿) ↔ (𝑋 ∈ Q ∧ ∃𝑏 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑋 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑋 +Q (*Q‘[⟨𝑏, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑏))) | ||
Theorem | caucvgprprlemelu 7687* | Lemma for caucvgprpr 7713. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ (𝑋 ∈ (2nd ‘𝐿) ↔ (𝑋 ∈ Q ∧ ∃𝑏 ∈ N ((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑋}, {𝑞 ∣ 𝑋 <Q 𝑞}⟩)) | ||
Theorem | caucvgprprlemcbv 7688* | Lemma for caucvgprpr 7713. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) ⇒ ⊢ (𝜑 → ∀𝑎 ∈ N ∀𝑏 ∈ N (𝑎 <N 𝑏 → ((𝐹‘𝑎)<P ((𝐹‘𝑏) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑏)<P ((𝐹‘𝑎) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑎, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑎, 1o⟩] ~Q ) <Q 𝑢}⟩)))) | ||
Theorem | caucvgprprlemval 7689* | Lemma for caucvgprpr 7713. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) ⇒ ⊢ ((𝜑 ∧ 𝐴 <N 𝐵) → ((𝐹‘𝐴)<P ((𝐹‘𝐵) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐴, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1o⟩] ~Q ) <Q 𝑞}⟩) ∧ (𝐹‘𝐵)<P ((𝐹‘𝐴) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐴, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐴, 1o⟩] ~Q ) <Q 𝑞}⟩))) | ||
Theorem | caucvgprprlemnkltj 7690* | Lemma for caucvgprpr 7713. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → 𝐾 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ ((𝜑 ∧ 𝐾 <N 𝐽) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) | ||
Theorem | caucvgprprlemnkeqj 7691* | Lemma for caucvgprpr 7713. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → 𝐾 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ ((𝜑 ∧ 𝐾 = 𝐽) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) | ||
Theorem | caucvgprprlemnjltk 7692* | Lemma for caucvgprpr 7713. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → 𝐾 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ ((𝜑 ∧ 𝐽 <N 𝐾) → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) | ||
Theorem | caucvgprprlemnkj 7693* | Lemma for caucvgprpr 7713. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → 𝐾 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) & ⊢ (𝜑 → 𝑆 ∈ Q) ⇒ ⊢ (𝜑 → ¬ (⟨{𝑝 ∣ 𝑝 <Q (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑆 +Q (*Q‘[⟨𝐾, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝐾) ∧ ((𝐹‘𝐽) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑆}, {𝑞 ∣ 𝑆 <Q 𝑞}⟩)) | ||
Theorem | caucvgprprlemnbj 7694* | Lemma for caucvgprpr 7713. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → 𝐵 ∈ N) & ⊢ (𝜑 → 𝐽 ∈ N) ⇒ ⊢ (𝜑 → ¬ (((𝐹‘𝐵) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐵, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐵, 1o⟩] ~Q ) <Q 𝑢}⟩) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑢}⟩)<P (𝐹‘𝐽)) | ||
Theorem | caucvgprprlemml 7695* | Lemma for caucvgprpr 7713. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿)) | ||
Theorem | caucvgprprlemmu 7696* | Lemma for caucvgprpr 7713. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ (𝜑 → ∃𝑡 ∈ Q 𝑡 ∈ (2nd ‘𝐿)) | ||
Theorem | caucvgprprlemm 7697* | Lemma for caucvgprpr 7713. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ (𝜑 → (∃𝑠 ∈ Q 𝑠 ∈ (1st ‘𝐿) ∧ ∃𝑡 ∈ Q 𝑡 ∈ (2nd ‘𝐿))) | ||
Theorem | caucvgprprlemopl 7698* | Lemma for caucvgprpr 7713. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 ∈ (1st ‘𝐿)) → ∃𝑡 ∈ Q (𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿))) | ||
Theorem | caucvgprprlemlol 7699* | Lemma for caucvgprpr 7713. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿)) → 𝑠 ∈ (1st ‘𝐿)) | ||
Theorem | caucvgprprlemopu 7700* | Lemma for caucvgprpr 7713. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
⊢ (𝜑 → 𝐹:N⟶P) & ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛)<P ((𝐹‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐹‘𝑘)<P ((𝐹‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩)))) & ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴<P (𝐹‘𝑚)) & ⊢ 𝐿 = ⟨{𝑙 ∈ Q ∣ ∃𝑟 ∈ N ⟨{𝑝 ∣ 𝑝 <Q (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q ))}, {𝑞 ∣ (𝑙 +Q (*Q‘[⟨𝑟, 1o⟩] ~Q )) <Q 𝑞}⟩<P (𝐹‘𝑟)}, {𝑢 ∈ Q ∣ ∃𝑟 ∈ N ((𝐹‘𝑟) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ⟨{𝑝 ∣ 𝑝 <Q 𝑢}, {𝑞 ∣ 𝑢 <Q 𝑞}⟩}⟩ ⇒ ⊢ ((𝜑 ∧ 𝑡 ∈ (2nd ‘𝐿)) → ∃𝑠 ∈ Q (𝑠 <Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |