Home | Intuitionistic Logic Explorer Theorem List (p. 78 of 132) | < 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 | ||
Axiom | ax-pre-ltwlin 7701 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7659. (Contributed by Jim Kingdon, 12-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐴 <ℝ 𝐶 ∨ 𝐶 <ℝ 𝐵))) | ||
Axiom | ax-pre-lttrn 7702 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7660. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶)) | ||
Axiom | ax-pre-apti 7703 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7661. (Contributed by Jim Kingdon, 29-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴)) → 𝐴 = 𝐵) | ||
Axiom | ax-pre-ltadd 7704 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7662. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵))) | ||
Axiom | ax-pre-mulgt0 7705 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7663. (Contributed by NM, 13-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵))) | ||
Axiom | ax-pre-mulext 7706 |
Strong extensionality of multiplication (expressed in terms of <ℝ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7664
(Contributed by Jim Kingdon, 18-Feb-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) <ℝ (𝐵 · 𝐶) → (𝐴 <ℝ 𝐵 ∨ 𝐵 <ℝ 𝐴))) | ||
Axiom | ax-arch 7707* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7667.
This axiom should not be used directly; instead use arch 8932 (which is the same, but stated in terms of ℕ and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴 <ℝ 𝑛) | ||
Axiom | ax-caucvg 7708* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7676.
A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / 𝑛 of the nth term. This axiom should not be used directly; instead use caucvgre 10708 (which is the same, but stated in terms of the ℕ and 1 / 𝑛 notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
⊢ 𝑁 = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} & ⊢ (𝜑 → 𝐹:𝑁⟶ℝ) & ⊢ (𝜑 → ∀𝑛 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑛 <ℝ 𝑘 → ((𝐹‘𝑛) <ℝ ((𝐹‘𝑘) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹‘𝑘) <ℝ ((𝐹‘𝑛) + (℩𝑟 ∈ ℝ (𝑛 · 𝑟) = 1))))) ⇒ ⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ (0 <ℝ 𝑥 → ∃𝑗 ∈ 𝑁 ∀𝑘 ∈ 𝑁 (𝑗 <ℝ 𝑘 → ((𝐹‘𝑘) <ℝ (𝑦 + 𝑥) ∧ 𝑦 <ℝ ((𝐹‘𝑘) + 𝑥))))) | ||
Axiom | ax-pre-suploc 7709* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given 𝑥 < 𝑦, either there is an element of the set greater than 𝑥, or 𝑦 is an upper bound. Although this and ax-caucvg 7708 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7708. (Contributed by Jim Kingdon, 23-Jan-2024.) |
⊢ (((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥 ∈ 𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 <ℝ 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 <ℝ 𝑦 → (∃𝑧 ∈ 𝐴 𝑥 <ℝ 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧 <ℝ 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧))) | ||
Axiom | ax-addf 7710 |
Addition is an operation on the complex numbers. This deprecated axiom is
provided for historical compatibility but is not a bona fide axiom for
complex numbers (independent of set theory) since it cannot be interpreted
as a first- or second-order statement (see
https://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific addcl 7713 should be used. Note that uses of ax-addf 7710 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 7644. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ + :(ℂ × ℂ)⟶ℂ | ||
Axiom | ax-mulf 7711 |
Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
https://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ax-mulcl 7686 should be used. Note that uses of ax-mulf 7711
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 7645. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
⊢ · :(ℂ × ℂ)⟶ℂ | ||
Theorem | cnex 7712 | Alias for ax-cnex 7679. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℂ ∈ V | ||
Theorem | addcl 7713 | Alias for ax-addcl 7684, for naming consistency with addcli 7738. Use this theorem instead of ax-addcl 7684 or axaddcl 7640. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | readdcl 7714 | Alias for ax-addrcl 7685, for naming consistency with readdcli 7747. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | mulcl 7715 | Alias for ax-mulcl 7686, for naming consistency with mulcli 7739. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | remulcl 7716 | Alias for ax-mulrcl 7687, for naming consistency with remulcli 7748. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | ||
Theorem | mulcom 7717 | Alias for ax-mulcom 7689, for naming consistency with mulcomi 7740. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addass 7718 | Alias for ax-addass 7690, for naming consistency with addassi 7742. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulass 7719 | Alias for ax-mulass 7691, for naming consistency with mulassi 7743. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddi 7720 | Alias for ax-distr 7692, for naming consistency with adddii 7744. (Contributed by NM, 10-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | recn 7721 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) | ||
Theorem | reex 7722 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
⊢ ℝ ∈ V | ||
Theorem | reelprrecn 7723 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ℝ ∈ {ℝ, ℂ} | ||
Theorem | cnelprrecn 7724 | 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 7725 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | 0cn 7726 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnd 7727 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℂ) | ||
Theorem | c0ex 7728 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ∈ V | ||
Theorem | 1ex 7729 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 1 ∈ V | ||
Theorem | cnre 7730* | Alias for ax-cnre 7699, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦))) | ||
Theorem | mulid1 7731 | 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2 7732 | Identity law for multiplication. Note: see mulid1 7731 for commuted version. (Contributed by NM, 8-Oct-1999.) |
⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴) | ||
Theorem | 1re 7733 | 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
⊢ 1 ∈ ℝ | ||
Theorem | 0re 7734 | 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 0 ∈ ℝ | ||
Theorem | 0red 7735 | 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 0 ∈ ℝ) | ||
Theorem | mulid1i 7736 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 1) = 𝐴 | ||
Theorem | mulid2i 7737 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (1 · 𝐴) = 𝐴 | ||
Theorem | addcli 7738 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℂ | ||
Theorem | mulcli 7739 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℂ | ||
Theorem | mulcomi 7740 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴) | ||
Theorem | mulcomli 7741 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (𝐵 · 𝐴) = 𝐶 | ||
Theorem | addassi 7742 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) | ||
Theorem | mulassi 7743 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)) | ||
Theorem | adddii 7744 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)) | ||
Theorem | adddiri 7745 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)) | ||
Theorem | recni 7746 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | readdcli 7747 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 + 𝐵) ∈ ℝ | ||
Theorem | remulcli 7748 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐴 · 𝐵) ∈ ℝ | ||
Theorem | 1red 7749 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℝ) | ||
Theorem | 1cnd 7750 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
⊢ (𝜑 → 1 ∈ ℂ) | ||
Theorem | mulid1d 7751 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 1) = 𝐴) | ||
Theorem | mulid2d 7752 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (1 · 𝐴) = 𝐴) | ||
Theorem | addcld 7753 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ) | ||
Theorem | mulcld 7754 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | ||
Theorem | mulcomd 7755 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
Theorem | addassd 7756 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | ||
Theorem | mulassd 7757 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) | ||
Theorem | adddid 7758 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) | ||
Theorem | adddird 7759 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
Theorem | adddirp1d 7760 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵)) | ||
Theorem | joinlmuladdmuld 7761 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷) | ||
Theorem | recnd 7762 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | readdcld 7763 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) | ||
Theorem | remulcld 7764 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ) | ||
Syntax | cpnf 7765 | Plus infinity. |
class +∞ | ||
Syntax | cmnf 7766 | Minus infinity. |
class -∞ | ||
Syntax | cxr 7767 | The set of extended reals (includes plus and minus infinity). |
class ℝ* | ||
Syntax | clt 7768 | 'Less than' predicate (extended to include the extended reals). |
class < | ||
Syntax | cle 7769 | Extend wff notation to include the 'less than or equal to' relation. |
class ≤ | ||
Definition | df-pnf 7770 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that +∞ be a set not in ℝ and different from -∞
(df-mnf 7771). 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 7775
and mnfnre 7776, and we'll also be able to prove +∞ ≠ -∞.
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 7771 | 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 7776). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
⊢ -∞ = 𝒫 +∞ | ||
Definition | df-xr 7772 | 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 7773* | 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 7774 | Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.) |
⊢ ≤ = ((ℝ* × ℝ*) ∖ ◡ < ) | ||
Theorem | pnfnre 7775 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
⊢ +∞ ∉ ℝ | ||
Theorem | mnfnre 7776 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
⊢ -∞ ∉ ℝ | ||
Theorem | ressxr 7777 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
⊢ ℝ ⊆ ℝ* | ||
Theorem | rexpssxrxp 7778 | The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*) | ||
Theorem | rexr 7779 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | ||
Theorem | 0xr 7780 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
⊢ 0 ∈ ℝ* | ||
Theorem | renepnf 7781 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞) | ||
Theorem | renemnf 7782 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞) | ||
Theorem | rexrd 7783 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | renepnfd 7784 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≠ +∞) | ||
Theorem | renemnfd 7785 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐴 ≠ -∞) | ||
Theorem | pnfxr 7786 | Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) |
⊢ +∞ ∈ ℝ* | ||
Theorem | pnfex 7787 | Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ +∞ ∈ V | ||
Theorem | pnfnemnf 7788 | Plus and minus infinity are different elements of ℝ*. (Contributed by NM, 14-Oct-2005.) |
⊢ +∞ ≠ -∞ | ||
Theorem | mnfnepnf 7789 | Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -∞ ≠ +∞ | ||
Theorem | mnfxr 7790 | Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ -∞ ∈ ℝ* | ||
Theorem | rexri 7791 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 𝐴 ∈ ℝ* | ||
Theorem | renfdisj 7792 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (ℝ ∩ {+∞, -∞}) = ∅ | ||
Theorem | ltrelxr 7793 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ < ⊆ (ℝ* × ℝ*) | ||
Theorem | ltrel 7794 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
⊢ Rel < | ||
Theorem | lerelxr 7795 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ≤ ⊆ (ℝ* × ℝ*) | ||
Theorem | lerel 7796 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel ≤ | ||
Theorem | xrlenlt 7797 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) | ||
Theorem | ltxrlt 7798 | The standard less-than <ℝ and the extended real less-than < are identical when restricted to the non-extended reals ℝ. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵)) | ||
Theorem | axltirr 7799 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7700 with ordering on the extended reals. New proofs should use ltnr 7809 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
⊢ (𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴) | ||
Theorem | axltwlin 7800 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7701 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶 ∨ 𝐶 < 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |