P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	caucvgsrlemasr 8101*	Lemma for caucvgsr 8113. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
⊢ (𝜑 → ∀𝑚 ∈ N 𝐴 <R (𝐹‘𝑚))    ⇒   ⊢ (𝜑 → 𝐴 ∈ R)
Theorem	caucvgsrlemfv 8102*	Lemma for caucvgsr 8113. 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 8103*	Lemma for caucvgsr 8113. 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 8104*	Lemma for caucvgsr 8113. 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 8105*	Lemma for caucvgsr 8113. 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 8106*	Lemma for caucvgsr 8113. 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 8107*	Lemma for caucvgsr 8113. 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 8108*	Lemma for caucvgsr 8113. 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 8109*	Lemma for caucvgsr 8113. 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 8110*	Lemma for caucvgsr 8113. 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 8111*	Lemma for caucvgsr 8113. 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 8112*	Lemma for caucvgsr 8113. 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 8113*	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 8023 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 8112). 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 8108). 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 8023 to get a limit (see caucvgsrlemgt1 8106). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 8106). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 8111). (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 8114	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 8115	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 8116*	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 8117*	Lemma for suplocsr 8120. 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 8118*	Lemma for suplocsr 8120. 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 8119*	Lemma for suplocsr 8120. 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 8120*	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 8121	Class of complex numbers.
class ℂ
Syntax	cr 8122	Class of real numbers.
class ℝ
Syntax	cc0 8123	Extend class notation to include the complex number 0.
class 0
Syntax	c1 8124	Extend class notation to include the complex number 1.
class 1
Syntax	ci 8125	Extend class notation to include the complex number i.
class i
Syntax	caddc 8126	Addition on complex numbers.
class +
Syntax	cltrr 8127	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 8128	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 8129	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℂ = (R × R)
Definition	df-0 8130	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 8131	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 8132	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 8133	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℝ = (R × {0R})
Definition	df-add 8134*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 8135*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
Definition	df-lt 8136*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 8137	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 8138	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
Theorem	elreal 8139*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elrealeu 8140*	The real number mapping in elreal 8139 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 8141	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1st ‘𝐴), 0R⟩))
Theorem	0ncn 8142	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 8143 which is a related property. (Contributed by NM, 2-May-1996.)
⊢ ¬ ∅ ∈ ℂ
Theorem	cnm 8143*	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 8144	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 8145	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)
Theorem	mulcnsr 8146	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 8147	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)
Theorem	addresr 8148	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)
Theorem	mulresr 8149	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)
Theorem	ltresr 8150	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Theorem	ltresr2 8151	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵)))
Theorem	dfcnqs 8152	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6833, 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 8129), 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 8153	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 8152 and mulcnsrec 8154. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E + [⟨𝐶, 𝐷⟩]◡ E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩]◡ E )
Theorem	mulcnsrec 8154	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6832, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 8152. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E · [⟨𝐶, 𝐷⟩]◡ E ) = [⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩]◡ E )
Theorem	addvalex 8155	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 8248. (Contributed by Jim Kingdon, 14-Jul-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V)
Theorem	pitonnlem1 8156*	Lemma for pitonn 8159. 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 8157	Lemma for pitonn 8159. 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 8158*	Lemma for pitonn 8159. 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 8159*	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 8160*	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 8161*	Embedding from N to ℝ. Similar to pitonn 8159 but separate in the sense that we have not proved nnssre 9237 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ℝ)
Theorem	recnnre 8162*	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 8163*	One is an element of ℕ. This is a counterpart to 1nn 9244 designed for real number axioms which involve natural numbers (notably, axcaucvg 8211). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ 1 ∈ 𝑁
Theorem	peano2nnnn 8164*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 9245 designed for real number axioms which involve to natural numbers (notably, axcaucvg 8211). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁)
Theorem	ltrennb 8165*	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 8166*	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 8167*	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 8168	Lemma for recidpirq 8169. 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 8169*	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 8170	The complex numbers form a set. Use cnex 8247 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	axresscn 8171	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 8215. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
⊢ ℝ ⊆ ℂ
Theorem	ax1cn 8172	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 8216. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
⊢ 1 ∈ ℂ
Theorem	ax1re 8173	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 8217. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 8216 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 8174	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 8218. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
⊢ i ∈ ℂ
Theorem	axaddcl 8175	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 8219 be used later. Instead, in most cases use addcl 8248. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	axaddrcl 8176	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 8220 be used later. Instead, in most cases use readdcl 8249. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	axmulcl 8177	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 8221 be used later. Instead, in most cases use mulcl 8250. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	axmulrcl 8178	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 8222 be used later. Instead, in most cases use remulcl 8251. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	axaddf 8179	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 8175. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8245. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ + :(ℂ × ℂ)⟶ℂ
Theorem	axmulf 8180	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 8246 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 8250. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ · :(ℂ × ℂ)⟶ℂ
Theorem	axaddcom 8181	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 8223 be used later. Instead, use addcom 8406. 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 8182	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 8224 be used later. Instead, use mulcom 8252. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	axaddass 8183	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 8225 be used later. Instead, use addass 8253. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	axmulass 8184	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 8226. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	axdistr 8185	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 8227 be used later. Instead, use adddi 8255. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	axi2m1 8186	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 8228. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ ((i · i) + 1) = 0
Theorem	ax0lt1 8187	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 8229. 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 8188	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 8230. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Theorem	ax0id 8189	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 8231. 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 8190*	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 8232. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	axprecex 8191*	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 8233. 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))
Theorem	axcnre 8192*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 8234. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	axpre-ltirr 8193	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 8235. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
Theorem	axpre-ltwlin 8194	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 8236. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
Theorem	axpre-lttrn 8195	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 8237. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-apti 8196	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-apti 8238. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Theorem	axpre-ltadd 8197	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 8239. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 8198	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 8240. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-mulext 8199	Strong extensionality of multiplication (expressed in terms of <ℝ). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 8241. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	rereceu 8200*	The reciprocal from axprecex 8191 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)