Home | Metamath
Proof Explorer Theorem List (p. 99 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pn0sr 9801 | A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ R → (𝐴 +R (𝐴 ·R -1R)) = 0R) | ||
Theorem | negexsr 9802* | Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ R → ∃𝑥 ∈ R (𝐴 +R 𝑥) = 0R) | ||
Theorem | recexsrlem 9803* | The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (0R <R 𝐴 → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R) | ||
Theorem | addgt0sr 9804 | The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵)) | ||
Theorem | mulgt0sr 9805 | The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 ·R 𝐵)) | ||
Theorem | sqgt0sr 9806 | The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → 0R <R (𝐴 ·R 𝐴)) | ||
Theorem | recexsr 9807* | The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐴 ≠ 0R) → ∃𝑥 ∈ R (𝐴 ·R 𝑥) = 1R) | ||
Theorem | mappsrpr 9808 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R -1R) <R (𝐶 +R [〈𝐴, 1P〉] ~R ) ↔ 𝐴 ∈ P) | ||
Theorem | ltpsrpr 9809 | Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R [〈𝐴, 1P〉] ~R ) <R (𝐶 +R [〈𝐵, 1P〉] ~R ) ↔ 𝐴<P 𝐵) | ||
Theorem | map2psrpr 9810* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 +R -1R) <R 𝐴 ↔ ∃𝑥 ∈ P (𝐶 +R [〈𝑥, 1P〉] ~R ) = 𝐴) | ||
Theorem | supsrlem 9811* | Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ 𝐵 = {𝑤 ∣ (𝐶 +R [〈𝑤, 1P〉] ~R ) ∈ 𝐴} & ⊢ 𝐶 ∈ R ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
Theorem | supsr 9812* | A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ R ∀𝑦 ∈ 𝐴 𝑦 <R 𝑥) → ∃𝑥 ∈ R (∀𝑦 ∈ 𝐴 ¬ 𝑥 <R 𝑦 ∧ ∀𝑦 ∈ R (𝑦 <R 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <R 𝑧))) | ||
Syntax | cc 9813 | Class of complex numbers. |
class ℂ | ||
Syntax | cr 9814 | Class of real numbers. |
class ℝ | ||
Syntax | cc0 9815 | Extend class notation to include the complex number 0. |
class 0 | ||
Syntax | c1 9816 | Extend class notation to include the complex number 1. |
class 1 | ||
Syntax | ci 9817 | Extend class notation to include the complex number i. |
class i | ||
Syntax | caddc 9818 | Addition on complex numbers. |
class + | ||
Syntax | cltrr 9819 | 'Less than' predicate (defined over real subset of complex numbers). |
class <ℝ | ||
Syntax | cmul 9820 | Multiplication on complex numbers. The token · is a center dot. |
class · | ||
Definition | df-c 9821 | Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 9848. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ ℂ = (R × R) | ||
Definition | df-0 9822 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ 0 = 〈0R, 0R〉 | ||
Definition | df-1 9823 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ 1 = 〈1R, 0R〉 | ||
Definition | df-i 9824 | Define the complex number i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ i = 〈0R, 1R〉 | ||
Definition | df-r 9825 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ ℝ = (R × {0R}) | ||
Definition | df-add 9826* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) |
⊢ + = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈(𝑤 +R 𝑢), (𝑣 +R 𝑓)〉))} | ||
Definition | df-mul 9827* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
⊢ · = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑓((𝑥 = 〈𝑤, 𝑣〉 ∧ 𝑦 = 〈𝑢, 𝑓〉) ∧ 𝑧 = 〈((𝑤 ·R 𝑢) +R (-1R ·R (𝑣 ·R 𝑓))), ((𝑣 ·R 𝑢) +R (𝑤 ·R 𝑓))〉))} | ||
Definition | df-lt 9828* | Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 9958. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ <ℝ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = 〈𝑧, 0R〉 ∧ 𝑦 = 〈𝑤, 0R〉) ∧ 𝑧 <R 𝑤))} | ||
Theorem | opelcn 9829 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
⊢ (〈𝐴, 𝐵〉 ∈ ℂ ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R)) | ||
Theorem | opelreal 9830 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ (〈𝐴, 0R〉 ∈ ℝ ↔ 𝐴 ∈ R) | ||
Theorem | elreal 9831* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ ↔ ∃𝑥 ∈ R 〈𝑥, 0R〉 = 𝐴) | ||
Theorem | elreal2 9832 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ ↔ ((1st ‘𝐴) ∈ R ∧ 𝐴 = 〈(1st ‘𝐴), 0R〉)) | ||
Theorem | 0ncn 9833 | The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ ℂ | ||
Theorem | ltrelre 9834 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ <ℝ ⊆ (ℝ × ℝ) | ||
Theorem | addcnsr 9835 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 + 〈𝐶, 𝐷〉) = 〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉) | ||
Theorem | mulcnsr 9836 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉) | ||
Theorem | eqresr 9837 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (〈𝐴, 0R〉 = 〈𝐵, 0R〉 ↔ 𝐴 = 𝐵) | ||
Theorem | addresr 9838 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 + 〈𝐵, 0R〉) = 〈(𝐴 +R 𝐵), 0R〉) | ||
Theorem | mulresr 9839 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (〈𝐴, 0R〉 · 〈𝐵, 0R〉) = 〈(𝐴 ·R 𝐵), 0R〉) | ||
Theorem | ltresr 9840 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ (〈𝐴, 0R〉 <ℝ 〈𝐵, 0R〉 ↔ 𝐴 <R 𝐵) | ||
Theorem | ltresr2 9841 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ (1st ‘𝐴) <R (1st ‘𝐵))) | ||
Theorem | dfcnqs 9842 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in ℂ from those in R. The trick involves qsid 7700, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that ℂ is a quotient set, even though it is not (compare df-c 9821), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
⊢ ℂ = ((R × R) / ◡ E ) | ||
Theorem | addcnsrec 9843 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 9842 and mulcnsrec 9844. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E + [〈𝐶, 𝐷〉]◡ E ) = [〈(𝐴 +R 𝐶), (𝐵 +R 𝐷)〉]◡ E ) | ||
Theorem | mulcnsrec 9844 |
Technical trick to permit re-use of some equivalence class lemmas for
operation laws. The trick involves ecid 7699,
which shows that the coset of
the converse epsilon relation (which is not an equivalence relation)
leaves a set unchanged. See also dfcnqs 9842.
Note: This is the last lemma (from which the axioms will be derived) in the construction of real and complex numbers. The construction starts at cnpi 9545. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) | ||
Theorem | axaddf 9845 | Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl 9851. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 9894. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Theorem | axmulf 9846 | Multiplication is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axmulcl 9853. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 9895. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | axcnex 9847 | The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 11704), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 4699 in later theorems by invoking the axiom ax-cnex 9871 instead of cnexALT 11704. Use cnex 9896 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | axresscn 9848 | The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 9872. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
⊢ ℝ ⊆ ℂ | ||
Theorem | ax1cn 9849 | 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 9873. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
⊢ 1 ∈ ℂ | ||
Theorem | axicn 9850 | i is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 9874. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
⊢ i ∈ ℂ | ||
Theorem | axaddcl 9851 | Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 9875 be used later. Instead, in most cases use addcl 9897. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | axaddrcl 9852 | Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 9876 be used later. Instead, in most cases use readdcl 9898. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | axmulcl 9853 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 9877 be used later. Instead, in most cases use mulcl 9899. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | axmulrcl 9854 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 9878 be used later. Instead, in most cases use remulcl 9900. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | axmulcom 9855 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 9879 be used later. Instead, use mulcom 9901. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | axaddass 9856 | Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom 9 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 9880 be used later. Instead, use addass 9902. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | axmulass 9857 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 9881. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | axdistr 9858 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 9882 be used later. Instead, use adddi 9904. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | axi2m1 9859 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 9883. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
⊢ ((i · i) + 1) = 0 | ||
Theorem | ax1ne0 9860 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 9884. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.) |
⊢ 1 ≠ 0 | ||
Theorem | ax1rid 9861 | 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, derived from ZF set theory. Weakened from the original axiom in the form of statement in mulid1 9916, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 9885. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Theorem | axrnegex 9862* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 9886. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | axrrecex 9863* | Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex 9887. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Theorem | axcnre 9864* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 9888. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | axpre-lttri 9865 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttri 9988. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 9889. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Theorem | axpre-lttrn 9866 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttrn 9989. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 9890. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Theorem | axpre-ltadd 9867 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd 9990. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 9891. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Theorem | axpre-mulgt0 9868 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axmulgt0 9991. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 9892. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Theorem | axpre-sup 9869* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 9992. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 9893. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Theorem | wuncn 9870 | A weak universe containing ω contains the complex number construction. This theorem is construction-dependent in the literal sense, but will also be satisfied by any other reasonable implementation of the complex numbers. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → ℂ ∈ 𝑈) | ||
Axiom | ax-cnex 9871 | The complex numbers form a set. This axiom is redundant - see cnexALT 11704- but we provide this axiom because the justification theorem axcnex 9847 does not use ax-rep 4699 even though the redundancy proof does. Proofs should normally use cnex 9896 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
⊢ ℂ ∈ V | ||
Axiom | ax-resscn 9872 | The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9848. (Contributed by NM, 1-Mar-1995.) |
⊢ ℝ ⊆ ℂ | ||
Axiom | ax-1cn 9873 | 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9849. (Contributed by NM, 1-Mar-1995.) |
⊢ 1 ∈ ℂ | ||
Axiom | ax-icn 9874 | i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9850. (Contributed by NM, 1-Mar-1995.) |
⊢ i ∈ ℂ | ||
Axiom | ax-addcl 9875 | Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by theorem axaddcl 9851. Proofs should normally use addcl 9897 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Axiom | ax-addrcl 9876 | Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by theorem axaddrcl 9852. Proofs should normally use readdcl 9898 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcl 9877 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by theorem axmulcl 9853. Proofs should normally use mulcl 9899 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Axiom | ax-mulrcl 9878 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by theorem axmulrcl 9854. Proofs should normally use remulcl 9900 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Axiom | ax-mulcom 9879 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by theorem axmulcom 9855. Proofs should normally use mulcom 9901 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Axiom | ax-addass 9880 | Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by theorem axaddass 9856. Proofs should normally use addass 9902 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Axiom | ax-mulass 9881 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9857. Proofs should normally use mulass 9903 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Axiom | ax-distr 9882 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9858. Proofs should normally use adddi 9904 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Axiom | ax-i2m1 9883 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by theorem axi2m1 9859. (Contributed by NM, 29-Jan-1995.) |
⊢ ((i · i) + 1) = 0 | ||
Axiom | ax-1ne0 9884 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9860. (Contributed by NM, 29-Jan-1995.) |
⊢ 1 ≠ 0 | ||
Axiom | ax-1rid 9885 | 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9861. Weakened from the original axiom in the form of statement in mulid1 9916, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.) |
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
Axiom | ax-rnegex 9886* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 9862. (Contributed by Eric Schmidt, 21-May-2007.) |
⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Axiom | ax-rrecex 9887* | Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by theorem axrrecex 9863. (Contributed by Eric Schmidt, 11-Apr-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
Axiom | ax-cnre 9888* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by theorem axcnre 9864. For naming consistency, use cnre 9915 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Axiom | ax-pre-lttri 9889 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri 9865. Note: The more general version for extended reals is axlttri 9988. Normally new proofs would use xrlttri 11848. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Axiom | ax-pre-lttrn 9890 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn 9866. Note: The more general version for extended reals is axlttrn 9989. Normally new proofs would use lttr 9993. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Axiom | ax-pre-ltadd 9891 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9867. Normally new proofs would use axltadd 9990. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Axiom | ax-pre-mulgt0 9892 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 9868. Normally new proofs would use axmulgt0 9991. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Axiom | ax-pre-sup 9893* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by theorem axpre-sup 9869. Note: Normally new proofs would use axsup 9992. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Axiom | ax-addf 9894 |
Addition is an operation on the complex numbers. This deprecated axiom is
provided for historical compatibility but is not a bona fide axiom for
complex numbers (independent of set theory) since it cannot be interpreted
as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific addcl 9897 should be used. Note that uses of ax-addf 9894 can
be eliminated by using the defined operation
(𝑥
∈ ℂ, 𝑦 ∈
ℂ ↦ (𝑥 + 𝑦)) in place of +, from which
this axiom (with the defined operation in place of +) follows as a
theorem.
This axiom is justified by theorem axaddf 9845. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Axiom | ax-mulf 9895 |
Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ax-mulcl 9877 should be used. Note that uses of ax-mulf 9895
can be eliminated by using the defined operation
(𝑥
∈ ℂ, 𝑦 ∈
ℂ ↦ (𝑥 ·
𝑦)) in place of
·, from which
this axiom (with the defined operation in place of ·) follows as a
theorem.
This axiom is justified by theorem axmulf 9846. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | cnex 9896 | Alias for ax-cnex 9871. See also cnexALT 11704. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 9897 | Alias for ax-addcl 9875, for naming consistency with addcli 9923. Use this theorem instead of ax-addcl 9875 or axaddcl 9851. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 9898 | Alias for ax-addrcl 9876, for naming consistency with readdcli 9932. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 9899 | Alias for ax-mulcl 9877, for naming consistency with mulcli 9924. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | remulcl 9900 | Alias for ax-mulrcl 9878, for naming consistency with remulcli 9933. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |