 Home Metamath Proof ExplorerTheorem List (p. 98 of 425) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-26947) Hilbert Space Explorer (26948-28472) Users' Mathboxes (28473-42426)

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Definitiondf-r 9701 Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
ℝ = (R × {0R})

Definitiondf-add 9702* Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
+ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨(𝑤 +R 𝑢), (𝑣 +R 𝑓)⟩))}

Definitiondf-mul 9703* Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
· = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤𝑣𝑢𝑓((𝑥 = ⟨𝑤, 𝑣⟩ ∧ 𝑦 = ⟨𝑢, 𝑓⟩) ∧ 𝑧 = ⟨((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))⟩))}

Definitiondf-lt 9704* Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 9834. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
< = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}

Theoremopelcn 9705 Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
(⟨𝐴, 𝐵⟩ ∈ ℂ ↔ (𝐴R𝐵R))

Theoremopelreal 9706 Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
(⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴R)

Theoremelreal 9707* Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
(𝐴 ∈ ℝ ↔ ∃𝑥R𝑥, 0R⟩ = 𝐴)

Theoremelreal2 9708 Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
(𝐴 ∈ ℝ ↔ ((1st𝐴) ∈ R𝐴 = ⟨(1st𝐴), 0R⟩))

Theorem0ncn 9709 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.)
¬ ∅ ∈ ℂ

Theoremltrelre 9710 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
< ⊆ (ℝ × ℝ)

Theoremaddcnsr 9711 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 𝐷)⟩)

Theoremmulcnsr 9712 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 𝐷))⟩)

Theoremeqresr 9713 Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
𝐴 ∈ V       (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)

Theoremaddresr 9714 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⟩)

Theoremmulresr 9715 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⟩)

Theoremltresr 9716 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 𝐵)

Theoremltresr2 9717 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𝐵)))

Theoremdfcnqs 9718 Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in R. The trick involves qsid 7576, 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 9697), 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.) (New usage is discouraged.)
ℂ = ((R × R) / E )

Theoremaddcnsrec 9719 Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 9718 and mulcnsrec 9720. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
(((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → ([⟨𝐴, 𝐵⟩] E + [⟨𝐶, 𝐷⟩] E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩] E )

Theoremmulcnsrec 9720 Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecid 7575, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 9718.

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 9421. (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

Theoremaxaddf 9721 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 9727. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 9770. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
+ :(ℂ × ℂ)⟶ℂ

Theoremaxmulf 9722 Multiplication 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 axmulcl 9729. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 9771. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
· :(ℂ × ℂ)⟶ℂ

Theoremaxcnex 9723 The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 11570), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 4597 in later theorems by invoking the axiom ax-cnex 9747 instead of cnexALT 11570. Use cnex 9772 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
ℂ ∈ V

Theoremaxresscn 9724 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 9748. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
ℝ ⊆ ℂ

Theoremax1cn 9725 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 9749. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
1 ∈ ℂ

Theoremaxicn 9726 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 9750. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
i ∈ ℂ

Theoremaxaddcl 9727 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 9751 be used later. Instead, in most cases use addcl 9773. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Theoremaxaddrcl 9728 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 9752 be used later. Instead, in most cases use readdcl 9774. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Theoremaxmulcl 9729 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 9753 be used later. Instead, in most cases use mulcl 9775. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Theoremaxmulrcl 9730 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 9754 be used later. Instead, in most cases use remulcl 9776. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Theoremaxmulcom 9731 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 9755 be used later. Instead, use mulcom 9777. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Theoremaxaddass 9732 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 9756 be used later. Instead, use addass 9778. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremaxmulass 9733 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 9757. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Theoremaxdistr 9734 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 9758 be used later. Instead, use adddi 9780. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Theoremaxi2m1 9735 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 9759. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
((i · i) + 1) = 0

Theoremax1ne0 9736 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 9760. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.)
1 ≠ 0

Theoremax1rid 9737 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 mulid1 9792, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 9761. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Theoremaxrnegex 9738* 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 9762. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)

Theoremaxrrecex 9739* 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 9763. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)

Theoremaxcnre 9740* 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 9764. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Theoremaxpre-lttri 9741 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 9859. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 9765. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴)))

Theoremaxpre-lttrn 9742 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 9860. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 9766. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremaxpre-ltadd 9743 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 9861. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 9767. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Theoremaxpre-mulgt0 9744 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 9862. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 9768. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))

Theoremaxpre-sup 9745* 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 9863. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 9769. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))

Theoremwuncn 9746 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

Axiomax-cnex 9747 The complex numbers form a set. This axiom is redundant - see cnexALT 11570- but we provide this axiom because the justification theorem axcnex 9723 does not use ax-rep 4597 even though the redundancy proof does. Proofs should normally use cnex 9772 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
ℂ ∈ V

Axiomax-resscn 9748 The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9724. (Contributed by NM, 1-Mar-1995.)
ℝ ⊆ ℂ

Axiomax-1cn 9749 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9725. (Contributed by NM, 1-Mar-1995.)
1 ∈ ℂ

