Home Intuitionistic Logic ExplorerTheorem List (p. 77 of 130) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 7601-7700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremaxmulcl 7601 Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 7643 be used later. Instead, in most cases use mulcl 7671. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Theoremaxmulrcl 7602 Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 7644 be used later. Instead, in most cases use remulcl 7672. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

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

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

Theoremaxaddcom 7605 Addition commutes. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcom 7645 be used later. Instead, use addcom 7822.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)

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

Theoremaxmulcom 7606 Multiplication of complex numbers is commutative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 7646 be used later. Instead, use mulcom 7673. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Theoremaxaddass 7607 Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 7647 be used later. Instead, use addass 7674. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Theoremaxmulass 7608 Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 7648. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Theoremaxdistr 7609 Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 7649 be used later. Instead, use adddi 7676. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Theoremaxi2m1 7610 i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 7650. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
((i · i) + 1) = 0

Theoremax0lt1 7611 0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 7651.

The version of this axiom in the Metamath Proof Explorer reads 1 ≠ 0; here we change it to 0 < 1. The proof of 0 < 1 from 1 ≠ 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)

0 < 1

Theoremax1rid 7612 1 is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 7652. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Theoremax0id 7613 0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 7653.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)

(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Theoremaxrnegex 7614* Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 7654. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)

Theoremaxprecex 7615* Existence of positive reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 7655.

In treatments which assume excluded middle, the 0 < 𝐴 condition is generally replaced by 𝐴 ≠ 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.)

((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))

Theoremaxcnre 7616* A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 7656. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Theoremaxpre-ltirr 7617 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 7657. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)

Theoremaxpre-ltwlin 7618 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 7658. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))

Theoremaxpre-lttrn 7619 Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 7659. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremaxpre-apti 7620 Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-apti 7660.

(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)

Theoremaxpre-ltadd 7621 Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 7661. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Theoremaxpre-mulgt0 7622 The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 7662. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))

Theoremaxpre-mulext 7623 Strong extensionality of multiplication (expressed in terms of <). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 7663.

(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))

Theoremrereceu 7624* The reciprocal from axprecex 7615 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)

Theoremrecriota 7625* Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
(𝑁N → (𝑟 ∈ ℝ (⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑁, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑁, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ · 𝑟) = 1) = ⟨[⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑁, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑁, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)

Theoremaxarch 7626* Archimedean axiom. The Archimedean property is more naturally stated once we have defined . Unless we find another way to state it, we'll just use the right hand side of dfnn2 8632 in stating what we mean by "natural number" in the context of this axiom.

This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7664. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)

(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)

Theorempeano5nnnn 7627* Peano's inductive postulate. This is a counterpart to peano5nni 8633 designed for real number axioms which involve natural numbers (notably, axcaucvg 7635). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}       ((1 ∈ 𝐴 ∧ ∀𝑧𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁𝐴)

Theoremnnindnn 7628* Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8646 designed for real number axioms which involve natural numbers (notably, axcaucvg 7635). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝑧 = 1 → (𝜑𝜓))    &   (𝑧 = 𝑘 → (𝜑𝜒))    &   (𝑧 = (𝑘 + 1) → (𝜑𝜃))    &   (𝑧 = 𝐴 → (𝜑𝜏))    &   𝜓    &   (𝑘𝑁 → (𝜒𝜃))       (𝐴𝑁𝜏)

Theoremnntopi 7629* Mapping from to N. (Contributed by Jim Kingdon, 13-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}       (𝐴𝑁 → ∃𝑧N ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑧, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑧, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = 𝐴)

Theoremaxcaucvglemcl 7630* Lemma for axcaucvg 7635. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)       ((𝜑𝐽N) → (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) ∈ R)

Theoremaxcaucvglemf 7631* Lemma for axcaucvg 7635. Mapping to N and R yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))       (𝜑𝐺:NR)

Theoremaxcaucvglemval 7632* Lemma for axcaucvg 7635. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))       ((𝜑𝐽N) → (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩)

Theoremaxcaucvglemcau 7633* Lemma for axcaucvg 7635. The result of mapping to N and R satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))       (𝜑 → ∀𝑛N𝑘N (𝑛 <N 𝑘 → ((𝐺𝑛) <R ((𝐺𝑘) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ) ∧ (𝐺𝑘) <R ((𝐺𝑛) +R [⟨(⟨{𝑙𝑙 <Q (*Q‘[⟨𝑛, 1o⟩] ~Q )}, {𝑢 ∣ (*Q‘[⟨𝑛, 1o⟩] ~Q ) <Q 𝑢}⟩ +P 1P), 1P⟩] ~R ))))

