P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axcnre 8001*	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 8043. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	axpre-ltirr 8002	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 8044. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
Theorem	axpre-ltwlin 8003	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 8045. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
Theorem	axpre-lttrn 8004	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 8046. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-apti 8005	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 8047. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Theorem	axpre-ltadd 8006	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 8048. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 8007	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 8049. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-mulext 8008	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 8050. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	rereceu 8009*	The reciprocal from axprecex 8000 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Theorem	recriota 8010*	Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
⊢ (𝑁 ∈ N → (℩𝑟 ∈ ℝ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ · 𝑟) = 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
Theorem	axarch 8011*	Archimedean axiom. The Archimedean property is more naturally stated once we have defined ℕ. Unless we find another way to state it, we'll just use the right hand side of dfnn2 9045 in stating what we mean by "natural number" in the context of this axiom. This construction-dependent theorem should not be referenced directly; instead, use ax-arch 8051. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
Theorem	peano5nnnn 8012*	Peano's inductive postulate. This is a counterpart to peano5nni 9046 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 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴)
Theorem	nnindnn 8013*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 9059 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 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ 𝑁 → 𝜏)
Theorem	nntopi 8014*	Mapping from ℕ to N. (Contributed by Jim Kingdon, 13-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑁 → ∃𝑧 ∈ N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑧, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 𝐴)
Theorem	axcaucvglemcl 8015*	Lemma for axcaucvg 8020. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) ∈ R)
Theorem	axcaucvglemf 8016*	Lemma for axcaucvg 8020. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))    ⇒   ⊢ (𝜑 → 𝐺:N⟶R)
Theorem	axcaucvglemval 8017*	Lemma for axcaucvg 8020. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺‘𝐽), 0R⟩)
Theorem	axcaucvglemcau 8018*	Lemma for axcaucvg 8020. The result of mapping to N and R satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ 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	axcaucvglemres 8019*	Lemma for axcaucvg 8020. Mapping the limit from N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   ⊢ 𝐺 = (𝑗 ∈ N ↦ (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
Theorem	axcaucvg 8020*	Real number completeness axiom. A Cauchy sequence with a modulus of convergence converges. 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). Because we are stating this axiom before we have introduced notations for ℕ or division, we use 𝑁 for the natural numbers and express a reciprocal in terms of ℩. This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 8052. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
Theorem	axpre-suploclemres 8021*	Lemma for axpre-suploc 8022. The result. The proof just needs to define 𝐵 as basically the same set as 𝐴 (but expressed as a subset of R rather than a subset of ℝ), and apply suplocsr 7929. (Contributed by Jim Kingdon, 24-Jan-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))    &   ⊢ 𝐵 = {𝑤 ∈ R ∣ ⟨𝑤, 0R⟩ ∈ 𝐴}    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Theorem	axpre-suploc 8022*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8053. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
4.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 8023	The complex numbers form a set. Proofs should normally use cnex 8056 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
⊢ ℂ ∈ V
Axiom	ax-resscn 8024	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7980. (Contributed by NM, 1-Mar-1995.)
⊢ ℝ ⊆ ℂ
Axiom	ax-1cn 8025	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7981. (Contributed by NM, 1-Mar-1995.)
⊢ 1 ∈ ℂ
Axiom	ax-1re 8026	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7982. Proofs should use 1re 8078 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
Axiom	ax-icn 8027	i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7983. (Contributed by NM, 1-Mar-1995.)
⊢ i ∈ ℂ
Axiom	ax-addcl 8028	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7984. Proofs should normally use addcl 8057 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Axiom	ax-addrcl 8029	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7985. Proofs should normally use readdcl 8058 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Axiom	ax-mulcl 8030	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7986. Proofs should normally use mulcl 8059 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Axiom	ax-mulrcl 8031	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7987. Proofs should normally use remulcl 8060 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Axiom	ax-addcom 8032	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7990. Proofs should normally use addcom 8216 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Axiom	ax-mulcom 8033	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7991. Proofs should normally use mulcom 8061 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Axiom	ax-addass 8034	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7992. Proofs should normally use addass 8062 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 8035	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7993. Proofs should normally use mulass 8063 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 8036	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7994. Proofs should normally use adddi 8064 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 8037	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7995. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0
Axiom	ax-0lt1 8038	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7996. Proofs should normally use 0lt1 8206 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ 0 <ℝ 1
Axiom	ax-1rid 8039	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7997. (Contributed by NM, 29-Jan-1995.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Axiom	ax-0id 8040	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7998. Proofs should normally use addrid 8217 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
Axiom	ax-rnegex 8041*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7999. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Axiom	ax-precex 8042*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 8000. (Contributed by Jim Kingdon, 6-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃𝑥 ∈ ℝ (0 <ℝ 𝑥 ∧ (𝐴 · 𝑥) = 1))
Axiom	ax-cnre 8043*	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, justified by Theorem axcnre 8001. For naming consistency, use cnre 8075 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Axiom	ax-pre-ltirr 8044	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 8044. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
Axiom	ax-pre-ltwlin 8045	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 8003. (Contributed by Jim Kingdon, 12-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
Axiom	ax-pre-lttrn 8046	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 8004. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Axiom	ax-pre-apti 8047	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 8005. (Contributed by Jim Kingdon, 29-Jan-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Axiom	ax-pre-ltadd 8048	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 8006. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Axiom	ax-pre-mulgt0 8049	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 8007. (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Axiom	ax-pre-mulext 8050	Strong extensionality of multiplication (expressed in terms of <ℝ). Axiom for real and complex numbers, justified by Theorem axpre-mulext 8008 (Contributed by Jim Kingdon, 18-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Axiom	ax-arch 8051*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 8011. This axiom should not be used directly; instead use arch 9299 (which is the same, but stated in terms of ℕ and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
Axiom	ax-caucvg 8052*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 8020. A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term. This axiom should not be used directly; instead use caucvgre 11336 (which is the same, but stated in terms of the ℕ and 1 / 𝑛 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
Axiom	ax-pre-suploc 8053*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound. Although this and ax-caucvg 8052 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8052. (Contributed by Jim Kingdon, 23-Jan-2024.)
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Axiom	ax-addf 8054	Addition is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see https://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 8057 should be used. Note that uses of ax-addf 8054 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) in place of +, from which this axiom (with the defined operation in place of +) follows as a theorem. This axiom is justified by Theorem axaddf 7988. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ + :(ℂ × ℂ)⟶ℂ
Axiom	ax-mulf 8055	Multiplication is an operation on the complex numbers. This axiom tells us that · is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 8281 or eff 12018. However, while Metamath can handle this axiom, if we wish to work with weaker complex number axioms, we can avoid it by using the less specific mulcl 8059. Note that uses of ax-mulf 8055 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 8069. This axiom is justified by Theorem axmulf 7989. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ · :(ℂ × ℂ)⟶ℂ
4.2  Derive the basic properties from the field axioms
4.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 8056	Alias for ax-cnex 8023. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 8057	Alias for ax-addcl 8028, for naming consistency with addcli 8083. Use this theorem instead of ax-addcl 8028 or axaddcl 7984. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 8058	Alias for ax-addrcl 8029, for naming consistency with readdcli 8092. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 8059	Alias for ax-mulcl 8030, for naming consistency with mulcli 8084. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 8060	Alias for ax-mulrcl 8031, for naming consistency with remulcli 8093. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 8061	Alias for ax-mulcom 8033, for naming consistency with mulcomi 8085. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 8062	Alias for ax-addass 8034, for naming consistency with addassi 8087. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 8063	Alias for ax-mulass 8035, for naming consistency with mulassi 8088. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 8064	Alias for ax-distr 8036, for naming consistency with adddii 8089. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 8065	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 8066	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 8067	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 8068	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	mpomulf 8069*	Multiplication is an operation on complex numbers. Version of ax-mulf 8055 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8030. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	adddir 8070	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 8071	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 8072	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)
Theorem	c0ex 8073	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 0 ∈ V
Theorem	1ex 8074	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
⊢ 1 ∈ V
Theorem	cnre 8075*	Alias for ax-cnre 8043, for naming consistency. (Contributed by NM, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	mulrid 8076	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
Theorem	mullid 8077	Identity law for multiplication. Note: see mulrid 8076 for commuted version. (Contributed by NM, 8-Oct-1999.)
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
Theorem	1re 8078	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
⊢ 1 ∈ ℝ
Theorem	0re 8079	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
⊢ 0 ∈ ℝ
Theorem	0red 8080	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℝ)
Theorem	mulridi 8081	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 · 1) = 𝐴
Theorem	mullidi 8082	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (1 · 𝐴) = 𝐴
Theorem	addcli 8083	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℂ
Theorem	mulcli 8084	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℂ
Theorem	mulcomi 8085	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)
Theorem	mulcomli 8086	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 · 𝐵) = 𝐶    ⇒   ⊢ (𝐵 · 𝐴) = 𝐶
Theorem	addassi 8087	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Theorem	mulassi 8088	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Theorem	adddii 8089	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
Theorem	adddiri 8090	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
Theorem	recni 8091	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 𝐴 ∈ ℂ
Theorem	readdcli 8092	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 + 𝐵) ∈ ℝ
Theorem	remulcli 8093	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 · 𝐵) ∈ ℝ
Theorem	1red 8094	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℝ)
Theorem	1cnd 8095	1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
⊢ (𝜑 → 1 ∈ ℂ)
Theorem	mulridd 8096	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 1) = 𝐴)
Theorem	mullidd 8097	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	mulid2d 8098	Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1 · 𝐴) = 𝐴)
Theorem	addcld 8099	Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
Theorem	mulcld 8100	Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ)