Home | Intuitionistic Logic Explorer Theorem List (p. 68 of 95) | < 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 | ||
Definition | df-r 6701 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ ℝ = (R × {0_{R}}) | ||
Definition | df-add 6702* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) |
⊢ + = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨(w +_{R} u), (v +_{R} f)⟩))} | ||
Definition | df-mul 6703* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) |
⊢ · = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ ℂ ∧ y ∈ ℂ) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = ⟨((w ·_{R} u) +_{R} (-1_{R} ·_{R} (v ·_{R} f))), ((v ·_{R} u) +_{R} (w ·_{R} f))⟩))} | ||
Definition | df-lt 6704* | Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <_{ℝ} = {⟨x, y⟩ ∣ ((x ∈ ℝ ∧ y ∈ ℝ) ∧ ∃z∃w((x = ⟨z, 0_{R}⟩ ∧ y = ⟨w, 0_{R}⟩) ∧ z <_{R} w))} | ||
Theorem | opelcn 6705 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) |
⊢ (⟨A, B⟩ ∈ ℂ ↔ (A ∈ R ∧ B ∈ R)) | ||
Theorem | opelreal 6706 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ (⟨A, 0_{R}⟩ ∈ ℝ ↔ A ∈ R) | ||
Theorem | elreal 6707* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) |
⊢ (A ∈ ℝ ↔ ∃x ∈ R ⟨x, 0_{R}⟩ = A) | ||
Theorem | elreal2 6708 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
⊢ (A ∈ ℝ ↔ ((1^{st} ‘A) ∈ R ∧ A = ⟨(1^{st} ‘A), 0_{R}⟩)) | ||
Theorem | 0ncn 6709 | 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.) |
⊢ ¬ ∅ ∈ ℂ | ||
Theorem | ltrelre 6710 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
⊢ <_{ℝ} ⊆ (ℝ × ℝ) | ||
Theorem | addcnsr 6711 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨A, B⟩ + ⟨𝐶, 𝐷⟩) = ⟨(A +_{R} 𝐶), (B +_{R} 𝐷)⟩) | ||
Theorem | mulcnsr 6712 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (⟨A, B⟩ · ⟨𝐶, 𝐷⟩) = ⟨((A ·_{R} 𝐶) +_{R} (-1_{R} ·_{R} (B ·_{R} 𝐷))), ((B ·_{R} 𝐶) +_{R} (A ·_{R} 𝐷))⟩) | ||
Theorem | eqresr 6713 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ A ∈ V ⇒ ⊢ (⟨A, 0_{R}⟩ = ⟨B, 0_{R}⟩ ↔ A = B) | ||
Theorem | addresr 6714 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((A ∈ R ∧ B ∈ R) → (⟨A, 0_{R}⟩ + ⟨B, 0_{R}⟩) = ⟨(A +_{R} B), 0_{R}⟩) | ||
Theorem | mulresr 6715 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
⊢ ((A ∈ R ∧ B ∈ R) → (⟨A, 0_{R}⟩ · ⟨B, 0_{R}⟩) = ⟨(A ·_{R} B), 0_{R}⟩) | ||
Theorem | ltresr 6716 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ (⟨A, 0_{R}⟩ <_{ℝ} ⟨B, 0_{R}⟩ ↔ A <_{R} B) | ||
Theorem | ltresr2 6717 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A <_{ℝ} B ↔ (1^{st} ‘A) <_{R} (1^{st} ‘B))) | ||
Theorem | dfcnqs 6718 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 6107, 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 6697), 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.) |
⊢ ℂ = ((R × R) / ^{◡} E ) | ||
Theorem | addcnsrec 6719 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 6718 and mulcnsrec 6720. (Contributed by NM, 13-Aug-1995.) |
⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨A, B⟩]^{◡} E + [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨(A +_{R} 𝐶), (B +_{R} 𝐷)⟩]^{◡} E ) | ||
Theorem | mulcnsrec 6720 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6106, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 6718. (Contributed by NM, 13-Aug-1995.) |
⊢ (((A ∈ R ∧ B ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([⟨A, B⟩]^{◡} E · [⟨𝐶, 𝐷⟩]^{◡} E ) = [⟨((A ·_{R} 𝐶) +_{R} (-1_{R} ·_{R} (B ·_{R} 𝐷))), ((B ·_{R} 𝐶) +_{R} (A ·_{R} 𝐷))⟩]^{◡} E ) | ||
Theorem | pitonnlem1 6721* | Lemma for pitonn 6724. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨1_{𝑜}, 1_{𝑜}⟩] ~_{Q} }, {u ∣ [⟨1_{𝑜}, 1_{𝑜}⟩] ~_{Q} <_{Q} u}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ = 1 | ||
Theorem | pitonnlem1p1 6722 | Lemma for pitonn 6724. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
⊢ (A ∈ P → [⟨(A +_{P} (1_{P} +_{P} 1_{P})), (1_{P} +_{P} 1_{P})⟩] ~_{R} = [⟨(A +_{P} 1_{P}), 1_{P}⟩] ~_{R} ) | ||
Theorem | pitonnlem2 6723* | Lemma for pitonn 6724. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
⊢ (𝐾 ∈ N → (⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝐾, 1_{𝑜}⟩] ~_{Q} }, {u ∣ [⟨𝐾, 1_{𝑜}⟩] ~_{Q} <_{Q} u}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ + 1) = ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨(𝐾 +_{N} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} }, {u ∣ [⟨(𝐾 +_{N} 1_{𝑜}), 1_{𝑜}⟩] ~_{Q} <_{Q} u}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩) | ||
Theorem | pitonn 6724* | Mapping from N to ℕ. (Contributed by Jim Kingdon, 22-Apr-2020.) |
⊢ (𝑛 ∈ N → ⟨[⟨(⟨{𝑙 ∣ 𝑙 <_{Q} [⟨𝑛, 1_{𝑜}⟩] ~_{Q} }, {u ∣ [⟨𝑛, 1_{𝑜}⟩] ~_{Q} <_{Q} u}⟩ +_{P} 1_{P}), 1_{P}⟩] ~_{R} , 0_{R}⟩ ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}) | ||
Theorem | axcnex 6725 | The complex numbers form a set. Use cnex 6783 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | axresscn 6726 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 6755. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
⊢ ℝ ⊆ ℂ | ||
Theorem | ax1cn 6727 | 1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 6756. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
⊢ 1 ∈ ℂ | ||
Theorem | ax1re 6728 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 6757.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6756 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Theorem | axicn 6729 | i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 6758. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
⊢ i ∈ ℂ | ||
Theorem | axaddcl 6730 | Closure law for addition 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-addcl 6759 be used later. Instead, in most cases use addcl 6784. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) ∈ ℂ) | ||
Theorem | axaddrcl 6731 | Closure law for addition 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-addrcl 6760 be used later. Instead, in most cases use readdcl 6785. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A + B) ∈ ℝ) | ||
Theorem | axmulcl 6732 | 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 6761 be used later. Instead, in most cases use mulcl 6786. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) ∈ ℂ) | ||
Theorem | axmulrcl 6733 | 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 6762 be used later. Instead, in most cases use remulcl 6787. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A · B) ∈ ℝ) | ||
Theorem | axaddcom 6734 |
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 6763 be used later.
Instead, use addcom 6927.
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.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) = (B + A)) | ||
Theorem | axmulcom 6735 | 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 6764 be used later. Instead, use mulcom 6788. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) = (B · A)) | ||
Theorem | axaddass 6736 | 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 6765 be used later. Instead, use addass 6789. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A + B) + 𝐶) = (A + (B + 𝐶))) | ||
Theorem | axmulass 6737 | 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 6766. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶))) | ||
Theorem | axdistr 6738 | 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 6767 be used later. Instead, use adddi 6791. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))) | ||
Theorem | axi2m1 6739 | 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 6768. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax0lt1 6740 |
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 6769.
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 6741 | 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 6770. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (A ∈ ℝ → (A · 1) = A) | ||
Theorem | ax0id 6742 |
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 6771.
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.) |
⊢ (A ∈ ℂ → (A + 0) = A) | ||
Theorem | axrnegex 6743* | 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 6772. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (A ∈ ℝ → ∃x ∈ ℝ (A + x) = 0) | ||
Theorem | axprecex 6744* |
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 6773.
In treatments which assume excluded middle, the 0 <_{ℝ} A condition is generally replaced by A ≠ 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.) |
⊢ ((A ∈ ℝ ∧ 0 <_{ℝ} A) → ∃x ∈ ℝ (0 <_{ℝ} x ∧ (A · x) = 1)) | ||
Theorem | axcnre 6745* | 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 6774. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (A ∈ ℂ → ∃x ∈ ℝ ∃y ∈ ℝ A = (x + (i · y))) | ||
Theorem | axpre-ltirr 6746 | 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 6775. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ (A ∈ ℝ → ¬ A <_{ℝ} A) | ||
Theorem | axpre-ltwlin 6747 | 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 6776. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <_{ℝ} B → (A <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} B))) | ||
Theorem | axpre-lttrn 6748 | 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 6777. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((A <_{ℝ} B ∧ B <_{ℝ} 𝐶) → A <_{ℝ} 𝐶)) | ||
Theorem | axpre-apti 6749 |
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 6778.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ (A <_{ℝ} B ∨ B <_{ℝ} A)) → A = B) | ||
Theorem | axpre-ltadd 6750 | 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 6779. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <_{ℝ} B → (𝐶 + A) <_{ℝ} (𝐶 + B))) | ||
Theorem | axpre-mulgt0 6751 | 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 6780. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 <_{ℝ} A ∧ 0 <_{ℝ} B) → 0 <_{ℝ} (A · B))) | ||
Theorem | axpre-mulext 6752 |
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 6781.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((A · 𝐶) <_{ℝ} (B · 𝐶) → (A <_{ℝ} B ∨ B <_{ℝ} A))) | ||
Theorem | axarch 6753* |
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 7677 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 6782. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
⊢ (A ∈ ℝ → ∃𝑛 ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A <_{ℝ} 𝑛) | ||
Axiom | ax-cnex 6754 | The complex numbers form a set. Proofs should normally use cnex 6783 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 6755 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6726. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 6756 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6727. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-1re 6757 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6728. Proofs should use 1re 6804 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
⊢ 1 ∈ ℝ | ||
Axiom | ax-icn 6758 | i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6729. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 6759 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 6730. Proofs should normally use addcl 6784 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) ∈ ℂ) | ||
Axiom | ax-addrcl 6760 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 6731. Proofs should normally use readdcl 6785 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A + B) ∈ ℝ) | ||
Axiom | ax-mulcl 6761 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 6732. Proofs should normally use mulcl 6786 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) ∈ ℂ) | ||
Axiom | ax-mulrcl 6762 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 6733. Proofs should normally use remulcl 6787 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A · B) ∈ ℝ) | ||
Axiom | ax-addcom 6763 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6734. Proofs should normally use addcom 6927 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) = (B + A)) | ||
Axiom | ax-mulcom 6764 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 6735. Proofs should normally use mulcom 6788 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) = (B · A)) | ||
Axiom | ax-addass 6765 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 6736. Proofs should normally use addass 6789 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A + B) + 𝐶) = (A + (B + 𝐶))) | ||
Axiom | ax-mulass 6766 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 6737. Proofs should normally use mulass 6790 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶))) | ||
Axiom | ax-distr 6767 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 6738. Proofs should normally use adddi 6791 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))) | ||
Axiom | ax-i2m1 6768 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 6739. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax-0lt1 6769 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6740. Proofs should normally use 0lt1 6918 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ 0 <_{ℝ} 1 | ||
Axiom | ax-1rid 6770 | 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 6741. (Contributed by NM, 29-Jan-1995.) |
⊢ (A ∈ ℝ → (A · 1) = A) | ||
Axiom | ax-0id 6771 |
0 is an identity element for real addition. Axiom for
real and
complex numbers, justified by theorem ax0id 6742.
Proofs should normally use addid1 6928 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
⊢ (A ∈ ℂ → (A + 0) = A) | ||
Axiom | ax-rnegex 6772* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 6743. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (A ∈ ℝ → ∃x ∈ ℝ (A + x) = 0) | ||
Axiom | ax-precex 6773* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6744. (Contributed by Jim Kingdon, 6-Feb-2020.) |
⊢ ((A ∈ ℝ ∧ 0 <_{ℝ} A) → ∃x ∈ ℝ (0 <_{ℝ} x ∧ (A · x) = 1)) | ||
Axiom | ax-cnre 6774* | 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 6745. For naming consistency, use cnre 6801 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (A ∈ ℂ → ∃x ∈ ℝ ∃y ∈ ℝ A = (x + (i · y))) | ||
Axiom | ax-pre-ltirr 6775 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6775. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ (A ∈ ℝ → ¬ A <_{ℝ} A) | ||
Axiom | ax-pre-ltwlin 6776 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6747. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <_{ℝ} B → (A <_{ℝ} 𝐶 ∨ 𝐶 <_{ℝ} B))) | ||
Axiom | ax-pre-lttrn 6777 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 6748. (Contributed by NM, 13-Oct-2005.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((A <_{ℝ} B ∧ B <_{ℝ} 𝐶) → A <_{ℝ} 𝐶)) | ||
Axiom | ax-pre-apti 6778 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6749. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ (A <_{ℝ} B ∨ B <_{ℝ} A)) → A = B) | ||
Axiom | ax-pre-ltadd 6779 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 6750. (Contributed by NM, 13-Oct-2005.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → (A <_{ℝ} B → (𝐶 + A) <_{ℝ} (𝐶 + B))) | ||
Axiom | ax-pre-mulgt0 6780 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 6751. (Contributed by NM, 13-Oct-2005.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((0 <_{ℝ} A ∧ 0 <_{ℝ} B) → 0 <_{ℝ} (A · B))) | ||
Axiom | ax-pre-mulext 6781 |
Strong extensionality of multiplication (expressed in terms of <_{ℝ}).
Axiom for real and complex numbers, justified by theorem axpre-mulext 6752
(Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((A · 𝐶) <_{ℝ} (B · 𝐶) → (A <_{ℝ} B ∨ B <_{ℝ} A))) | ||
Axiom | ax-arch 6782* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 6753.
This axiom should not be used directly; instead use arch 7934 (which is the same, but stated in terms of ℕ and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
⊢ (A ∈ ℝ → ∃𝑛 ∈ ∩ {x ∣ (1 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}A <_{ℝ} 𝑛) | ||
Theorem | cnex 6783 | Alias for ax-cnex 6754. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 6784 | Alias for ax-addcl 6759, for naming consistency with addcli 6809. Use this theorem instead of ax-addcl 6759 or axaddcl 6730. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A + B) ∈ ℂ) | ||
Theorem | readdcl 6785 | Alias for ax-addrcl 6760, for naming consistency with readdcli 6818. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A + B) ∈ ℝ) | ||
Theorem | mulcl 6786 | Alias for ax-mulcl 6761, for naming consistency with mulcli 6810. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) ∈ ℂ) | ||
Theorem | remulcl 6787 | Alias for ax-mulrcl 6762, for naming consistency with remulcli 6819. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A · B) ∈ ℝ) | ||
Theorem | mulcom 6788 | Alias for ax-mulcom 6764, for naming consistency with mulcomi 6811. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → (A · B) = (B · A)) | ||
Theorem | addass 6789 | Alias for ax-addass 6765, for naming consistency with addassi 6813. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A + B) + 𝐶) = (A + (B + 𝐶))) | ||
Theorem | mulass 6790 | Alias for ax-mulass 6766, for naming consistency with mulassi 6814. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶))) | ||
Theorem | adddi 6791 | Alias for ax-distr 6767, for naming consistency with adddii 6815. (Contributed by NM, 10-Mar-2008.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))) | ||
Theorem | recn 6792 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
⊢ (A ∈ ℝ → A ∈ ℂ) | ||
Theorem | reex 6793 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 6794 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 6795 | 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 6796 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((A + B) · 𝐶) = ((A · 𝐶) + (B · 𝐶))) | ||
Theorem | 0cn 6797 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 6798 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (φ → 0 ∈ ℂ) | ||
Theorem | c0ex 6799 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1ex 6800 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |