 Home Metamath Proof ExplorerTheorem List (p. 99 of 424) < 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-27159) Hilbert Space Explorer (27160-28684) Users' Mathboxes (28685-42360)

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

Theorempn0sr 9801 A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
(𝐴R → (𝐴 +R (𝐴 ·R -1R)) = 0R)

Theoremnegexsr 9802* Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
(𝐴R → ∃𝑥R (𝐴 +R 𝑥) = 0R)

Theoremrecexsrlem 9803* The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
(0R <R 𝐴 → ∃𝑥R (𝐴 ·R 𝑥) = 1R)

Theoremaddgt0sr 9804 The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))

Theoremmulgt0sr 9805 The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵))

Theoremsqgt0sr 9806 The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
((𝐴R𝐴 ≠ 0R) → 0R <R (𝐴 ·R 𝐴))

Theoremrecexsr 9807* The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
((𝐴R𝐴 ≠ 0R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)

Theoremmappsrpr 9808 Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
𝐶R       ((𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ) ↔ 𝐴P)

Theoremltpsrpr 9809 Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
𝐶R       ((𝐶 +R [⟨𝐴, 1P⟩] ~R ) <R (𝐶 +R [⟨𝐵, 1P⟩] ~R ) ↔ 𝐴<P 𝐵)

Theoremmap2psrpr 9810* Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
𝐶R       ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥P (𝐶 +R [⟨𝑥, 1P⟩] ~R ) = 𝐴)

Theoremsupsrlem 9811* Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
𝐵 = {𝑤 ∣ (𝐶 +R [⟨𝑤, 1P⟩] ~R ) ∈ 𝐴}    &   𝐶R       ((𝐶𝐴 ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))

Theoremsupsr 9812* A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
((𝐴 ≠ ∅ ∧ ∃𝑥R𝑦𝐴 𝑦 <R 𝑥) → ∃𝑥R (∀𝑦𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦R (𝑦 <R 𝑥 → ∃𝑧𝐴 𝑦 <R 𝑧)))

Syntaxcc 9813 Class of complex numbers.
class

Syntaxcr 9814 Class of real numbers.
class

Syntaxcc0 9815 Extend class notation to include the complex number 0.
class 0

Syntaxc1 9816 Extend class notation to include the complex number 1.
class 1

Syntaxci 9817 Extend class notation to include the complex number i.
class i

class +

Syntaxcltrr 9819 'Less than' predicate (defined over real subset of complex numbers).
class <

Syntaxcmul 9820 Multiplication on complex numbers. The token · is a center dot.
class ·

Definitiondf-c 9821 Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 9848. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
ℂ = (R × R)

Definitiondf-0 9822 Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
0 = ⟨0R, 0R

Definitiondf-1 9823 Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
1 = ⟨1R, 0R

Definitiondf-i 9824 Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
i = ⟨0R, 1R

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

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

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

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

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

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

Theoremelreal2 9832 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 9833 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 9834 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
< ⊆ (ℝ × ℝ)

Theoremaddcnsr 9835 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 9836 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 9837 Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
𝐴 ∈ V       (⟨𝐴, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝐴 = 𝐵)

Theoremaddresr 9838 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 9839 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 9840 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 9841 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 9842 Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in R. The trick involves qsid 7700, 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 9821), 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 9843 Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 9842 and mulcnsrec 9844. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
(((𝐴R𝐵R) ∧ (𝐶R𝐷R)) → ([⟨𝐴, 𝐵⟩] E + [⟨𝐶, 𝐷⟩] E ) = [⟨(𝐴 +R 𝐶), (𝐵 +R 𝐷)⟩] E )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremwuncn 9870 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 9871 The complex numbers form a set. This axiom is redundant - see cnexALT 11704- but we provide this axiom because the justification theorem axcnex 9847 does not use ax-rep 4699 even though the redundancy proof does. Proofs should normally use cnex 9896 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
ℂ ∈ V

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

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

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

Axiomax-addcl 9875 Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by theorem axaddcl 9851. Proofs should normally use addcl 9897 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 9876 Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by theorem axaddrcl 9852. Proofs should normally use readdcl 9898 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Axiomax-addf 9894 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 9897 should be used. Note that uses of ax-addf 9894 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 9845. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

+ :(ℂ × ℂ)⟶ℂ

Axiomax-mulf 9895 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 9877 should be used. Note that uses of ax-mulf 9895 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 9846. (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 9896 Alias for ax-cnex 9871. See also cnexALT 11704. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℂ ∈ V

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