| Metamath
Proof Explorer Theorem List (p. 113 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ax1rid 11201 | 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 mulrid 11259, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 11225. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
| Theorem | axrnegex 11202* | 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 11226. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
| Theorem | axrrecex 11203* | 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 11227. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
| Theorem | axcnre 11204* | 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 11228. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
| Theorem | axpre-lttri 11205 | 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 11332. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 11229. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
| Theorem | axpre-lttrn 11206 | 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 11333. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 11230. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
| Theorem | axpre-ltadd 11207 | 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 11334. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 11231. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
| Theorem | axpre-mulgt0 11208 | 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 11335. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 11232. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
| Theorem | axpre-sup 11209* | 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 11336. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 11233. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
| Theorem | wuncn 11210 | 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 11211 | The complex numbers form a set. This axiom is redundant - see cnexALT 13028- but we provide this axiom because the justification theorem axcnex 11187 does not use ax-rep 5279 even though the redundancy proof does. Proofs should normally use cnex 11236 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
| ⊢ ℂ ∈ V | ||
| Axiom | ax-resscn 11212 | The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by Theorem axresscn 11188. (Contributed by NM, 1-Mar-1995.) |
| ⊢ ℝ ⊆ ℂ | ||
| Axiom | ax-1cn 11213 | 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by Theorem ax1cn 11189. (Contributed by NM, 1-Mar-1995.) |
| ⊢ 1 ∈ ℂ | ||
| Axiom | ax-icn 11214 | i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by Theorem axicn 11190. (Contributed by NM, 1-Mar-1995.) |
| ⊢ i ∈ ℂ | ||
| Axiom | ax-addcl 11215 | Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by Theorem axaddcl 11191. Proofs should normally use addcl 11237 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 11216 | Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by Theorem axaddrcl 11192. Proofs should normally use readdcl 11238 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
| Axiom | ax-mulcl 11217 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by Theorem axmulcl 11193. Proofs should normally use mulcl 11239 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
| Axiom | ax-mulrcl 11218 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by Theorem axmulrcl 11194. Proofs should normally use remulcl 11240 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
| Axiom | ax-mulcom 11219 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by Theorem axmulcom 11195. Proofs should normally use mulcom 11241 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Axiom | ax-addass 11220 | Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by Theorem axaddass 11196. Proofs should normally use addass 11242 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
| Axiom | ax-mulass 11221 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass 11197. Proofs should normally use mulass 11243 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
| Axiom | ax-distr 11222 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr 11198. Proofs should normally use adddi 11244 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
| Axiom | ax-i2m1 11223 | 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 11199. (Contributed by NM, 29-Jan-1995.) |
| ⊢ ((i · i) + 1) = 0 | ||
| Axiom | ax-1ne0 11224 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by Theorem ax1ne0 11200. (Contributed by NM, 29-Jan-1995.) |
| ⊢ 1 ≠ 0 | ||
| Axiom | ax-1rid 11225 | 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11201. Weakened from the original axiom in the form of statement in mulrid 11259, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | ||
| Axiom | ax-rnegex 11226* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex 11202. (Contributed by Eric Schmidt, 21-May-2007.) |
| ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
| Axiom | ax-rrecex 11227* | Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by Theorem axrrecex 11203. (Contributed by Eric Schmidt, 11-Apr-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1) | ||
| Axiom | ax-cnre 11228* | 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 11204. For naming consistency, use cnre 11258 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
| Axiom | ax-pre-lttri 11229 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by Theorem axpre-lttri 11205. Note: The more general version for extended reals is axlttri 11332. Normally new proofs would use xrlttri 13181. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
| Axiom | ax-pre-lttrn 11230 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by Theorem axpre-lttrn 11206. Note: The more general version for extended reals is axlttrn 11333. Normally new proofs would use lttr 11337. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
| Axiom | ax-pre-ltadd 11231 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by Theorem axpre-ltadd 11207. Normally new proofs would use axltadd 11334. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
| Axiom | ax-pre-mulgt0 11232 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by Theorem axpre-mulgt0 11208. Normally new proofs would use axmulgt0 11335. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
| Axiom | ax-pre-sup 11233* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by Theorem axpre-sup 11209. Note: Normally new proofs would use axsup 11336. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
| Axiom | ax-addf 11234 |
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-order 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 11237 should be used. Note that uses of ax-addf 11234 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 11185. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
| ⊢ + :(ℂ × ℂ)⟶ℂ | ||
| Axiom | ax-mulf 11235 |
Multiplication is an operation on the complex numbers. This axiom tells
us that · is defined only on complex
numbers which is analogous to
the way that other operations are defined, for example see subf 11510
or
eff 16117. However, while Metamath can handle this
axiom, if we wish to work
with weaker complex number axioms, we can avoid it by using the less
specific mulcl 11239. Note that uses of ax-mulf 11235 can be eliminated by using
the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of
·, as seen in mpomulf 11250.
This axiom is justified by Theorem axmulf 11186. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
| ⊢ · :(ℂ × ℂ)⟶ℂ | ||
| Theorem | cnex 11236 | Alias for ax-cnex 11211. See also cnexALT 13028. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| ⊢ ℂ ∈ V | ||
| Theorem | addcl 11237 | Alias for ax-addcl 11215, for naming consistency with addcli 11267. Use this theorem instead of ax-addcl 11215 or axaddcl 11191. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
| Theorem | readdcl 11238 | Alias for ax-addrcl 11216, for naming consistency with readdcli 11276. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
| Theorem | mulcl 11239 | Alias for ax-mulcl 11217, for naming consistency with mulcli 11268. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
| Theorem | remulcl 11240 | Alias for ax-mulrcl 11218, for naming consistency with remulcli 11277. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
| Theorem | mulcom 11241 | Alias for ax-mulcom 11219, for naming consistency with mulcomi 11269. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | addass 11242 | Alias for ax-addass 11220, for naming consistency with addassi 11271. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
| Theorem | mulass 11243 | Alias for ax-mulass 11221, for naming consistency with mulassi 11272. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
| Theorem | adddi 11244 | Alias for ax-distr 11222, for naming consistency with adddii 11273. (Contributed by NM, 10-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
| Theorem | recn 11245 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
| ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) | ||
| Theorem | reex 11246 | The real numbers form a set. See also reexALT 13026. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| ⊢ ℝ ∈ V | ||
| Theorem | reelprrecn 11247 | Reals are a subset of the pair of real and complex numbers. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ ℝ ∈ {ℝ, ℂ} | ||
| Theorem | cnelprrecn 11248 | Complex numbers are a subset of the pair of real and complex numbers . (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ ℂ ∈ {ℝ, ℂ} | ||
| Theorem | mpoaddf 11249* | Addition is an operation on complex numbers. Version of ax-addf 11234 using maps-to notation, proved from the axioms of set theory and ax-addcl 11215. (Contributed by GG, 31-Mar-2025.) |
| ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)):(ℂ × ℂ)⟶ℂ | ||
| Theorem | mpomulf 11250* | Multiplication is an operation on complex numbers. Version of ax-mulf 11235 using maps-to notation, proved from the axioms of set theory and ax-mulcl 11217. (Contributed by GG, 16-Mar-2025.) |
| ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ × ℂ)⟶ℂ | ||
| Theorem | elimne0 11251 | Hypothesis for weak deduction theorem to eliminate 𝐴 ≠ 0. (Contributed by NM, 15-May-1999.) |
| ⊢ if(𝐴 ≠ 0, 𝐴, 1) ≠ 0 | ||
| Theorem | adddir 11252 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
| Theorem | 0cn 11253 | Zero is a complex number. See also 0cnALT 11496. (Contributed by NM, 19-Feb-2005.) |
| ⊢ 0 ∈ ℂ | ||
| Theorem | 0cnd 11254 | Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (𝜑 → 0 ∈ ℂ) | ||
| Theorem | c0ex 11255 | Zero is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ 0 ∈ V | ||
| Theorem | 1cnd 11256 | One is a complex number, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ (𝜑 → 1 ∈ ℂ) | ||
| Theorem | 1ex 11257 | One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.) |
| ⊢ 1 ∈ V | ||
| Theorem | cnre 11258* | Alias for ax-cnre 11228, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
| ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
| Theorem | mulrid 11259 | The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
| Theorem | mullid 11260 | Identity law for multiplication. See mulrid 11259 for commuted version. (Contributed by NM, 8-Oct-1999.) |
| ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
| Theorem | 1re 11261 | The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11213, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
| ⊢ 1 ∈ ℝ | ||
| Theorem | 1red 11262 | The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ (𝜑 → 1 ∈ ℝ) | ||
| Theorem | 0re 11263 | The number 0 is real. Remark: the first step could also be ax-icn 11214. See also 0reALT 11606. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.) |
| ⊢ 0 ∈ ℝ | ||
| Theorem | 0red 11264 | The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
| ⊢ (𝜑 → 0 ∈ ℝ) | ||
| Theorem | mulridi 11265 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
| Theorem | mullidi 11266 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
| Theorem | addcli 11267 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
| Theorem | mulcli 11268 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
| Theorem | mulcomi 11269 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
| Theorem | mulcomli 11270 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
| Theorem | addassi 11271 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
| Theorem | mulassi 11272 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
| Theorem | adddii 11273 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) | ||
| Theorem | adddiri 11274 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)) | ||
| Theorem | recni 11275 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℂ | ||
| Theorem | readdcli 11276 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℝ | ||
| Theorem | remulcli 11277 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℝ | ||
| Theorem | mulridd 11278 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐴) | ||
| Theorem | mullidd 11279 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐴) | ||
| Theorem | addcld 11280 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) | ||
| Theorem | mulcld 11281 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | ||
| Theorem | mulcomd 11282 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | addassd 11283 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
| Theorem | mulassd 11284 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
| Theorem | adddid 11285 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
| Theorem | adddird 11286 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
| Theorem | adddirp1d 11287 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵)) | ||
| Theorem | joinlmuladdmuld 11288 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷) | ||
| Theorem | recnd 11289 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
| Theorem | readdcld 11290 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) | ||
| Theorem | remulcld 11291 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) | ||
| Syntax | cpnf 11292 | Plus infinity. |
| class +∞ | ||
| Syntax | cmnf 11293 | Minus infinity. |
| class -∞ | ||
| Syntax | cxr 11294 | The set of extended reals (includes plus and minus infinity). |
| class ℝ* | ||
| Syntax | clt 11295 | 'Less than' predicate (extended to include the extended reals). |
| class < | ||
| Syntax | cle 11296 | Extend wff notation to include the 'less than or equal to' relation. |
| class ≤ | ||
| Definition | df-pnf 11297 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that +∞ be a set not in ℝ and different from -∞
(df-mnf 11298). We use 𝒫 ∪ ℂ to make it independent of the
construction of ℂ, and Cantor's Theorem will
show that it is
different from any member of ℂ and therefore
ℝ. See pnfnre 11302,
mnfnre 11304, and pnfnemnf 11316.
A simpler possibility is to define +∞ as ℂ and -∞ as {ℂ}, but that approach requires the Axiom of Regularity to show that +∞ and -∞ are different from each other and from all members of ℝ. (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
| ⊢ +∞ = 𝒫 ∪ ℂ | ||
| Definition | df-mnf 11298 | Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -∞ be a set not in ℝ and different from +∞ (see mnfnre 11304 and pnfnemnf 11316). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
| ⊢ -∞ = 𝒫 +∞ | ||
| Definition | df-xr 11299 | Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.) |
| ⊢ ℝ* = (ℝ ∪ {+∞, -∞}) | ||
| Definition | df-ltxr 11300* | Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, <ℝ is primitive and not necessarily a relation on ℝ. (Contributed by NM, 13-Oct-2005.) |
| ⊢ < = ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |