P. 80 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulextsr1 7901	Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R ∧ 𝐶 ∈ R) → ((𝐴 ·R 𝐶) <R (𝐵 ·R 𝐶) → (𝐴 <R 𝐵 ∨ 𝐵 <R 𝐴)))
Theorem	archsr 7902*	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 7903*	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 7904	Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.)
⊢ (𝐴 ∈ P → [⟨(𝐴 +P 1P), 1P⟩] ~R ∈ R)
Theorem	prsrpos 7905	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 7906	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 7907	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 7908*	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 7909*	Lemma for caucvgsr 7922. Terms of the sequence from caucvgsrlemgt1 7915 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 7910*	Lemma for caucvgsr 7922. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → 𝐴 ∈ R)
Theorem	caucvgsrlemfv 7911*	Lemma for caucvgsr 7922. 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 7912*	Lemma for caucvgsr 7922. 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 7913*	Lemma for caucvgsr 7922. 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 7914*	Lemma for caucvgsr 7922. 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 7915*	Lemma for caucvgsr 7922. 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 7916*	Lemma for caucvgsr 7922. 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 7917*	Lemma for caucvgsr 7922. 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 7918*	Lemma for caucvgsr 7922. 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 7919*	Lemma for caucvgsr 7922. 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 7920*	Lemma for caucvgsr 7922. 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 7921*	Lemma for caucvgsr 7922. 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 7922*	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 7832 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 7921). 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 7917). 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 7832 to get a limit (see caucvgsrlemgt1 7915). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7915). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7920). (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 7923	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 7924	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 7925*	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 7926*	Lemma for suplocsr 7929. 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 7927*	Lemma for suplocsr 7929. 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 7928*	Lemma for suplocsr 7929. 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 7929*	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 7930	Class of complex numbers.
class ℂ
Syntax	cr 7931	Class of real numbers.
class ℝ
Syntax	cc0 7932	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7933	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7934	Extend class notation to include the complex number i.
class i
Syntax	caddc 7935	Addition on complex numbers.
class +
Syntax	cltrr 7936	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 7937	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 7938	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℂ = (R × R)
Definition	df-0 7939	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 7940	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 7941	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 7942	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℝ = (R × {0R})
Definition	df-add 7943*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 7944*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
Definition	df-lt 7945*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 7946	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 7947	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
Theorem	elreal 7948*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elrealeu 7949*	The real number mapping in elreal 7948 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 7950	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1st ‘𝐴), 0R⟩))
Theorem	0ncn 7951	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 7952 which is a related property. (Contributed by NM, 2-May-1996.)
⊢ ¬ ∅ ∈ ℂ
Theorem	cnm 7952*	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 7953	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 7954	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)
Theorem	mulcnsr 7955	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 7956	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)
Theorem	addresr 7957	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)
Theorem	mulresr 7958	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)
Theorem	ltresr 7959	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Theorem	ltresr2 7960	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵)))
Theorem	dfcnqs 7961	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6694, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ℂ is a quotient set, even though it is not (compare df-c 7938), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.)
⊢ ℂ = ((R × R) / ◡ E )
Theorem	addcnsrec 7962	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7961 and mulcnsrec 7963. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E + [⟨𝐶, 𝐷⟩]◡ E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩]◡ E )
Theorem	mulcnsrec 7963	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6693, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7961. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E · [⟨𝐶, 𝐷⟩]◡ E ) = [⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩]◡ E )
Theorem	addvalex 7964	Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 8057. (Contributed by Jim Kingdon, 14-Jul-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V)
Theorem	pitonnlem1 7965*	Lemma for pitonn 7968. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
⊢ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨1o, 1o⟩] ~Q }, {𝑢 ∣ [⟨1o, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 1
Theorem	pitonnlem1p1 7966	Lemma for pitonn 7968. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
⊢ (𝐴 ∈ P → [⟨(𝐴 +P (1P +P 1P)), (1P +P 1P)⟩] ~R = [⟨(𝐴 +P 1P), 1P⟩] ~R )
Theorem	pitonnlem2 7967*	Lemma for pitonn 7968. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ + 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨(𝐾 +N 1o), 1o⟩] ~Q }, {𝑢 ∣ [⟨(𝐾 +N 1o), 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
Theorem	pitonn 7968*	Mapping from N to ℕ. (Contributed by Jim Kingdon, 22-Apr-2020.)
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
Theorem	pitoregt0 7969*	Embedding from N to ℝ yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → 0 <ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
Theorem	pitore 7970*	Embedding from N to ℝ. Similar to pitonn 7968 but separate in the sense that we have not proved nnssre 9047 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ℝ)
Theorem	recnnre 7971*	Embedding the reciprocal of a natural number into ℝ. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ℝ)
Theorem	peano1nnnn 7972*	One is an element of ℕ. This is a counterpart to 1nn 9054 designed for real number axioms which involve natural numbers (notably, axcaucvg 8020). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ 1 ∈ 𝑁
Theorem	peano2nnnn 7973*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 9055 designed for real number axioms which involve to natural numbers (notably, axcaucvg 8020). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁)
Theorem	ltrennb 7974*	Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 13-Jul-2021.)
⊢ ((𝐽 ∈ N ∧ 𝐾 ∈ N) → (𝐽 <N 𝐾 ↔ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ <ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
Theorem	ltrenn 7975*	Ordering of natural numbers with <N or <ℝ. (Contributed by Jim Kingdon, 12-Jul-2021.)
⊢ (𝐽 <N 𝐾 → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ <ℝ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
Theorem	recidpipr 7976*	Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.)
⊢ (𝑁 ∈ N → (⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ ·P ⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩) = 1P)
Theorem	recidpirqlemcalc 7977	Lemma for recidpirq 7978. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ P)    &   ⊢ (𝜑 → 𝐵 ∈ P)    &   ⊢ (𝜑 → (𝐴 ·P 𝐵) = 1P)    ⇒   ⊢ (𝜑 → ((((𝐴 +P 1P) ·P (𝐵 +P 1P)) +P (1P ·P 1P)) +P 1P) = ((((𝐴 +P 1P) ·P 1P) +P (1P ·P (𝐵 +P 1P))) +P (1P +P 1P)))
Theorem	recidpirq 7978*	A real number times its reciprocal is one, where reciprocal is expressed with *Q. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ · ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = 1)
4.1.2  Final derivation of real and complex number postulates
Theorem	axcnex 7979	The complex numbers form a set. Use cnex 8056 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	axresscn 7980	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 8024. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
⊢ ℝ ⊆ ℂ
Theorem	ax1cn 7981	1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 8025. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
⊢ 1 ∈ ℂ
Theorem	ax1re 7982	1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 8026. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 8025 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
Theorem	axicn 7983	i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 8027. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
⊢ i ∈ ℂ
Theorem	axaddcl 7984	Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 8028 be used later. Instead, in most cases use addcl 8057. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	axaddrcl 7985	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 8029 be used later. Instead, in most cases use readdcl 8058. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	axmulcl 7986	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 8030 be used later. Instead, in most cases use mulcl 8059. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	axmulrcl 7987	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 8031 be used later. Instead, in most cases use remulcl 8060. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	axaddf 7988	Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl 7984. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8054. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ + :(ℂ × ℂ)⟶ℂ
Theorem	axmulf 7989	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 8055 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 8059. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ · :(ℂ × ℂ)⟶ℂ
Theorem	axaddcom 7990	Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 8032 be used later. Instead, use addcom 8216. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	axmulcom 7991	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 8033 be used later. Instead, use mulcom 8061. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	axaddass 7992	Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 8034 be used later. Instead, use addass 8062. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	axmulass 7993	Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 8035. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	axdistr 7994	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 8036 be used later. Instead, use adddi 8064. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	axi2m1 7995	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 8037. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ ((i · i) + 1) = 0
Theorem	ax0lt1 7996	0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 8038. The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 <ℝ 1. The proof of 0 <ℝ 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ 0 <ℝ 1
Theorem	ax1rid 7997	1 is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 8039. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Theorem	ax0id 7998	0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 8040. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Theorem	axrnegex 7999*	Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 8041. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	axprecex 8000*	Existence of positive reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 8042. In treatments which assume excluded middle, the 0 <ℝ 𝐴 condition is generally replaced by 𝐴 ≠ 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1))