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	mulcmpblnr 7801	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 7802*	Decomposing signed reals into positive reals. Lemma for addsrpr 7805 and mulsrpr 7806. (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 7803*	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 7804*	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 7805	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 7806	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 7807	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 7808	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
⊢ (0R <R [⟨𝐴, 𝐵⟩] ~R ↔ 𝐵<P 𝐴)
Theorem	0nsr 7809	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
⊢ ¬ ∅ ∈ R
Theorem	0r 7810	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 0R ∈ R
Theorem	1sr 7811	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ 1R ∈ R
Theorem	m1r 7812	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
⊢ -1R ∈ R
Theorem	addclsr 7813	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) ∈ R)
Theorem	mulclsr 7814	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R)
Theorem	addcomsrg 7815	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 +R 𝐵) = (𝐵 +R 𝐴))
Theorem	addasssrg 7816	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 +R 𝐵) +R 𝐶) = (𝐴 +R (𝐵 +R 𝐶)))
Theorem	mulcomsrg 7817	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) = (𝐵 ·R 𝐴))
Theorem	mulasssrg 7818	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐵) ·R 𝐶) = (𝐴 ·R (𝐵 ·R 𝐶)))
Theorem	distrsrg 7819	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → (𝐴 ·R (𝐵 +R 𝐶)) = ((𝐴 ·R 𝐵) +R (𝐴 ·R 𝐶)))
Theorem	m1p1sr 7820	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.)
⊢ (-1R +R 1R) = 0R
Theorem	m1m1sr 7821	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.)
⊢ (-1R ·R -1R) = 1R
Theorem	lttrsr 7822*	Signed real 'less than' is a transitive relation. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ ((𝑓 ∈ R ∧ 𝑔 ∈ R ∧ ℎ ∈ R) → ((𝑓 <R 𝑔 ∧ 𝑔 <R ℎ) → 𝑓 <R ℎ))
Theorem	ltposr 7823	Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
⊢ <R Po R
Theorem	ltsosr 7824	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.)
⊢ <R Or R
Theorem	0lt1sr 7825	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.)
⊢ 0R <R 1R
Theorem	1ne0sr 7826	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.)
⊢ ¬ 1R = 0R
Theorem	0idsr 7827	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 7828	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
⊢ (𝐴 ∈ R → (𝐴 ·R 1R) = 𝐴)
Theorem	00sr 7829	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
⊢ (𝐴 ∈ R → (𝐴 ·R 0R) = 0R)
Theorem	ltasrg 7830	Ordering property of addition. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → (𝐴 <R 𝐵 ↔ (𝐶 +R 𝐴) <R (𝐶 +R 𝐵)))
Theorem	pn0sr 7831	A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.)
⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R)
Theorem	negexsr 7832*	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 7833*	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 7834*	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 7835	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))
Theorem	ltadd1sr 7836	Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.)
⊢ (𝐴 ∈ R → 𝐴 <R (𝐴 +R 1R))
Theorem	ltm1sr 7837	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 7838	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.)
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵))
Theorem	aptisr 7839	Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ ¬ (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴)) → 𝐴 = 𝐵)
Theorem	mulextsr1lem 7840	Lemma for mulextsr1 7841. (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 7841	Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐶) <R (𝐵 ·R 𝐶) → (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴)))
Theorem	archsr 7842*	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 7843*	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 7844	Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ (𝐴 ∈ P → [⟨(𝐴 +P 1P), 1P⟩] ~R ∈ R)
Theorem	prsrpos 7845	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 7846	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 7847	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 7848*	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 7849*	Lemma for caucvgsr 7862. Terms of the sequence from caucvgsrlemgt1 7855 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 7850*	Lemma for caucvgsr 7862. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → 𝐴 ∈ R)
Theorem	caucvgsrlemfv 7851*	Lemma for caucvgsr 7862. 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 7852*	Lemma for caucvgsr 7862. 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 7853*	Lemma for caucvgsr 7862. 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 7854*	Lemma for caucvgsr 7862. 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 7855*	Lemma for caucvgsr 7862. 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 7856*	Lemma for caucvgsr 7862. 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 7857*	Lemma for caucvgsr 7862. 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 7858*	Lemma for caucvgsr 7862. 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 7859*	Lemma for caucvgsr 7862. 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 7860*	Lemma for caucvgsr 7862. 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 7861*	Lemma for caucvgsr 7862. 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 7862*	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 7772 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 7861). 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 7857). 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 7772 to get a limit (see caucvgsrlemgt1 7855). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7855). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7860). (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 7863	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 7864	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 7865*	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 7866*	Lemma for suplocsr 7869. 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 7867*	Lemma for suplocsr 7869. 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 7868*	Lemma for suplocsr 7869. 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 7869*	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 7870	Class of complex numbers.
class ℂ
Syntax	cr 7871	Class of real numbers.
class ℝ
Syntax	cc0 7872	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7873	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7874	Extend class notation to include the complex number i.
class i
Syntax	caddc 7875	Addition on complex numbers.
class +
Syntax	cltrr 7876	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 7877	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 7878	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℂ = (R × R)
Definition	df-0 7879	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 7880	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 7881	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 7882	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℝ = (R × {0R})
Definition	df-add 7883*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 7884*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
Definition	df-lt 7885*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 7886	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 7887	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
Theorem	elreal 7888*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elrealeu 7889*	The real number mapping in elreal 7888 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 7890	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1st ‘𝐴), 0R⟩))
Theorem	0ncn 7891	The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. See also cnm 7892 which is a related property. (Contributed by NM, 2-May-1996.)
⊢ ¬ ∅ ∈ ℂ
Theorem	cnm 7892*	A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 𝑥 ∈ 𝐴)
Theorem	ltrelre 7893	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 7894	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)
Theorem	mulcnsr 7895	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ · ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)
Theorem	eqresr 7896	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)
Theorem	addresr 7897	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)
Theorem	mulresr 7898	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)
Theorem	ltresr 7899	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Theorem	ltresr2 7900	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵)))