![]() |
Intuitionistic Logic Explorer Theorem List (p. 77 of 148) | < 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 | ltexprlemopu 7601* | The upper cut of our constructed difference is open. Lemma for ltexpri 7611. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐶)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemupu 7602* | The upper cut of our constructed difference is upper. Lemma for ltexpri 7611. (Contributed by Jim Kingdon, 21-Dec-2019.) |
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}〉 ⇒ ⊢ ((𝐴<P 𝐵 ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐶)) → 𝑟 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemrnd 7603* | Our constructed difference is rounded. Lemma for ltexpri 7611. (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 7604* | Our constructed difference is disjoint. Lemma for ltexpri 7611. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐶) ∧ 𝑞 ∈ (2nd ‘𝐶))) | ||
Theorem | ltexprlemloc 7605* | Our constructed difference is located. Lemma for ltexpri 7611. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐶) ∨ 𝑟 ∈ (2nd ‘𝐶)))) | ||
Theorem | ltexprlempr 7606* | Our constructed difference is a positive real. Lemma for ltexpri 7611. (Contributed by Jim Kingdon, 17-Dec-2019.) |
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st ‘𝐵))}, {𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd ‘𝐵))}〉 ⇒ ⊢ (𝐴<P 𝐵 → 𝐶 ∈ P) | ||
Theorem | ltexprlemfl 7607* | Lemma for ltexpri 7611. 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 7608* | Lemma for ltexpri 7611. 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 7609* | Lemma for ltexpri 7611. 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 7610* | Lemma for ltexpri 7611. 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 7611* | 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 7612 | Lemma for addcanprg 7614. (Contributed by Jim Kingdon, 25-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (1st ‘𝐵) ⊆ (1st ‘𝐶)) | ||
Theorem | addcanprlemu 7613 | Lemma for addcanprg 7614. (Contributed by Jim Kingdon, 25-Dec-2019.) |
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) ∧ (𝐴 +P 𝐵) = (𝐴 +P 𝐶)) → (2nd ‘𝐵) ⊆ (2nd ‘𝐶)) | ||
Theorem | addcanprg 7614 | 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 7615* | The difference from ltexpri 7611 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
⊢ (𝐴<P 𝐵 → ∃!𝑥 ∈ P (𝐴 +P 𝑥) = 𝐵) | ||
Theorem | ltaprlem 7616 | Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) |
⊢ (𝐶 ∈ P → (𝐴<P 𝐵 → (𝐶 +P 𝐴)<P (𝐶 +P 𝐵))) | ||
Theorem | ltaprg 7617 | 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 7618* | 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 7619 | Strong extensionality of addition (ordering version). This is similar to addext 8565 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 7620* | Membership in the lower cut of 𝐵. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐶 ∈ (1st ‘𝐵) ↔ ∃𝑦(𝐶 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))) | ||
Theorem | recexprlemelu 7621* | Membership in the upper cut of 𝐵. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐶 ∈ (2nd ‘𝐵) ↔ ∃𝑦(𝑦 <Q 𝐶 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))) | ||
Theorem | recexprlemm 7622* | 𝐵 is inhabited. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (∃𝑞 ∈ Q 𝑞 ∈ (1st ‘𝐵) ∧ ∃𝑟 ∈ Q 𝑟 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemopl 7623* | The lower cut of 𝐵 is open. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q ∧ 𝑞 ∈ (1st ‘𝐵)) → ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵))) | ||
Theorem | recexprlemlol 7624* | The lower cut of 𝐵 is lower. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑞 ∈ Q) → (∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ (1st ‘𝐵)) → 𝑞 ∈ (1st ‘𝐵))) | ||
Theorem | recexprlemopu 7625* | The upper cut of 𝐵 is open. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑟 ∈ Q ∧ 𝑟 ∈ (2nd ‘𝐵)) → ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemupu 7626* | The upper cut of 𝐵 is upper. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 28-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ ((𝐴 ∈ P ∧ 𝑟 ∈ Q) → (∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵)) → 𝑟 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemrnd 7627* | 𝐵 is rounded. Lemma for recexpr 7636. (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 7628* | 𝐵 is disjoint. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → ∀𝑞 ∈ Q ¬ (𝑞 ∈ (1st ‘𝐵) ∧ 𝑞 ∈ (2nd ‘𝐵))) | ||
Theorem | recexprlemloc 7629* | 𝐵 is located. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ (1st ‘𝐵) ∨ 𝑟 ∈ (2nd ‘𝐵)))) | ||
Theorem | recexprlempr 7630* | 𝐵 is a positive real. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → 𝐵 ∈ P) | ||
Theorem | recexprlem1ssl 7631* | The lower cut of one is a subset of the lower cut of 𝐴 ·P 𝐵. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵))) | ||
Theorem | recexprlem1ssu 7632* | The upper cut of one is a subset of the upper cut of 𝐴 ·P 𝐵. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵))) | ||
Theorem | recexprlemss1l 7633* | The lower cut of 𝐴 ·P 𝐵 is a subset of the lower cut of one. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (1st ‘(𝐴 ·P 𝐵)) ⊆ (1st ‘1P)) | ||
Theorem | recexprlemss1u 7634* | The upper cut of 𝐴 ·P 𝐵 is a subset of the upper cut of one. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (2nd ‘(𝐴 ·P 𝐵)) ⊆ (2nd ‘1P)) | ||
Theorem | recexprlemex 7635* | 𝐵 is the reciprocal of 𝐴. Lemma for recexpr 7636. (Contributed by Jim Kingdon, 27-Dec-2019.) |
⊢ 𝐵 = 〈{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}〉 ⇒ ⊢ (𝐴 ∈ P → (𝐴 ·P 𝐵) = 1P) | ||
Theorem | recexpr 7636* | 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 7637 | Lemma for aptipr 7639. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (1st ‘𝐴) ⊆ (1st ‘𝐵)) | ||
Theorem | aptiprlemu 7638 | Lemma for aptipr 7639. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (2nd ‘𝐵) ⊆ (2nd ‘𝐴)) | ||
Theorem | aptipr 7639 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ (𝐴<P 𝐵 ∨ 𝐵<P 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | ltmprr 7640 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐶 ·P 𝐴)<P (𝐶 ·P 𝐵) → 𝐴<P 𝐵)) | ||
Theorem | archpr 7641* | 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 7551. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝐴 ∈ P → ∃𝑥 ∈ N 𝐴<P 〈{𝑙 ∣ 𝑙 <Q [〈𝑥, 1o〉] ~Q }, {𝑢 ∣ [〈𝑥, 1o〉] ~Q <Q 𝑢}〉) | ||
Theorem | caucvgprlemcanl 7642* | Lemma for cauappcvgprlemladdrl 7655. 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 7643* | Lemma for cauappcvgpr 7660. 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 7644* | Lemma for cauappcvgpr 7660. 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 7645* | Lemma for cauappcvgpr 7660. 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 7646* | Lemma for cauappcvgpr 7660. 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 7647* | Lemma for cauappcvgpr 7660. 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 7648* | Lemma for cauappcvgpr 7660. 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 7649* | Lemma for cauappcvgpr 7660. 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 7650* | Lemma for cauappcvgpr 7660. 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 7651* | Lemma for cauappcvgpr 7660. 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 7652* | Lemma for cauappcvgprlemladd 7656. 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 7653* | Lemma for cauappcvgprlemladd 7656. 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 7654* | Lemma for cauappcvgprlemladd 7656. 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 7655* | Lemma for cauappcvgprlemladd 7656. 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 7656* | Lemma for cauappcvgpr 7660. 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 7657* | Lemma for cauappcvgpr 7660. 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 7658* | Lemma for cauappcvgpr 7660. 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 7659* | Lemma for cauappcvgpr 7660. 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 7660* |
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 7680 and caucvgprpr 7710 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 7661* | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
⊢ (𝐴 ∈ Q → ∃𝑗 ∈ N (*Q‘[〈𝑗, 1o〉] ~Q ) <Q 𝐴) | ||
Theorem | archrecpr 7662* | 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 7663 | Lemma for caucvgpr 7680. 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 7664* | Lemma for caucvgpr 7680. 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 7665* | Lemma for caucvgpr 7680. 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 7666* | Lemma for caucvgpr 7680. 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 7667* | Lemma for caucvgpr 7680. 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 7668* | Lemma for caucvgpr 7680. 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 7669* | Lemma for caucvgpr 7680. 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 7670* | Lemma for caucvgpr 7680. 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 7671* | Lemma for caucvgpr 7680. 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 7672* | Lemma for caucvgpr 7680. 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 7673* | Lemma for caucvgpr 7680. 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 7674* | Lemma for caucvgpr 7680. 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 7675* | Lemma for caucvgpr 7680. 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 7676* | Lemma for caucvgpr 7680. 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 7677* | Lemma for caucvgpr 7680. 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 7678* | Lemma for caucvgpr 7680. 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 7679* | Lemma for caucvgpr 7680. 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 7680* |
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 7660 and caucvgprpr 7710. Reading cauappcvgpr 7660 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 7681* | Lemma for caucvgprpr 7710. 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 7682* | Lemma for caucvgprpr 7710. Rearranging some expressions for caucvgprprlemloc 7701. (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 7683* | Lemma for caucvgprpr 7710. 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 7684* | Lemma for caucvgprpr 7710. 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 7685* | Lemma for caucvgprpr 7710. 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 7686* | Lemma for caucvgprpr 7710. 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 7687* | Lemma for caucvgprpr 7710. 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 7688* | Lemma for caucvgprpr 7710. 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 7689* | Lemma for caucvgprpr 7710. 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 7690* | Lemma for caucvgprpr 7710. 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 7691* | Lemma for caucvgprpr 7710. 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 7692* | Lemma for caucvgprpr 7710. 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 7693* | Lemma for caucvgprpr 7710. 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 7694* | Lemma for caucvgprpr 7710. 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 7695* | Lemma for caucvgprpr 7710. 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 7696* | Lemma for caucvgprpr 7710. 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 7697* | Lemma for caucvgprpr 7710. 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 ‘𝐿))) | ||
Theorem | caucvgprprlemupu 7698* | Lemma for caucvgprpr 7710. The upper cut of the putative limit is upper. (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 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿)) → 𝑡 ∈ (2nd ‘𝐿)) | ||
Theorem | caucvgprprlemrnd 7699* | Lemma for caucvgprpr 7710. The putative limit is rounded. (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 (𝑠 <Q 𝑡 ∧ 𝑡 ∈ (1st ‘𝐿))) ∧ ∀𝑡 ∈ Q (𝑡 ∈ (2nd ‘𝐿) ↔ ∃𝑠 ∈ Q (𝑠 <Q 𝑡 ∧ 𝑠 ∈ (2nd ‘𝐿))))) | ||
Theorem | caucvgprprlemdisj 7700* | Lemma for caucvgprpr 7710. The putative limit is disjoint. (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 ‘𝐿) ∧ 𝑠 ∈ (2nd ‘𝐿))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |