P. 112 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11101-11200   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cc0 11101	Extend class notation to include the complex number 0.
class 0
Syntax	c1 11102	Extend class notation to include the complex number 1.
class 1
Syntax	ci 11103	Extend class notation to include the complex number i.
class i
Syntax	caddc 11104	Addition on complex numbers.
class +
Syntax	cltrr 11105	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 11106	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 11107	Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 11134. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ ℂ = (R × R)
Definition	df-0 11108	Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 11109	Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 11110	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 11111	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ ℝ = (R × {0R})
Definition	df-add 11112*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 11113*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ · = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}
Definition	df-lt 11114*	Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 11249. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 11115	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 11116	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
Theorem	elreal 11117*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 11118	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = ⟨(1st ‘𝐴), 0R⟩))
Theorem	0ncn 11119	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.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ ℂ
Theorem	ltrelre 11120	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 11121	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ + ⟨𝐶, 𝐷⟩) = ⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩)
Theorem	mulcnsr 11122	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨𝐴, 𝐵⟩ · ⟨𝐶, 𝐷⟩) = ⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩)
Theorem	eqresr 11123	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)
Theorem	addresr 11124	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ + ⟨𝐵, 0R⟩) = ⟨(𝐴 +R 𝐵), 0R⟩)
Theorem	mulresr 11125	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)
Theorem	ltresr 11126	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Theorem	ltresr2 11127	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵)))
Theorem	dfcnqs 11128	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 8780, which shows that the coset of the converse membership 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 11107), and allows 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.) (New usage is discouraged.)
⊢ ℂ = ((R × R) / ◡ E )
Theorem	addcnsrec 11129	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 11128 and mulcnsrec 11130. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E + [⟨𝐶, 𝐷⟩]◡ E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩]◡ E )
Theorem	mulcnsrec 11130	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecid 8779, which shows that the coset of the converse membership relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 11128. Note: This is the last lemma (from which the axioms will be derived) in the construction of real and complex numbers. The construction starts at cnpi 10830. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E · [⟨𝐶, 𝐷⟩]◡ E ) = [⟨((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))⟩]◡ E )
5.1.2  Final derivation of real and complex number postulates
Theorem	axaddf 11131	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 11137. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 11180. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ + :(ℂ × ℂ)⟶ℂ
Theorem	axmulf 11132	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 11181 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 11185. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ · :(ℂ × ℂ)⟶ℂ
Theorem	axcnex 11133	The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 13011), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 5239 in later theorems by invoking Axiom ax-cnex 11157 instead of cnexALT 13011. Use cnex 11182 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	axresscn 11134	The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 11158. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
⊢ ℝ ⊆ ℂ
Theorem	ax1cn 11135	1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 11159. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
⊢ 1 ∈ ℂ
Theorem	axicn 11136	i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 11160. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
⊢ i ∈ ℂ
Theorem	axaddcl 11137	Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 11161 be used later. Instead, in most cases use addcl 11183. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	axaddrcl 11138	Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 11162 be used later. Instead, in most cases use readdcl 11184. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	axmulcl 11139	Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 11163 be used later. Instead, in most cases use mulcl 11185. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	axmulrcl 11140	Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 11164 be used later. Instead, in most cases use remulcl 11186. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	axmulcom 11141	Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 11165 be used later. Instead, use mulcom 11187. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	axaddass 11142	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 9 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 11166 be used later. Instead, use addass 11188. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	axmulass 11143	Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 11167. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	axdistr 11144	Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 11168 be used later. Instead, use adddi 11190. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	axi2m1 11145	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 11169. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ ((i · i) + 1) = 0
Theorem	ax1ne0 11146	1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 11170. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.)
⊢ 1 ≠ 0
Theorem	ax1rid 11147	1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, derived from ZF set theory. Weakened from the original axiom in the form of statement in mulrid 11207, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 11171. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Theorem	axrnegex 11148*	Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 11172. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	axrrecex 11149*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex 11173. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Theorem	axcnre 11150*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 11174. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	axpre-lttri 11151	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttri 11282. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 11175. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	axpre-lttrn 11152	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttrn 11283. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 11176. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-ltadd 11153	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd 11284. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 11177. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 11154	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axmulgt0 11285. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 11178. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-sup 11155*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 11286. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 11179. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Theorem	wuncn 11156	A weak universe containing ω contains the complex number construction. This theorem is construction-dependent in the literal sense, but will also be satisfied by any other reasonable implementation of the complex numbers. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝜑 → 𝑈 ∈ WUni)    &   ⊢ (𝜑 → ω ∈ 𝑈)    ⇒   ⊢ (𝜑 → ℂ ∈ 𝑈)
5.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 11157	The complex numbers form a set. This axiom is redundant - see cnexALT 13011- but we provide this axiom because the justification theorem axcnex 11133 does not use ax-rep 5239 even though the redundancy proof does. Proofs should normally use cnex 11182 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
⊢ ℂ ∈ V
Axiom	ax-resscn 11158	The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 11134. (Contributed by NM, 1-Mar-1995.)
⊢ ℝ ⊆ ℂ
Axiom	ax-1cn 11159	1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by Theorem ax1cn 11135. (Contributed by NM, 1-Mar-1995.)
⊢ 1 ∈ ℂ
Axiom	ax-icn 11160	i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11136. (Contributed by NM, 1-Mar-1995.)
⊢ i ∈ ℂ
Axiom	ax-addcl 11161	Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by Theorem axaddcl 11137. Proofs should normally use addcl 11183 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 11162	Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by Theorem axaddrcl 11138. Proofs should normally use readdcl 11184 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Axiom	ax-mulcl 11163	Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by Theorem axmulcl 11139. Proofs should normally use mulcl 11185 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Axiom	ax-mulrcl 11164	Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by Theorem axmulrcl 11140. Proofs should normally use remulcl 11186 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Axiom	ax-mulcom 11165	Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by Theorem axmulcom 11141. Proofs should normally use mulcom 11187 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Axiom	ax-addass 11166	Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass 11142. Proofs should normally use addass 11188 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 11167	Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass 11143. Proofs should normally use mulass 11189 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 11168	Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr 11144. Proofs should normally use adddi 11190 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 11169	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by Theorem axi2m1 11145. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0
Axiom	ax-1ne0 11170	1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11146. (Contributed by NM, 29-Jan-1995.)
⊢ 1 ≠ 0
Axiom	ax-1rid 11171	1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11147. Weakened from the original axiom in the form of statement in mulrid 11207, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Axiom	ax-rnegex 11172*	Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex 11148. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Axiom	ax-rrecex 11173*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex 11149. (Contributed by Eric Schmidt, 11-Apr-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Axiom	ax-cnre 11174*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by Theorem axcnre 11150. For naming consistency, use cnre 11206 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Axiom	ax-pre-lttri 11175	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by Theorem axpre-lttri 11151. Note: The more general version for extended reals is axlttri 11282. Normally new proofs would use xrlttri 13165. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Axiom	ax-pre-lttrn 11176	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by Theorem axpre-lttrn 11152. Note: The more general version for extended reals is axlttrn 11283. Normally new proofs would use lttr 11287. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Axiom	ax-pre-ltadd 11177	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by Theorem axpre-ltadd 11153. Normally new proofs would use axltadd 11284. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Axiom	ax-pre-mulgt0 11178	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by Theorem axpre-mulgt0 11154. Normally new proofs would use axmulgt0 11285. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Axiom	ax-pre-sup 11179*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup 11155. Note: Normally new proofs would use axsup 11286. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Axiom	ax-addf 11180	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-order 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 11183 should be used. Note that uses of ax-addf 11180 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 11131. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ + :(ℂ × ℂ)⟶ℂ
Axiom	ax-mulf 11181	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 11460 or eff 16136. 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 11185. Note that uses of ax-mulf 11181 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11196. This axiom is justified by Theorem axmulf 11132. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ · :(ℂ × ℂ)⟶ℂ
5.2  Derive the basic properties from the field axioms
5.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 11182	Alias for ax-cnex 11157. See also cnexALT 13011. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 11183	Alias for ax-addcl 11161, for naming consistency with addcli 11216. Use this theorem instead of ax-addcl 11161 or axaddcl 11137. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 11184	Alias for ax-addrcl 11162, for naming consistency with readdcli 11225. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 11185	Alias for ax-mulcl 11163, for naming consistency with mulcli 11217. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 11186	Alias for ax-mulrcl 11164, for naming consistency with remulcli 11226. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 11187	Alias for ax-mulcom 11165, for naming consistency with mulcomi 11218. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 11188	Alias for ax-addass 11166, for naming consistency with addassi 11220. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 11189	Alias for ax-mulass 11167, for naming consistency with mulassi 11221. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 11190	Alias for ax-distr 11168, for naming consistency with adddii 11222. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 11191	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 11192	The real numbers form a set. See also reexALT 13009. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 11193	Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 11194	Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	mpoaddf 11195*	Addition is an operation on complex numbers. Version of ax-addf 11180 using maps-to notation, proved from the axioms of set theory and ax-addcl 11161. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	mpomulf 11196*	Multiplication is an operation on complex numbers. Version of ax-mulf 11181 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11163. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	elimne0 11197	Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.)
⊢ if(𝐴 ≠ 0, 𝐴, 1) ≠ 0
Theorem	adddir 11198	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 11199	Zero is a complex number. See also 0cnALT 11446. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ
Theorem	0cnd 11200	Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (𝜑 → 0 ∈ ℂ)