Theoremaxcaucvglemres 7634* Lemma for axcaucvg 7635. Mapping the limit from N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))    &   𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))

Theoremaxcaucvg 7635* Real number completeness axiom. A Cauchy sequence with a modulus of convergence converges. This is basically Corollary 11.2.13 of [HoTT], p. (varies). The HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / 𝑛 of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis).

Because we are stating this axiom before we have introduced notations for or division, we use 𝑁 for the natural numbers and express a reciprocal in terms of .

This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 7665. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)

𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))

4.1.3  Real and complex number postulates restated as axioms

Axiomax-cnex 7636 The complex numbers form a set. Proofs should normally use cnex 7668 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
ℂ ∈ V

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

Axiomax-1cn 7638 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7596. (Contributed by NM, 1-Mar-1995.)
1 ∈ ℂ

Axiomax-1re 7639 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7597. Proofs should use 1re 7689 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
1 ∈ ℝ

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

Axiomax-addcl 7641 Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7599. Proofs should normally use addcl 7669 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 7642 Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7600. Proofs should normally use readdcl 7670 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

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

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

Axiomax-addcom 7645 Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7605. Proofs should normally use addcom 7822 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))

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

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

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

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

Axiomax-i2m1 7650 i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7610. (Contributed by NM, 29-Jan-1995.)
((i · i) + 1) = 0

Axiomax-0lt1 7651 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7611. Proofs should normally use 0lt1 7812 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
0 < 1

Axiomax-1rid 7652 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7612. (Contributed by NM, 29-Jan-1995.)
(𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Axiomax-0id 7653 0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 7613.

Proofs should normally use addid1 7823 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

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

Axiomax-precex 7655* Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7615. (Contributed by Jim Kingdon, 6-Feb-2020.)
((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ (𝐴 · 𝑥) = 1))

Axiomax-cnre 7656* A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by theorem axcnre 7616. For naming consistency, use cnre 7686 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))

Axiomax-pre-ltirr 7657 Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7657. (Contributed by Jim Kingdon, 12-Jan-2020.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)

Axiomax-pre-ltwlin 7658 Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7618. (Contributed by Jim Kingdon, 12-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))

Axiomax-pre-lttrn 7659 Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7619. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Axiomax-pre-apti 7660 Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7620. (Contributed by Jim Kingdon, 29-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)

Axiomax-pre-ltadd 7661 Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7621. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))

Axiomax-pre-mulgt0 7662 The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7622. (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))

Axiomax-pre-mulext 7663 Strong extensionality of multiplication (expressed in terms of <). Axiom for real and complex numbers, justified by theorem axpre-mulext 7623

(Contributed by Jim Kingdon, 18-Feb-2020.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))

Axiomax-arch 7664* Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 7626.

This axiom should not be used directly; instead use arch 8878 (which is the same, but stated in terms of and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)

(𝐴 ∈ ℝ → ∃𝑛 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 < 𝑛)

Axiomax-caucvg 7665* Completeness. Axiom for real and complex numbers, justified by theorem axcaucvg 7635.

A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term.

This axiom should not be used directly; instead use caucvgre 10645 (which is the same, but stated in terms of the and 1 / 𝑛 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)

𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}    &   (𝜑𝐹:𝑁⟶ℝ)    &   (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))       (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))

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

+ :(ℂ × ℂ)⟶ℂ

Axiomax-mulf 7667 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 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 ax-mulcl 7643 should be used. Note that uses of ax-mulf 7667 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 7604. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

· :(ℂ × ℂ)⟶ℂ

4.2  Derive the basic properties from the field axioms

4.2.1  Some deductions from the field axioms for complex numbers

Theoremcnex 7668 Alias for ax-cnex 7636. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℂ ∈ V

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

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

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

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

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

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

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

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

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

Theoremreex 7678 The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℝ ∈ V

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

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

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

Theorem0cn 7682 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
0 ∈ ℂ

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

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

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

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

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

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

Theorem1re 7689 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1 ∈ ℝ

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

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

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

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

𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 + 𝐵) ∈ ℂ

Theoremmulcli 7695 Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 · 𝐵) ∈ ℂ

Theoremmulcomi 7696 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 · 𝐵) = (𝐵 · 𝐴)

Theoremmulcomli 7697 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   (𝐴 · 𝐵) = 𝐶       (𝐵 · 𝐴) = 𝐶