Home | Intuitionistic Logic Explorer Theorem 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axmulcl 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | axmulrcl 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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | axaddf 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.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Theorem | axmulf 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.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | axaddcom 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | axmulcom 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | axaddass 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | axmulass 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 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 | ||
Theorem | ax0lt1 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 | ||
Theorem | ax1rid 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) = 𝐴) | ||
Theorem | ax0id 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) = 𝐴) | ||
Theorem | axrnegex 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) | ||
Theorem | axprecex 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)) | ||
Theorem | axcnre 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 · 𝑦))) | ||
Theorem | axpre-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.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Theorem | axpre-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Theorem | axpre-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Theorem | axpre-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | axpre-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) | ||
Theorem | axpre-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 <_{ℝ} (𝐴 · 𝐵))) | ||
Theorem | axpre-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <_{ℝ} (𝐵 · 𝐶) → (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴))) | ||
Theorem | rereceu 7624* | The reciprocal from axprecex 7615 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | recriota 7625* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
⊢ (𝑁 ∈ N → (℩𝑟 ∈ ℝ (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑁, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑁, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ · 𝑟) = 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑁, 1_{o}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑁, 1_{o}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | axarch 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) ∈ 𝑥)}𝐴 <_{ℝ} 𝑛) | ||
Theorem | peano5nnnn 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) ∈ 𝐴) → 𝑁 ⊆ 𝐴) | ||
Theorem | nnindnn 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) → (𝜑 ↔ 𝜃)) & ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ 𝑁 → 𝜏) | ||
Theorem | nntopi 7629* | Mapping from ℕ to N. (Contributed by Jim Kingdon, 13-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑁 → ∃𝑧 ∈ N ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑧, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑧, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ = 𝐴) | ||
Theorem | axcaucvglemcl 7630* | Lemma for axcaucvg 7635. Mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (℩𝑧 ∈ R (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩) ∈ R) | ||
Theorem | axcaucvglemf 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} [⟨𝑗, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → 𝐺:N⟶R) | ||
Theorem | axcaucvglemval 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} [⟨𝑗, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ N) → (𝐹‘⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐽, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝐽, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨(𝐺‘𝐽), 0_{R}⟩) | ||
Theorem | axcaucvglemcau 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} [⟨𝑗, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ N ∀𝑘 ∈ N (𝑛 <_{N} 𝑘 → ((𝐺‘𝑛) <_{R} ((𝐺‘𝑘) +_{R} [⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑛, 1_{o}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑛, 1_{o}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} ) ∧ (𝐺‘𝑘) <_{R} ((𝐺‘𝑛) +_{R} [⟨(⟨{𝑙 ∣ 𝑙 <_{Q} (*_{Q}‘[⟨𝑛, 1_{o}⟩] ~_{Q} )}, {𝑢 ∣ (*_{Q}‘[⟨𝑛, 1_{o}⟩] ~_{Q} ) <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} )))) | ||
Theorem | axcaucvglemres 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} [⟨𝑗, 1_{o}⟩] ~_{Q} }, {𝑢 ∣ [⟨𝑗, 1_{o}⟩] ~_{Q} <_{Q} 𝑢}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) = ⟨𝑧, 0_{R}⟩)) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | axcaucvg 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 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Axiom | ax-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 | ||
Axiom | ax-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.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-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 ∈ ℂ | ||
Axiom | ax-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 ∈ ℝ | ||
Axiom | ax-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 ∈ ℂ | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-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 | ||
Axiom | ax-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 | ||
Axiom | ax-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) = 𝐴) | ||
Axiom | ax-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) = 𝐴) | ||
Axiom | ax-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) | ||
Axiom | ax-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)) | ||
Axiom | ax-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 · 𝑦))) | ||
Axiom | ax-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.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) | ||
Axiom | ax-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 <_{ℝ} (𝐴 · 𝐵))) | ||
Axiom | ax-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.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <_{ℝ} (𝐵 · 𝐶) → (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴))) | ||
Axiom | ax-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) ∈ 𝑥)}𝐴 <_{ℝ} 𝑛) | ||
Axiom | ax-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 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Axiom | ax-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.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Axiom | ax-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.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | cnex 7668 | Alias for ax-cnex 7636. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 7669 | Alias for ax-addcl 7641, for naming consistency with addcli 7694. Use this theorem instead of ax-addcl 7641 or axaddcl 7599. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 7670 | Alias for ax-addrcl 7642, for naming consistency with readdcli 7703. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 7671 | Alias for ax-mulcl 7643, for naming consistency with mulcli 7695. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | remulcl 7672 | Alias for ax-mulrcl 7644, for naming consistency with remulcli 7704. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | mulcom 7673 | Alias for ax-mulcom 7646, for naming consistency with mulcomi 7696. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addass 7674 | Alias for ax-addass 7647, for naming consistency with addassi 7698. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulass 7675 | Alias for ax-mulass 7648, for naming consistency with mulassi 7699. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddi 7676 | Alias for ax-distr 7649, for naming consistency with adddii 7700. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | recn 7677 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) | ||
Theorem | reex 7678 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 7679 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 7680 | Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℂ ∈ {ℝ, ℂ} | ||
Theorem | adddir 7681 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | 0cn 7682 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 7683 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℂ) | ||
Theorem | c0ex 7684 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1ex 7685 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V | ||
Theorem | cnre 7686* | Alias for ax-cnre 7656, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | mulid1 7687 | 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2 7688 | Identity law for multiplication. Note: see mulid1 7687 for commuted version. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | 1re 7689 | 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
⊢ 1 ∈ ℝ | ||
Theorem | 0re 7690 | 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 0 ∈ ℝ | ||
Theorem | 0red 7691 | 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℝ) | ||
Theorem | mulid1i 7692 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
Theorem | mulid2i 7693 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
Theorem | addcli 7694 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
Theorem | mulcli 7695 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
Theorem | mulcomi 7696 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | mulcomli 7697 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
Theorem | addassi 7698 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | mulassi 7699 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | adddii 7700 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |