Home | Intuitionistic Logic Explorer Theorem List (p. 78 of 135) | < 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 | axmulass 7701 | 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 7743. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 7702 | 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 7744 be used later. Instead, use adddi 7772. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 7703 | 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 7745. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax0lt1 7704 |
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 7746.
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 7705 | 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 7747. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Theorem | ax0id 7706 |
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 7748.
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 7707* | 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 7749. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | axprecex 7708* |
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 7750.
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 7709* | 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 7751. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | axpre-ltirr 7710 | 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 7752. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Theorem | axpre-ltwlin 7711 | 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 7753. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Theorem | axpre-lttrn 7712 | 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 7754. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Theorem | axpre-apti 7713 |
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 7755.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Theorem | axpre-ltadd 7714 | 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 7756. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) | ||
Theorem | axpre-mulgt0 7715 | 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 7757. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <_{ℝ} 𝐴 ∧ 0 <_{ℝ} 𝐵) → 0 <_{ℝ} (𝐴 · 𝐵))) | ||
Theorem | axpre-mulext 7716 |
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 7758.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <_{ℝ} (𝐵 · 𝐶) → (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴))) | ||
Theorem | rereceu 7717* | The reciprocal from axprecex 7708 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃!𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | recriota 7718* | 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 7719* |
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 8742 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 7759. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <_{ℝ} 𝑛) | ||
Theorem | peano5nnnn 7720* | Peano's inductive postulate. This is a counterpart to peano5nni 8743 designed for real number axioms which involve natural numbers (notably, axcaucvg 7728). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ⇒ ⊢ ((1 ∈ 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝑧 + 1) ∈ 𝐴) → 𝑁 ⊆ 𝐴) | ||
Theorem | nnindnn 7721* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8756 designed for real number axioms which involve natural numbers (notably, axcaucvg 7728). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝑧 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑧 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑧 = (𝑘 + 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑧 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑘 ∈ 𝑁 → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ 𝑁 → 𝜏) | ||
Theorem | nntopi 7722* | 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 7723* | Lemma for axcaucvg 7728. 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 7724* | Lemma for axcaucvg 7728. 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 7725* | Lemma for axcaucvg 7728. 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 7726* | Lemma for axcaucvg 7728. 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 7727* | Lemma for axcaucvg 7728. 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 7728* |
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 7760. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <_{ℝ} 𝑘 → ((𝐹‘𝑛) <_{ℝ} ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <_{ℝ} ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <_{ℝ} 𝑘 → ((𝐹‘𝑘) <_{ℝ} (𝑦 + 𝑥) ∧ 𝑦 <_{ℝ} ((𝐹‘𝑘) + 𝑥))))) | ||
Theorem | axpre-suploclemres 7729* | Lemma for axpre-suploc 7730. The result. The proof just needs to define 𝐵 as basically the same set as 𝐴 (but expressed as a subset of R rather than a subset of ℝ), and apply suplocsr 7637. (Contributed by Jim Kingdon, 24-Jan-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <_{ℝ} 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <_{ℝ} 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <_{ℝ} 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <_{ℝ} 𝑦))) & ⊢ 𝐵 = {𝑤 ∈ R ∣ ⟨𝑤, 0_{R}⟩ ∈ 𝐴} ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <_{ℝ} 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <_{ℝ} 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <_{ℝ} 𝑧))) | ||
Theorem | axpre-suploc 7730* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7761. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <_{ℝ} 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <_{ℝ} 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <_{ℝ} 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <_{ℝ} 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <_{ℝ} 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <_{ℝ} 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <_{ℝ} 𝑧))) | ||
Axiom | ax-cnex 7731 | The complex numbers form a set. Proofs should normally use cnex 7764 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 7732 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7688. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 7733 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7689. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-1re 7734 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7690. Proofs should use 1re 7785 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Axiom | ax-icn 7735 | i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7691. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 7736 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7692. Proofs should normally use addcl 7765 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 7737 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7693. Proofs should normally use readdcl 7766 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcl 7738 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7694. Proofs should normally use mulcl 7767 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-mulrcl 7739 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7695. Proofs should normally use remulcl 7768 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-addcom 7740 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7698. Proofs should normally use addcom 7919 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Axiom | ax-mulcom 7741 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7699. Proofs should normally use mulcom 7769 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-addass 7742 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7700. Proofs should normally use addass 7770 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-mulass 7743 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7701. Proofs should normally use mulass 7771 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-distr 7744 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7702. Proofs should normally use adddi 7772 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-i2m1 7745 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7703. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Axiom | ax-0lt1 7746 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7704. Proofs should normally use 0lt1 7909 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ 0 <_{ℝ} 1 | ||
Axiom | ax-1rid 7747 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7705. (Contributed by NM, 29-Jan-1995.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Axiom | ax-0id 7748 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by theorem ax0id 7706.
Proofs should normally use addid1 7920 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Axiom | ax-rnegex 7749* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7707. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Axiom | ax-precex 7750* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7708. (Contributed by Jim Kingdon, 6-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 <_{ℝ} 𝐴) → ∃𝑥 ∈ ℝ (0 <_{ℝ} 𝑥 ∧ (𝐴 · 𝑥) = 1)) | ||
Axiom | ax-cnre 7751* | 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 7709. For naming consistency, use cnre 7782 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Axiom | ax-pre-ltirr 7752 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7752. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 <_{ℝ} 𝐴) | ||
Axiom | ax-pre-ltwlin 7753 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7711. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐴 <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} 𝐵))) | ||
Axiom | ax-pre-lttrn 7754 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7712. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <_{ℝ} 𝐵 ∧ 𝐵 <_{ℝ} 𝐶) → 𝐴 <_{ℝ} 𝐶)) | ||
Axiom | ax-pre-apti 7755 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7713. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-pre-ltadd 7756 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7714. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <_{ℝ} 𝐵 → (𝐶 + 𝐴) <_{ℝ} (𝐶 + 𝐵))) | ||
Axiom | ax-pre-mulgt0 7757 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7715. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <_{ℝ} 𝐴 ∧ 0 <_{ℝ} 𝐵) → 0 <_{ℝ} (𝐴 · 𝐵))) | ||
Axiom | ax-pre-mulext 7758 |
Strong extensionality of multiplication (expressed in terms of <_{ℝ}).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7716
(Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <_{ℝ} (𝐵 · 𝐶) → (𝐴 <_{ℝ} 𝐵 ∨ 𝐵 <_{ℝ} 𝐴))) | ||
Axiom | ax-arch 7759* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7719.
This axiom should not be used directly; instead use arch 8994 (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 7760* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7728.
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 10781 (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-pre-suploc 7761* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound. Although this and ax-caucvg 7760 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7760. (Contributed by Jim Kingdon, 23-Jan-2024.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <_{ℝ} 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <_{ℝ} 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <_{ℝ} 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <_{ℝ} 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <_{ℝ} 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <_{ℝ} 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <_{ℝ} 𝑧))) | ||
Axiom | ax-addf 7762 |
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 7765 should be used. Note that uses of ax-addf 7762 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 7696. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Axiom | ax-mulf 7763 |
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 7738 should be used. Note that uses of ax-mulf 7763
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 7697. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | cnex 7764 | Alias for ax-cnex 7731. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 7765 | Alias for ax-addcl 7736, for naming consistency with addcli 7790. Use this theorem instead of ax-addcl 7736 or axaddcl 7692. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 7766 | Alias for ax-addrcl 7737, for naming consistency with readdcli 7799. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 7767 | Alias for ax-mulcl 7738, for naming consistency with mulcli 7791. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | remulcl 7768 | Alias for ax-mulrcl 7739, for naming consistency with remulcli 7800. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | mulcom 7769 | Alias for ax-mulcom 7741, for naming consistency with mulcomi 7792. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addass 7770 | Alias for ax-addass 7742, for naming consistency with addassi 7794. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulass 7771 | Alias for ax-mulass 7743, for naming consistency with mulassi 7795. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddi 7772 | Alias for ax-distr 7744, for naming consistency with adddii 7796. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | recn 7773 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) | ||
Theorem | reex 7774 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 7775 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 7776 | 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 7777 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | 0cn 7778 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 7779 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℂ) | ||
Theorem | c0ex 7780 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1ex 7781 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V | ||
Theorem | cnre 7782* | Alias for ax-cnre 7751, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | mulid1 7783 | 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2 7784 | Identity law for multiplication. Note: see mulid1 7783 for commuted version. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | 1re 7785 | 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
⊢ 1 ∈ ℝ | ||
Theorem | 0re 7786 | 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 0 ∈ ℝ | ||
Theorem | 0red 7787 | 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℝ) | ||
Theorem | mulid1i 7788 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
Theorem | mulid2i 7789 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
Theorem | addcli 7790 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
Theorem | mulcli 7791 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
Theorem | mulcomi 7792 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | mulcomli 7793 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
Theorem | addassi 7794 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | mulassi 7795 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | adddii 7796 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) | ||
Theorem | adddiri 7797 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)) | ||
Theorem | recni 7798 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | readdcli 7799 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℝ | ||
Theorem | remulcli 7800 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℝ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |