P. 77 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cauappcvgprlem2 7601*	Lemma for cauappcvgpr 7603. 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 7602*	Lemma for cauappcvgpr 7603. 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 7603*	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 7623 and caucvgprpr 7653 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 7604*	Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
⊢ (𝐴 ∈ Q → ∃𝑗 ∈ N (*Q‘[⟨𝑗, 1o⟩] ~Q ) <Q 𝐴)
Theorem	archrecpr 7605*	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 7606	Lemma for caucvgpr 7623. 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 7607*	Lemma for caucvgpr 7623. 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 7608*	Lemma for caucvgpr 7623. 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 7609*	Lemma for caucvgpr 7623. 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 7610*	Lemma for caucvgpr 7623. 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 7611*	Lemma for caucvgpr 7623. 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 7612*	Lemma for caucvgpr 7623. 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 7613*	Lemma for caucvgpr 7623. 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 7614*	Lemma for caucvgpr 7623. 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 7615*	Lemma for caucvgpr 7623. 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 7616*	Lemma for caucvgpr 7623. 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 7617*	Lemma for caucvgpr 7623. 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 7618*	Lemma for caucvgpr 7623. 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 7619*	Lemma for caucvgpr 7623. 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 7620*	Lemma for caucvgpr 7623. 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 7621*	Lemma for caucvgpr 7623. 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 7622*	Lemma for caucvgpr 7623. 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 7623*	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 7603 and caucvgprpr 7653. Reading cauappcvgpr 7603 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 7624*	Lemma for caucvgprpr 7653. 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 7625*	Lemma for caucvgprpr 7653. Rearranging some expressions for caucvgprprlemloc 7644. (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 7626*	Lemma for caucvgprpr 7653. 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 7627*	Lemma for caucvgprpr 7653. 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 7628*	Lemma for caucvgprpr 7653. 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 7629*	Lemma for caucvgprpr 7653. 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 7630*	Lemma for caucvgprpr 7653. 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 7631*	Lemma for caucvgprpr 7653. 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 7632*	Lemma for caucvgprpr 7653. 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 7633*	Lemma for caucvgprpr 7653. 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 7634*	Lemma for caucvgprpr 7653. 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 7635*	Lemma for caucvgprpr 7653. 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 7636*	Lemma for caucvgprpr 7653. 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 7637*	Lemma for caucvgprpr 7653. 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 7638*	Lemma for caucvgprpr 7653. 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 7639*	Lemma for caucvgprpr 7653. 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 7640*	Lemma for caucvgprpr 7653. 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 7641*	Lemma for caucvgprpr 7653. 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 7642*	Lemma for caucvgprpr 7653. 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 7643*	Lemma for caucvgprpr 7653. 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 7644*	Lemma for caucvgprpr 7653. 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 7645*	Lemma for caucvgprpr 7653. 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 7646*	Lemma for caucvgprpr 7653. The putative limit is a positive real. Like caucvgprprlemcl 7645 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 7647*	Lemma for caucvgprpr 7653. 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 7648*	Lemma for caucvgprpr 7653. 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 7649*	Lemma for caucvgprpr 7653. 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 7650*	Lemma for caucvgprpr 7653. 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 7651*	Lemma for caucvgprpr 7653. 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 7652*	Lemma for caucvgprpr 7653. 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 7653*	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 7623 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 7603) 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 7654*	Lemma for suplocexpr 7666. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
⊢ (𝐵 ∈ ∪ (1st “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 𝐵 ∈ (1st ‘𝑥))
Theorem	suplocexprlem2b 7655	Lemma for suplocexpr 7666. 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 7656*	Lemma for suplocexpr 7666. 𝐴 is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ P)
Theorem	suplocexprlemml 7657*	Lemma for suplocexpr 7666. 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 7658*	Lemma for suplocexpr 7666. 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 7659*	Lemma for suplocexpr 7666. 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 7660*	Lemma for suplocexpr 7666. 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 7661*	Lemma for suplocexpr 7666. 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 7662*	Lemma for suplocexpr 7666. 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 7663*	Lemma for suplocexpr 7666. 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 7664*	Lemma for suplocexpr 7666. 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 7665*	Lemma for suplocexpr 7666. 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 7666*	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 7667*	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 7668	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 7669*	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 7670*	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 7671*	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 7672	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 7673	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
Definition	df-m1r 7674	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. (Contributed by NM, 9-Aug-1995.)
⊢ -1R = [⟨1P, (1P +P 1P)⟩] ~R
Theorem	enrbreq 7675	Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → (⟨𝐴, 𝐵⟩ ~R ⟨𝐶, 𝐷⟩ ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶)))
Theorem	enrer 7676	The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
⊢ ~R Er (P × P)
Theorem	enreceq 7677	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷) = (𝐵 +P 𝐶)))
Theorem	enrex 7678	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.)
⊢ ~R ∈ V
Theorem	ltrelsr 7679	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.)
⊢ <R ⊆ (R × R)
Theorem	addcmpblnr 7680	Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.)
⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨(𝐴 +P 𝐹), (𝐵 +P 𝐺)⟩ ~R ⟨(𝐶 +P 𝑅), (𝐷 +P 𝑆)⟩))
Theorem	mulcmpblnrlemg 7681	Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆))))))
Theorem	mulcmpblnr 7682	Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.)
⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))
Theorem	prsrlem1 7683*	Decomposing signed reals into positive reals. Lemma for addsrpr 7686 and mulsrpr 7687. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ (((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) ∧ ((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ (𝐴 = [⟨𝑠, 𝑓⟩] ~R ∧ 𝐵 = [⟨𝑔, ℎ⟩] ~R ))) → ((((𝑤 ∈ P ∧ 𝑣 ∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧ ((𝑢 ∈ P ∧ 𝑡 ∈ P) ∧ (𝑔 ∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔))))
Theorem	addsrmo 7684*	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
Theorem	mulsrmo 7685*	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
⊢ ((𝐴 ∈ ((P × P) / ~R ) ∧ 𝐵 ∈ ((P × P) / ~R )) → ∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [⟨𝑤, 𝑣⟩] ~R ∧ 𝐵 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R ))
Theorem	addsrpr 7686	Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
Theorem	mulsrpr 7687	Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )
Theorem	ltsrprg 7688	Ordering of signed reals in terms of positive reals. (Contributed by Jim Kingdon, 2-Jan-2019.)
⊢ (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) → ([⟨𝐴, 𝐵⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶)))
Theorem	gt0srpr 7689	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
⊢ (0R <R [⟨𝐴, 𝐵⟩] ~R ↔ 𝐵<P 𝐴)
Theorem	0nsr 7690	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
⊢ ¬ ∅ ∈ R
Theorem	0r 7691	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 0R ∈ R
Theorem	1sr 7692	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 1R ∈ R
Theorem	m1r 7693	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ -1R ∈ R
Theorem	addclsr 7694	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R)
Theorem	mulclsr 7695	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R)
Theorem	addcomsrg 7696	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) = (𝐵 +R 𝐴))
Theorem	addasssrg 7697	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 +R 𝐵) +R 𝐶) = (𝐴 +R (𝐵 +R 𝐶)))
Theorem	mulcomsrg 7698	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) = (𝐵 ·R 𝐴))
Theorem	mulasssrg 7699	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐵) ·R 𝐶) = (𝐴 ·R (𝐵 ·R 𝐶)))
Theorem	distrsrg 7700	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → (𝐴 ·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R (𝐴 ·R 𝐶)))