Axiomax-icn 9750 i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9726. (Contributed by NM, 1-Mar-1995.)
i ∈ ℂ

Axiomax-addcl 9751 Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by theorem axaddcl 9727. Proofs should normally use addcl 9773 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

Axiomax-addrcl 9752 Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by theorem axaddrcl 9728. Proofs should normally use readdcl 9774 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Axiomax-mulcl 9753 Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by theorem axmulcl 9729. Proofs should normally use mulcl 9775 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Axiomax-mulrcl 9754 Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by theorem axmulrcl 9730. Proofs should normally use remulcl 9776 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Axiomax-mulcom 9755 Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by theorem axmulcom 9731. Proofs should normally use mulcom 9777 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Axiomax-addass 9756 Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by theorem axaddass 9732. Proofs should normally use addass 9778 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Axiomax-mulass 9757 Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9733. Proofs should normally use mulass 9779 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Axiomax-distr 9758 Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9734. Proofs should normally use adddi 9780 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Axiomax-i2m1 9759 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 9735. (Contributed by NM, 29-Jan-1995.)
((i · i) + 1) = 0

Axiomax-1ne0 9760 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9736. (Contributed by NM, 29-Jan-1995.)
1 ≠ 0

Axiomax-1rid 9761 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9737. Weakened from the original axiom in the form of statement in mulid1 9792, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Axiomax-rnegex 9762* Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 9738. (Contributed by Eric Schmidt, 21-May-2007.)
(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)

Axiomax-rrecex 9763* Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by theorem axrrecex 9739. (Contributed by Eric Schmidt, 11-Apr-2007.)
((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)

Axiomax-cnre 9764* 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 9740. For naming consistency, use cnre 9791 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Axiomax-pre-lttri 9765 Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri 9741. Note: The more general version for extended reals is axlttri 9859. Normally new proofs would use xrlttri 11717. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ (𝐴 = 𝐵𝐵 < 𝐴)))

Axiomax-pre-lttrn 9766 Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn 9742. Note: The more general version for extended reals is axlttrn 9860. Normally new proofs would use lttr 9864. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Axiomax-pre-ltadd 9767 Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9743. Normally new proofs would use axltadd 9861. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Axiomax-pre-mulgt0 9768 The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 9744. Normally new proofs would use axmulgt0 9862. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))

Axiomax-pre-sup 9769* A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by theorem axpre-sup 9745. Note: Normally new proofs would use axsup 9863. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))

Axiomax-addf 9770 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 http://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 9773 should be used. Note that uses of ax-addf 9770 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 9721. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

+ :(ℂ × ℂ)⟶ℂ

Axiomax-mulf 9771 Multiplication 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 http://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 ax-mulcl 9753 should be used. Note that uses of ax-mulf 9771 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 axmulf 9722. (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

Theoremcnex 9772 Alias for ax-cnex 9747. See also cnexALT 11570. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℂ ∈ V

((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Theoremmulcl 9775 Alias for ax-mulcl 9753, for naming consistency with mulcli 9800. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Theoremremulcl 9776 Alias for ax-mulrcl 9754, for naming consistency with remulcli 9809. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Theoremmulcom 9777 Alias for ax-mulcom 9755, for naming consistency with mulcomi 9801. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremmulass 9779 Alias for ax-mulass 9757, for naming consistency with mulassi 9804. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Theoremadddi 9780 Alias for ax-distr 9758, for naming consistency with adddii 9805. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Theoremrecn 9781 A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
(𝐴 ∈ ℝ → 𝐴 ∈ ℂ)

Theoremreex 9782 The real numbers form a set. See also reexALT 11568. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℝ ∈ V

Theoremreelprrecn 9783 Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
ℝ ∈ {ℝ, ℂ}

Theoremcnelprrecn 9784 Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
ℂ ∈ {ℝ, ℂ}

Theoremelimne0 9785 Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.)
if(𝐴 ≠ 0, 𝐴, 1) ≠ 0

Theoremadddir 9786 Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))

Theorem0cn 9787 0 is a complex number. See also 0cnALT 10021. (Contributed by NM, 19-Feb-2005.)
0 ∈ ℂ

Theorem0cnd 9788 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
(𝜑 → 0 ∈ ℂ)

Theoremc0ex 9789 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
0 ∈ V

Theorem1ex 9790 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
1 ∈ V

Theoremcnre 9791* Alias for ax-cnre 9764, for naming consistency. (Contributed by NM, 3-Jan-2013.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Theoremmulid1 9792 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
(𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)

Theoremmulid2 9793 Identity law for multiplication. Note: see mulid1 9792 for commuted version. (Contributed by NM, 8-Oct-1999.)
(𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)

Theorem1re 9794 1 is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 9749, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
1 ∈ ℝ

Theorem0re 9795 0 is a real number. See also 0reALT 10129. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
0 ∈ ℝ

Theorem0red 9796 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
(𝜑 → 0 ∈ ℝ)

Theoremmulid1i 9797 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ ℂ       (𝐴 · 1) = 𝐴

Theoremmulid2i 9798 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ ℂ       (1 · 𝐴) = 𝐴