P. 79 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7801-7900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	suplocexprlemss 7801*	Lemma for suplocexpr 7811. 𝐴 is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P 𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦)))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ P)
Theorem	suplocexprlemml 7802*	Lemma for suplocexpr 7811. 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 7803*	Lemma for suplocexpr 7811. 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 7804*	Lemma for suplocexpr 7811. 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 7805*	Lemma for suplocexpr 7811. 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 7806*	Lemma for suplocexpr 7811. 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 7807*	Lemma for suplocexpr 7811. 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 7808*	Lemma for suplocexpr 7811. 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 7809*	Lemma for suplocexpr 7811. 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 7810*	Lemma for suplocexpr 7811. 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 7811*	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 7812*	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 7813	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 7814*	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 7815*	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 7816*	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 7817	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 7818	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 7819	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 7820	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 7821	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 7822	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 7823	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.)
⊢ ~R ∈ V
Theorem	ltrelsr 7824	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.)
⊢ <R ⊆ (R × R)
Theorem	addcmpblnr 7825	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 7826	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 7827	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 7828*	Decomposing signed reals into positive reals. Lemma for addsrpr 7831 and mulsrpr 7832. (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 7829*	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 7830*	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 7831	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 7832	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 7833	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 7834	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
⊢ (0R <R [⟨𝐴, 𝐵⟩] ~R ↔ 𝐵<P 𝐴)
Theorem	0nsr 7835	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
⊢ ¬ ∅ ∈ R
Theorem	0r 7836	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 0R ∈ R
Theorem	1sr 7837	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 1R ∈ R
Theorem	m1r 7838	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ -1R ∈ R
Theorem	addclsr 7839	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R)
Theorem	mulclsr 7840	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R)
Theorem	addcomsrg 7841	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) = (𝐵 +R 𝐴))
Theorem	addasssrg 7842	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 +R 𝐵) +R 𝐶) = (𝐴 +R (𝐵 +R 𝐶)))
Theorem	mulcomsrg 7843	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) = (𝐵 ·R 𝐴))
Theorem	mulasssrg 7844	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐵) ·R 𝐶) = (𝐴 ·R (𝐵 ·R 𝐶)))
Theorem	distrsrg 7845	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → (𝐴 ·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R (𝐴 ·R 𝐶)))
Theorem	m1p1sr 7846	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.)
⊢ (-1R +R 1R) = 0R
Theorem	m1m1sr 7847	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.)
⊢ (-1R ·R -1R) = 1R
Theorem	lttrsr 7848*	Signed real 'less than' is a transitive relation. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → ((𝑓 <R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ))
Theorem	ltposr 7849	Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ <R Po R
Theorem	ltsosr 7850	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.)
⊢ <R Or R
Theorem	0lt1sr 7851	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.)
⊢ 0R <R 1R
Theorem	1ne0sr 7852	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.)
⊢ ¬ 1R = 0R
Theorem	0idsr 7853	The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.)
⊢ (𝐴 ∈ R → (𝐴 +R 0R) = 𝐴)
Theorem	1idsr 7854	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
⊢ (𝐴 ∈ R → (𝐴 ·R 1R) = 𝐴)
Theorem	00sr 7855	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
⊢ (𝐴 ∈ R → (𝐴 ·R 0R) = 0R)
Theorem	ltasrg 7856	Ordering property of addition. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
Theorem	pn0sr 7857	A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.)
⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R)
Theorem	negexsr 7858*	Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.)
⊢ (𝐴 ∈ R → ∃𝑥 ∈ R (𝐴 +R 𝑥) = 0R)
Theorem	recexgt0sr 7859*	The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)
⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (0R <R 𝑥 ∧ (𝐴 ·R 𝑥) = 1R))
Theorem	recexsrlem 7860*	The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.)
⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R)
Theorem	addgt0sr 7861	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))
Theorem	ltadd1sr 7862	Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.)
⊢ (𝐴 ∈ R → 𝐴 <R (𝐴 +R 1R))
Theorem	ltm1sr 7863	Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.)
⊢ (𝐴 ∈ R → (𝐴 +R -1R) <R 𝐴)
Theorem	mulgt0sr 7864	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵))
Theorem	aptisr 7865	Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ ¬ (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴)) → 𝐴 = 𝐵)
Theorem	mulextsr1lem 7866	Lemma for mulextsr1 7867. (Contributed by Jim Kingdon, 17-Feb-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 𝑋))))
Theorem	mulextsr1 7867	Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐶) <R (𝐵 ·R 𝐶) → (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴)))
Theorem	archsr 7868*	For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R is the embedding of the positive integer 𝑥 into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
⊢ (𝐴 ∈ R → ∃𝑥 ∈ N 𝐴 <R [⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑥, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑥, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
Theorem	srpospr 7869*	Mapping from a signed real greater than zero to a positive real. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ ((𝐴 ∈ R ∧ 0R <R 𝐴) → ∃!𝑥 ∈ P [⟨(𝑥 +P 1P), 1P⟩] ~R = 𝐴)
Theorem	prsrcl 7870	Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ (𝐴 ∈ P → [⟨(𝐴 +P 1P), 1P⟩] ~R ∈ R)
Theorem	prsrpos 7871	Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ (𝐴 ∈ P → 0R <R [⟨(𝐴 +P 1P), 1P⟩] ~R )
Theorem	prsradd 7872	Mapping from positive real addition to signed real addition. (Contributed by Jim Kingdon, 29-Jun-2021.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → [⟨((𝐴 +P 𝐵) +P 1P), 1P⟩] ~R = ([⟨(𝐴 +P 1P), 1P⟩] ~R +R [⟨(𝐵 +P 1P), 1P⟩] ~R ))
Theorem	prsrlt 7873	Mapping from positive real ordering to signed real ordering. (Contributed by Jim Kingdon, 29-Jun-2021.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P) → (𝐴<P 𝐵 ↔ [⟨(𝐴 +P 1P), 1P⟩] ~R <R [⟨(𝐵 +P 1P), 1P⟩] ~R ))
Theorem	prsrriota 7874*	Mapping a restricted iota from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
⊢ ((𝐴 ∈ R ∧ 0R <R 𝐴) → [⟨((℩𝑥 ∈ P [⟨(𝑥 +P 1P), 1P⟩] ~R = 𝐴) +P 1P), 1P⟩] ~R = 𝐴)
Theorem	caucvgsrlemcl 7875*	Lemma for caucvgsr 7888. Terms of the sequence from caucvgsrlemgt1 7881 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ N) → (℩𝑦 ∈ P (𝐹‘𝐴) = [⟨(𝑦 +P 1P), 1P⟩] ~R ) ∈ P)
Theorem	caucvgsrlemasr 7876*	Lemma for caucvgsr 7888. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → 𝐴 ∈ R)
Theorem	caucvgsrlemfv 7877*	Lemma for caucvgsr 7888. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ N) → [⟨((𝐺‘𝐴) +P 1P), 1P⟩] ~R = (𝐹‘𝐴))
Theorem	caucvgsrlemf 7878*	Lemma for caucvgsr 7888. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))    ⇒   ⊢ (𝜑 → 𝐺:N⟶P)
Theorem	caucvgsrlemcau 7879*	Lemma for caucvgsr 7888. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛)<P ((𝐺‘𝑘) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩) ∧ (𝐺‘𝑘)<P ((𝐺‘𝑛) +P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩))))
Theorem	caucvgsrlembound 7880*	Lemma for caucvgsr 7888. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑥 ∈ N ↦ (℩𝑦 ∈ P (𝐹‘𝑥) = [⟨(𝑦 +P 1P), 1P⟩] ~R ))    ⇒   ⊢ (𝜑 → ∀𝑚 ∈ N 1P<P (𝐺‘𝑚))
Theorem	caucvgsrlemgt1 7881*	Lemma for caucvgsr 7888. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑖 ∈ N (𝑗 <N 𝑖 → ((𝐹‘𝑖) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑖) +R 𝑥)))))
Theorem	caucvgsrlemoffval 7882*	Lemma for caucvgsr 7888. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ N) → ((𝐺‘𝐽) +R 𝐴) = ((𝐹‘𝐽) +R 1R))
Theorem	caucvgsrlemofff 7883*	Lemma for caucvgsr 7888. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))    ⇒   ⊢ (𝜑 → 𝐺:N⟶R)
Theorem	caucvgsrlemoffcau 7884*	Lemma for caucvgsr 7888. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐺‘𝑛) <R ((𝐺‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐺‘𝑘) <R ((𝐺‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))
Theorem	caucvgsrlemoffgt1 7885*	Lemma for caucvgsr 7888. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))    ⇒   ⊢ (𝜑 → ∀𝑚 ∈ N 1R <R (𝐺‘𝑚))
Theorem	caucvgsrlemoffres 7886*	Lemma for caucvgsr 7888. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    &   ⊢ 𝐺 = (𝑎 ∈ N ↦ (((𝐹‘𝑎) +R 1R) +R (𝐴 ·R -1R)))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))
Theorem	caucvgsrlembnd 7887*	Lemma for caucvgsr 7888. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    &   ⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))
Theorem	caucvgsr 7888*	A Cauchy sequence of signed reals with a modulus of convergence converges to a signed real. This is basically Corollary 11.2.13 of [HoTT], p. (varies). 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). This is similar to caucvgprpr 7798 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 7887). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 7883). 3. Since a signed real (element of R) which is greater than zero can be mapped to a positive real (element of P), perform that mapping on each element of the sequence and invoke caucvgprpr 7798 to get a limit (see caucvgsrlemgt1 7881). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7881). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7886). (Contributed by Jim Kingdon, 20-Jun-2021.)
⊢ (𝜑 → 𝐹:N⟶R)    &   ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <N 𝑘 → ((𝐹‘𝑛) <R ((𝐹‘𝑘) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐹‘𝑘) <R ((𝐹‘𝑛) +R [⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ R ∀𝑥 ∈ R (0R <R 𝑥 → ∃𝑗 ∈ N ∀𝑘 ∈ N (𝑗 <N 𝑘 → ((𝐹‘𝑘) <R (𝑦 +R 𝑥) ∧ 𝑦 <R ((𝐹‘𝑘) +R 𝑥)))))
Theorem	ltpsrprg 7889	Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ R) → ((𝐶 +R [⟨𝐴, 1P⟩] ~R ) <R (𝐶 +R [⟨𝐵, 1P⟩] ~R ) ↔ 𝐴<P 𝐵))
Theorem	mappsrprg 7890	Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
⊢ ((𝐴 ∈ P ∧ 𝐶 ∈ R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ))
Theorem	map2psrprg 7891*	Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
⊢ (𝐶 ∈ R → ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴))
Theorem	suplocsrlemb 7892*	Lemma for suplocsr 7895. The set 𝐵 is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   ⊢ (𝜑 → 𝐴 ⊆ R)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   ⊢ (𝜑 → ∀𝑢 ∈ P ∀𝑣 ∈ P (𝑢<P 𝑣 → (∃𝑞 ∈ 𝐵 𝑢<P 𝑞 ∨ ∀𝑞 ∈ 𝐵 𝑞<P 𝑣)))
Theorem	suplocsrlempr 7893*	Lemma for suplocsr 7895. The set 𝐵 has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.)
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   ⊢ (𝜑 → 𝐴 ⊆ R)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑣 ∈ P (∀𝑤 ∈ 𝐵 ¬ 𝑣<P 𝑤 ∧ ∀𝑤 ∈ P (𝑤<P 𝑣 → ∃𝑢 ∈ 𝐵 𝑤<P 𝑢)))
Theorem	suplocsrlem 7894*	Lemma for suplocsr 7895. The set 𝐴 has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
⊢ 𝐵 = {𝑤 ∈ P ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   ⊢ (𝜑 → 𝐴 ⊆ R)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
Theorem	suplocsr 7895*	An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.)
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ R ∀𝑦 ∈ R (𝑥 <R 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <R 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <R 𝑦)))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧)))
Syntax	cc 7896	Class of complex numbers.
class ℂ
Syntax	cr 7897	Class of real numbers.
class ℝ
Syntax	cc0 7898	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7899	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7900	Extend class notation to include the complex number i.
class i