P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	c1 7501	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7502	Extend class notation to include the complex number i.
class i
Syntax	caddc 7503	Addition on complex numbers.
class +
Syntax	cltrr 7504	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 7505	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 7506	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℂ = (R × R)
Definition	df-0 7507	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 7508	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 7509	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 7510	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ ℝ = (R × {0R})
Definition	df-add 7511*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 7512*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
Definition	df-lt 7513*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 7514	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 7515	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
Theorem	elreal 7516*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elrealeu 7517*	The real number mapping in elreal 7516 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
⊢ (𝐴 ∈ ℝ ↔ ∃!𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 7518	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1st ‘𝐴), 0R⟩))
Theorem	0ncn 7519	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. (Contributed by NM, 2-May-1996.)
⊢ ¬ ∅ ∈ ℂ
Theorem	ltrelre 7520	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 7521	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)
Theorem	mulcnsr 7522	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 7523	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)
Theorem	addresr 7524	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)
Theorem	mulresr 7525	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)
Theorem	ltresr 7526	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Theorem	ltresr2 7527	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵)))
Theorem	dfcnqs 7528	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6424, 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 7506), 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 7529	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7528 and mulcnsrec 7530. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E + [⟨𝐶, 𝐷⟩]◡ E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩]◡ E )
Theorem	mulcnsrec 7530	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6423, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7528. (Contributed by NM, 13-Aug-1995.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E · [⟨𝐶, 𝐷⟩]◡ E ) = [⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩]◡ E )
Theorem	addvalex 7531	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 7617. (Contributed by Jim Kingdon, 14-Jul-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 + 𝐵) ∈ V)
Theorem	pitonnlem1 7532*	Lemma for pitonn 7535. 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 7533	Lemma for pitonn 7535. 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 7534*	Lemma for pitonn 7535. 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 7535*	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 7536*	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 7537*	Embedding from N to ℝ. Similar to pitonn 7535 but separate in the sense that we have not proved nnssre 8582 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ (𝑁 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ ℝ)
Theorem	recnnre 7538*	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 7539*	One is an element of ℕ. This is a counterpart to 1nn 8589 designed for real number axioms which involve natural numbers (notably, axcaucvg 7585). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ 1 ∈ 𝑁
Theorem	peano2nnnn 7540*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8590 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7585). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ (𝐴 ∈ 𝑁 → (𝐴 + 1) ∈ 𝑁)
Theorem	ltrennb 7541*	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 7542*	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 7543*	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 7544	Lemma for recidpirq 7545. 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 7545*	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)
3.1.2  Final derivation of real and complex number postulates
Theorem	axcnex 7546	The complex numbers form a set. Use cnex 7616 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	axresscn 7547	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 7587. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
⊢ ℝ ⊆ ℂ
Theorem	ax1cn 7548	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 7588. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
⊢ 1 ∈ ℂ
Theorem	ax1re 7549	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 7589. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7588 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 7550	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 7590. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
⊢ i ∈ ℂ
Theorem	axaddcl 7551	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 7591 be used later. Instead, in most cases use addcl 7617. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	axaddrcl 7552	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 7592 be used later. Instead, in most cases use readdcl 7618. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	axmulcl 7553	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 7593 be used later. Instead, in most cases use mulcl 7619. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	axmulrcl 7554	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 7594 be used later. Instead, in most cases use remulcl 7620. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	axaddcom 7555	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 7595 be used later. Instead, use addcom 7770. 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 7556	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 7596 be used later. Instead, use mulcom 7621. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	axaddass 7557	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 7597 be used later. Instead, use addass 7622. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	axmulass 7558	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 7598. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	axdistr 7559	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 7599 be used later. Instead, use adddi 7624. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	axi2m1 7560	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 7600. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ ((i · i) + 1) = 0
Theorem	ax0lt1 7561	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 7601. 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 7562	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 7602. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Theorem	ax0id 7563	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 7603. 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 7564*	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 7604. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	axprecex 7565*	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 7605. 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 7566*	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 7606. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	axpre-ltirr 7567	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 7607. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <ℝ 𝐴)
Theorem	axpre-ltwlin 7568	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 7608. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵)))
Theorem	axpre-lttrn 7569	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 7609. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-apti 7570	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 7610. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵)
Theorem	axpre-ltadd 7571	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 7611. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 7572	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 7612. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-mulext 7573	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 7613. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	rereceu 7574*	The reciprocal from axprecex 7565 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 <ℝ 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Theorem	recriota 7575*	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 7576*	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 8580 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 7614. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛)
Theorem	peano5nnnn 7577*	Peano's inductive postulate. This is a counterpart to peano5nni 8581 designed for real number axioms which involve natural numbers (notably, axcaucvg 7585). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    ⇒   ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴)
Theorem	nnindnn 7578*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8594 designed for real number axioms which involve natural numbers (notably, axcaucvg 7585). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ 𝑁 → 𝜏)
Theorem	nntopi 7579*	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 7580*	Lemma for axcaucvg 7585. 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 7581*	Lemma for axcaucvg 7585. 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 7582*	Lemma for axcaucvg 7585. 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 7583*	Lemma for axcaucvg 7585. 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 7584*	Lemma for axcaucvg 7585. 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 7585*	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 7615. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝐹:𝑁⟶ℝ)    &   ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    ⇒   ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥)))))
3.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 7586	The complex numbers form a set. Proofs should normally use cnex 7616 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
⊢ ℂ ∈ V
Axiom	ax-resscn 7587	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7547. (Contributed by NM, 1-Mar-1995.)
⊢ ℝ ⊆ ℂ
Axiom	ax-1cn 7588	1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7548. (Contributed by NM, 1-Mar-1995.)
⊢ 1 ∈ ℂ
Axiom	ax-1re 7589	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7549. Proofs should use 1re 7637 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
⊢ 1 ∈ ℝ
Axiom	ax-icn 7590	i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7550. (Contributed by NM, 1-Mar-1995.)
⊢ i ∈ ℂ
Axiom	ax-addcl 7591	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7551. Proofs should normally use addcl 7617 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 7592	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7552. Proofs should normally use readdcl 7618 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Axiom	ax-mulcl 7593	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7553. Proofs should normally use mulcl 7619 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Axiom	ax-mulrcl 7594	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7554. Proofs should normally use remulcl 7620 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Axiom	ax-addcom 7595	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7555. Proofs should normally use addcom 7770 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Axiom	ax-mulcom 7596	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7556. Proofs should normally use mulcom 7621 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Axiom	ax-addass 7597	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7557. Proofs should normally use addass 7622 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 7598	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7558. Proofs should normally use mulass 7623 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 7599	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7559. Proofs should normally use adddi 7624 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 7600	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7560. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0