P. 113 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 11201-11300   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cr 11201	Class of real numbers.
class ℝ
Syntax	cc0 11202	Extend class notation to include the complex number 0.
class 0
Syntax	c1 11203	Extend class notation to include the complex number 1.
class 1
Syntax	ci 11204	Extend class notation to include the complex number i.
class i
Syntax	caddc 11205	Addition on complex numbers.
class +
Syntax	cltrr 11206	'Less than' predicate (defined over real subset of complex numbers).
class <ℝ
Syntax	cmul 11207	Multiplication on complex numbers. The token · is a center dot.
class ·
Definition	df-c 11208	Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 11235. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ ℂ = (R × R)
Definition	df-0 11209	Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ 0 = ⟨0R, 0R⟩
Definition	df-1 11210	Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ 1 = ⟨1R, 0R⟩
Definition	df-i 11211	Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ i = ⟨0R, 1R⟩
Definition	df-r 11212	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ ℝ = (R × {0R})
Definition	df-add 11213*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
⊢ + = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}
Definition	df-mul 11214*	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 11215*	Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 11350. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
Theorem	opelcn 11216	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
⊢ (⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
Theorem	opelreal 11217	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 11218*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R ⟨𝑥, 0R⟩ = 𝐴)
Theorem	elreal2 11219	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 11220	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 11221	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
⊢ <ℝ ⊆ (ℝ × ℝ)
Theorem	addcnsr 11222	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 11223	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 11224	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 11225	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 11226	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 11227	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 11228	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 11229	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 8804, 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 11208), 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 11230	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 11229 and mulcnsrec 11231. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨𝐴, 𝐵⟩]◡ E + [⟨𝐶, 𝐷⟩]◡ E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩]◡ E )
Theorem	mulcnsrec 11231	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecid 8803, which shows that the coset of the converse membership relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 11229. 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 10931. (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 11232	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 11238. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 11281. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ + :(ℂ × ℂ)⟶ℂ
Theorem	axmulf 11233	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 11282 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 11286. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
⊢ · :(ℂ × ℂ)⟶ℂ
Theorem	axcnex 11234	The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 13116), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 5231 in later theorems by invoking Axiom ax-cnex 11258 instead of cnexALT 13116. Use cnex 11283 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ ℂ ∈ V
Theorem	axresscn 11235	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 11259. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
⊢ ℝ ⊆ ℂ
Theorem	ax1cn 11236	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 11260. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
⊢ 1 ∈ ℂ
Theorem	axicn 11237	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 11261. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
⊢ i ∈ ℂ
Theorem	axaddcl 11238	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 11262 be used later. Instead, in most cases use addcl 11284. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	axaddrcl 11239	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 11263 be used later. Instead, in most cases use readdcl 11285. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	axmulcl 11240	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 11264 be used later. Instead, in most cases use mulcl 11286. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	axmulrcl 11241	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 11265 be used later. Instead, in most cases use remulcl 11287. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	axmulcom 11242	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 11266 be used later. Instead, use mulcom 11288. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	axaddass 11243	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 11267 be used later. Instead, use addass 11289. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	axmulass 11244	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 11268. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	axdistr 11245	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 11269 be used later. Instead, use adddi 11291. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	axi2m1 11246	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 11270. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
⊢ ((i · i) + 1) = 0
Theorem	ax1ne0 11247	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 11271. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.)
⊢ 1 ≠ 0
Theorem	ax1rid 11248	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 11308, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 11272. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Theorem	axrnegex 11249*	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 11273. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Theorem	axrrecex 11250*	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 11274. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Theorem	axcnre 11251*	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 11275. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Theorem	axpre-lttri 11252	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 11383. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 11276. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Theorem	axpre-lttrn 11253	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 11384. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 11277. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Theorem	axpre-ltadd 11254	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 11385. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 11278. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Theorem	axpre-mulgt0 11255	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 11386. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 11279. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Theorem	axpre-sup 11256*	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 11387. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 11280. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Theorem	wuncn 11257	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 11258	The complex numbers form a set. This axiom is redundant - see cnexALT 13116- but we provide this axiom because the justification theorem axcnex 11234 does not use ax-rep 5231 even though the redundancy proof does. Proofs should normally use cnex 11283 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
⊢ ℂ ∈ V
Axiom	ax-resscn 11259	The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 11235. (Contributed by NM, 1-Mar-1995.)
⊢ ℝ ⊆ ℂ
Axiom	ax-1cn 11260	1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by Theorem ax1cn 11236. (Contributed by NM, 1-Mar-1995.)
⊢ 1 ∈ ℂ
Axiom	ax-icn 11261	i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11237. (Contributed by NM, 1-Mar-1995.)
⊢ i ∈ ℂ
Axiom	ax-addcl 11262	Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by Theorem axaddcl 11238. Proofs should normally use addcl 11284 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 11263	Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by Theorem axaddrcl 11239. Proofs should normally use readdcl 11285 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Axiom	ax-mulcl 11264	Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by Theorem axmulcl 11240. Proofs should normally use mulcl 11286 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Axiom	ax-mulrcl 11265	Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by Theorem axmulrcl 11241. Proofs should normally use remulcl 11287 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Axiom	ax-mulcom 11266	Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by Theorem axmulcom 11242. Proofs should normally use mulcom 11288 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Axiom	ax-addass 11267	Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass 11243. Proofs should normally use addass 11289 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Axiom	ax-mulass 11268	Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass 11244. Proofs should normally use mulass 11290 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Axiom	ax-distr 11269	Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr 11245. Proofs should normally use adddi 11291 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Axiom	ax-i2m1 11270	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 11246. (Contributed by NM, 29-Jan-1995.)
⊢ ((i · i) + 1) = 0
Axiom	ax-1ne0 11271	1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11247. (Contributed by NM, 29-Jan-1995.)
⊢ 1 ≠ 0
Axiom	ax-1rid 11272	1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11248. Weakened from the original axiom in the form of statement in mulrid 11308, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Axiom	ax-rnegex 11273*	Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex 11249. (Contributed by Eric Schmidt, 21-May-2007.)
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
Axiom	ax-rrecex 11274*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex 11250. (Contributed by Eric Schmidt, 11-Apr-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Axiom	ax-cnre 11275*	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 11251. For naming consistency, use cnre 11307 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
Axiom	ax-pre-lttri 11276	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by Theorem axpre-lttri 11252. Note: The more general version for extended reals is axlttri 11383. Normally new proofs would use xrlttri 13270. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))
Axiom	ax-pre-lttrn 11277	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by Theorem axpre-lttrn 11253. Note: The more general version for extended reals is axlttrn 11384. Normally new proofs would use lttr 11388. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))
Axiom	ax-pre-ltadd 11278	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by Theorem axpre-ltadd 11254. Normally new proofs would use axltadd 11385. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))
Axiom	ax-pre-mulgt0 11279	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by Theorem axpre-mulgt0 11255. Normally new proofs would use axmulgt0 11386. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))
Axiom	ax-pre-sup 11280*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup 11256. Note: Normally new proofs would use axsup 11387. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))
Axiom	ax-addf 11281	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 11284 should be used. Note that uses of ax-addf 11281 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 11232. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
⊢ + :(ℂ × ℂ)⟶ℂ
Axiom	ax-mulf 11282	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 11561 or eff 16249. 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 11286. Note that uses of ax-mulf 11282 can be eliminated by using the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of ·, as seen in mpomulf 11297. This axiom is justified by Theorem axmulf 11233. (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 11283	Alias for ax-cnex 11258. See also cnexALT 13116. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℂ ∈ V
Theorem	addcl 11284	Alias for ax-addcl 11262, for naming consistency with addcli 11317. Use this theorem instead of ax-addcl 11262 or axaddcl 11238. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
Theorem	readdcl 11285	Alias for ax-addrcl 11263, for naming consistency with readdcli 11326. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Theorem	mulcl 11286	Alias for ax-mulcl 11264, for naming consistency with mulcli 11318. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
Theorem	remulcl 11287	Alias for ax-mulrcl 11265, for naming consistency with remulcli 11327. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Theorem	mulcom 11288	Alias for ax-mulcom 11266, for naming consistency with mulcomi 11319. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Theorem	addass 11289	Alias for ax-addass 11267, for naming consistency with addassi 11321. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	mulass 11290	Alias for ax-mulass 11268, for naming consistency with mulassi 11322. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
Theorem	adddi 11291	Alias for ax-distr 11269, for naming consistency with adddii 11323. (Contributed by NM, 10-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Theorem	recn 11292	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
Theorem	reex 11293	The real numbers form a set. See also reexALT 13114. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ℝ ∈ V
Theorem	reelprrecn 11294	Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℝ ∈ {ℝ, ℂ}
Theorem	cnelprrecn 11295	Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ℂ ∈ {ℝ, ℂ}
Theorem	mpoaddf 11296*	Addition is an operation on complex numbers. Version of ax-addf 11281 using maps-to notation, proved from the axioms of set theory and ax-addcl 11262. (Contributed by GG, 31-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	mpomulf 11297*	Multiplication is an operation on complex numbers. Version of ax-mulf 11282 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11264. (Contributed by GG, 16-Mar-2025.)
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ
Theorem	elimne0 11298	Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.)
⊢ if(𝐴 ≠ 0, 𝐴, 1) ≠ 0
Theorem	adddir 11299	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
Theorem	0cn 11300	Zero is a complex number. See also 0cnALT 11547. (Contributed by NM, 19-Feb-2005.)
⊢ 0 ∈ ℂ