P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recexprlem1ssl 8001*	The lower cut of one is a subset of the lower cut of 𝐴 ·P 𝐵. Lemma for recexpr 8006. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵)))
Theorem	recexprlem1ssu 8002*	The upper cut of one is a subset of the upper cut of 𝐴 ·P 𝐵. Lemma for recexpr 8006. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵)))
Theorem	recexprlemss1l 8003*	The lower cut of 𝐴 ·P 𝐵 is a subset of the lower cut of one. Lemma for recexpr 8006. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (1st ‘(𝐴 ·P 𝐵)) ⊆ (1st ‘1P))
Theorem	recexprlemss1u 8004*	The upper cut of 𝐴 ·P 𝐵 is a subset of the upper cut of one. Lemma for recexpr 8006. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (2nd ‘(𝐴 ·P 𝐵)) ⊆ (2nd ‘1P))
Theorem	recexprlemex 8005*	𝐵 is the reciprocal of 𝐴. Lemma for recexpr 8006. (Contributed by Jim Kingdon, 27-Dec-2019.)
⊢ 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q‘𝑦) ∈ (2nd ‘𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q‘𝑦) ∈ (1st ‘𝐴))}⟩    ⇒   ⊢ (𝐴 ∈ P → (𝐴 ·P 𝐵) = 1P)
Theorem	recexpr 8006*	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 8007	Lemma for aptipr 8009. (Contributed by Jim Kingdon, 28-Jan-2020.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (1st ‘𝐴) ⊆ (1st ‘𝐵))
Theorem	aptiprlemu 8008	Lemma for aptipr 8009. (Contributed by Jim Kingdon, 28-Jan-2020.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ 𝐵<P 𝐴) → (2nd ‘𝐵) ⊆ (2nd ‘𝐴))
Theorem	aptipr 8009	Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ ¬ (𝐴<P 𝐵 ∨ 𝐵<P 𝐴)) → 𝐴 = 𝐵)
Theorem	ltmprr 8010	Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P) → ((𝐶 ·P 𝐴)<P (𝐶 ·P 𝐵) → 𝐴<P 𝐵))
Theorem	archpr 8011*	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 7921. (Contributed by Jim Kingdon, 22-Apr-2020.)
⊢ (𝐴 ∈ P → ∃𝑥 ∈ N 𝐴<P ⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩] ~Q <Q 𝑢}⟩)
Theorem	caucvgprlemcanl 8012*	Lemma for cauappcvgprlemladdrl 8025. 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 8013*	Lemma for cauappcvgpr 8030. 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 8014*	Lemma for cauappcvgpr 8030. 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 8015*	Lemma for cauappcvgpr 8030. 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 8016*	Lemma for cauappcvgpr 8030. 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 8017*	Lemma for cauappcvgpr 8030. 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 8018*	Lemma for cauappcvgpr 8030. 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 8019*	Lemma for cauappcvgpr 8030. 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 8020*	Lemma for cauappcvgpr 8030. 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 8021*	Lemma for cauappcvgpr 8030. 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 8022*	Lemma for cauappcvgprlemladd 8026. 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 8023*	Lemma for cauappcvgprlemladd 8026. 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 8024*	Lemma for cauappcvgprlemladd 8026. 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 8025*	Lemma for cauappcvgprlemladd 8026. 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 8026*	Lemma for cauappcvgpr 8030. 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 8027*	Lemma for cauappcvgpr 8030. 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 8028*	Lemma for cauappcvgpr 8030. 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 8029*	Lemma for cauappcvgpr 8030. 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 8030*	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 8050 and caucvgprpr 8080 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 8031*	Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
⊢ (𝐴 ∈ Q → ∃𝑗 ∈ N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴)
Theorem	archrecpr 8032*	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 8033	Lemma for caucvgpr 8050. 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 8034*	Lemma for caucvgpr 8050. 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 8035*	Lemma for caucvgpr 8050. 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 8036*	Lemma for caucvgpr 8050. 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 8037*	Lemma for caucvgpr 8050. 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 8038*	Lemma for caucvgpr 8050. 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 8039*	Lemma for caucvgpr 8050. 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 8040*	Lemma for caucvgpr 8050. 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 8041*	Lemma for caucvgpr 8050. 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 8042*	Lemma for caucvgpr 8050. 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 8043*	Lemma for caucvgpr 8050. 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 8044*	Lemma for caucvgpr 8050. 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 8045*	Lemma for caucvgpr 8050. 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 8046*	Lemma for caucvgpr 8050. 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 8047*	Lemma for caucvgpr 8050. 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 8048*	Lemma for caucvgpr 8050. 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 8049*	Lemma for caucvgpr 8050. 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 8050*	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 8030 and caucvgprpr 8080. Reading cauappcvgpr 8030 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 8051*	Lemma for caucvgprpr 8080. 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 8052*	Lemma for caucvgprpr 8080. Rearranging some expressions for caucvgprprlemloc 8071. (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 8053*	Lemma for caucvgprpr 8080. 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 8054*	Lemma for caucvgprpr 8080. 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 8055*	Lemma for caucvgprpr 8080. 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 8056*	Lemma for caucvgprpr 8080. 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 8057*	Lemma for caucvgprpr 8080. 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 8058*	Lemma for caucvgprpr 8080. 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 8059*	Lemma for caucvgprpr 8080. 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 8060*	Lemma for caucvgprpr 8080. 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 8061*	Lemma for caucvgprpr 8080. 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 8062*	Lemma for caucvgprpr 8080. 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 8063*	Lemma for caucvgprpr 8080. 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 8064*	Lemma for caucvgprpr 8080. 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 8065*	Lemma for caucvgprpr 8080. 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 8066*	Lemma for caucvgprpr 8080. 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 8067*	Lemma for caucvgprpr 8080. 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 8068*	Lemma for caucvgprpr 8080. 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 8069*	Lemma for caucvgprpr 8080. 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 8070*	Lemma for caucvgprpr 8080. 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 ‘𝐿)))
Theorem	caucvgprprlemloc 8071*	Lemma for caucvgprpr 8080. The putative limit is located. (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 ∀𝑡 ∈ Q (𝑠 <Q 𝑡 → (𝑠 ∈ (1st ‘𝐿) ∨ 𝑡 ∈ (2nd ‘𝐿))))
Theorem	caucvgprprlemcl 8072*	Lemma for caucvgprpr 8080. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-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 𝑞}⟩}⟩    ⇒   ⊢ (𝜑 → 𝐿 ∈ P)
Theorem	caucvgprprlemclphr 8073*	Lemma for caucvgprpr 8080. The putative limit is a positive real. Like caucvgprprlemcl 8072 but without a disjoint variable condition between 𝜑 and 𝑟. (Contributed by Jim Kingdon, 19-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 𝐴<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 𝑞}⟩}⟩    ⇒   ⊢ (𝜑 → 𝐿 ∈ P)
Theorem	caucvgprprlemexbt 8074*	Lemma for caucvgprpr 8080. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-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 𝐴<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)    &   ⊢ (𝜑 → 𝑇 ∈ P)    &   ⊢ (𝜑 → (𝐿 +P ⟨{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}⟩)<P 𝑇)    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P ⟨{𝑝 ∣ 𝑝 <Q 𝑄}, {𝑞 ∣ 𝑄 <Q 𝑞}⟩)<P 𝑇)
Theorem	caucvgprprlemexb 8075*	Lemma for caucvgprpr 8080. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-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 𝐴<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 𝑞}⟩}⟩    &   ⊢ (𝜑 → 𝑄 ∈ P)    &   ⊢ (𝜑 → 𝑅 ∈ N)    ⇒   ⊢ (𝜑 → (((𝐿 +P 𝑄) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑅, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑅, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑅) +P 𝑄) → ∃𝑏 ∈ N (((𝐹‘𝑏) +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑏, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑏, 1o⟩] ~Q ) <Q 𝑞}⟩) +P (𝑄 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑅, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑅, 1o⟩] ~Q ) <Q 𝑞}⟩))<P ((𝐹‘𝑅) +P 𝑄)))
Theorem	caucvgprprlemaddq 8076*	Lemma for caucvgprpr 8080. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-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 𝐴<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 𝑞}⟩}⟩    &   ⊢ (𝜑 → 𝑋 ∈ P)    &   ⊢ (𝜑 → 𝑄 ∈ P)    &   ⊢ (𝜑 → ∃𝑟 ∈ N (𝑋 +P ⟨{𝑝 ∣ 𝑝 <Q (*Q‘[⟨𝑟, 1o⟩] ~Q )}, {𝑞 ∣ (*Q‘[⟨𝑟, 1o⟩] ~Q ) <Q 𝑞}⟩)<P ((𝐹‘𝑟) +P 𝑄))    ⇒   ⊢ (𝜑 → 𝑋<P (𝐿 +P 𝑄))
Theorem	caucvgprprlem1 8077*	Lemma for caucvgprpr 8080. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-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 𝑞}⟩}⟩    &   ⊢ (𝜑 → 𝑄 ∈ P)    &   ⊢ (𝜑 → 𝐽 <N 𝐾)    &   ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝑄)    ⇒   ⊢ (𝜑 → (𝐹‘𝐾)<P (𝐿 +P 𝑄))
Theorem	caucvgprprlem2 8078*	Lemma for caucvgprpr 8080. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-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 𝑞}⟩}⟩    &   ⊢ (𝜑 → 𝑄 ∈ P)    &   ⊢ (𝜑 → 𝐽 <N 𝐾)    &   ⊢ (𝜑 → ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝐽, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝐽, 1o⟩] ~Q ) <Q 𝑢}⟩<P 𝑄)    ⇒   ⊢ (𝜑 → 𝐿<P ((𝐹‘𝐾) +P 𝑄))
Theorem	caucvgprprlemlim 8079*	Lemma for caucvgprpr 8080. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-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 𝑞}⟩}⟩    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘)<P (𝐿 +P 𝑥) ∧ 𝐿<P ((𝐹‘𝑘) +P 𝑥))))
Theorem	caucvgprpr 8080*	A Cauchy sequence of positive reals 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 given value 𝐴, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real). This is similar to caucvgpr 8050 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 8030) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-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 (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ P ∀𝑥 ∈ P ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘)<P (𝑦 +P 𝑥) ∧ 𝑦<P ((𝐹‘𝑘) +P 𝑥))))
Theorem	suplocexprlemell 8081*	Lemma for suplocexpr 8093. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝐵 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (1st ‘𝑥))
Theorem	suplocexprlem2b 8082	Lemma for suplocexpr 8093. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝐴 ⊆ P → (2nd ‘𝐵) = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})
Theorem	suplocexprlemss 8083*	Lemma for suplocexpr 8093. 𝐴 is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ P)
Theorem	suplocexprlemml 8084*	Lemma for suplocexpr 8093. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ ∪ (1st “ 𝐴))
Theorem	suplocexprlemrl 8085*	Lemma for suplocexpr 8093. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ Q (𝑞 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ ∪ (1st “ 𝐴))))
Theorem	suplocexprlemmu 8086*	Lemma for suplocexpr 8093. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (2nd ‘𝐵))
Theorem	suplocexprlemru 8087*	Lemma for suplocexpr 8093. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → ∀𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝐵) ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ (2nd ‘𝐵))))
Theorem	suplocexprlemdisj 8088*	Lemma for suplocexpr 8093. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ Q ¬ (𝑞 ∈ ∪ (1st “ 𝐴) ∧ 𝑞 ∈ (2nd ‘𝐵)))
Theorem	suplocexprlemloc 8089*	Lemma for suplocexpr 8093. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ ∪ (1st “ 𝐴) ∨ 𝑟 ∈ (2nd ‘𝐵))))
Theorem	suplocexprlemex 8090*	Lemma for suplocexpr 8093. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → 𝐵 ∈ P)
Theorem	suplocexprlemub 8091*	Lemma for suplocexpr 8093. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ¬ 𝐵<P 𝑦)
Theorem	suplocexprlemlub 8092*	Lemma for suplocexpr 8093. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    &   ⊢ 𝐵 = ⟨∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}⟩    ⇒   ⊢ (𝜑 → (𝑦<P 𝐵 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))
Theorem	suplocexpr 8093*	An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P 𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))
Definition	df-enr 8094*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
⊢ ~R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (P × P) ∧ 𝑦 ∈ (P × P)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 +P 𝑢) = (𝑤 +P 𝑣)))}
Definition	df-nr 8095	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
⊢ R = ((P × P) / ~R )
Definition	df-plr 8096*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
⊢ +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑓)⟩] ~R ))}
Definition	df-mr 8097*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
⊢ ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝑦 = [⟨𝑢, 𝑓⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑓)), ((𝑤 ·P 𝑓) +P (𝑣 ·P 𝑢))⟩] ~R ))}
Definition	df-ltr 8098*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.)
⊢ <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
Definition	df-0r 8099	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
⊢ 0R = [⟨1P, 1P⟩] ~R
Definition	df-1r 8100	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
⊢ 1R = [⟨(1P +P 1P), 1P⟩] ~R