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