HomeHome 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

Theorem List for Intuitionistic Logic Explorer - 7701-7800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Axiomax-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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
 
Axiomax-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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Axiomax-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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
 
Axiomax-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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
 
Axiomax-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 < (𝐴 · 𝐵)))
 
Axiomax-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.)

((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 𝐶) < (𝐵 · 𝐶) → (𝐴 < 𝐵𝐵 < 𝐴)))
 
Axiomax-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) ∈ 𝑥)}𝐴 < 𝑛)
 
Axiomax-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 < 𝑥 → ∃𝑗𝑁𝑘𝑁 (𝑗 < 𝑘 → ((𝐹𝑘) < (𝑦 + 𝑥) ∧ 𝑦 < ((𝐹𝑘) + 𝑥)))))
 
Axiomax-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.)

(((𝐴 ⊆ ℝ ∧ ∃𝑥 𝑥𝐴) ∧ (∃𝑥 ∈ ℝ ∀𝑦𝐴 𝑦 < 𝑥 ∧ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → (∃𝑧𝐴 𝑥 < 𝑧 ∨ ∀𝑧𝐴 𝑧 < 𝑦)))) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
 
Axiomax-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.)

+ :(ℂ × ℂ)⟶ℂ
 
Axiomax-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.)

· :(ℂ × ℂ)⟶ℂ
 
4.2  Derive the basic properties from the field axioms
 
4.2.1  Some deductions from the field axioms for complex numbers
 
Theoremcnex 7712 Alias for ax-cnex 7679. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℂ ∈ V
 
Theoremaddcl 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.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
 
Theoremreaddcl 7714 Alias for ax-addrcl 7685, for naming consistency with readdcli 7747. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
 
Theoremmulcl 7715 Alias for ax-mulcl 7686, for naming consistency with mulcli 7739. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
 
Theoremremulcl 7716 Alias for ax-mulrcl 7687, for naming consistency with remulcli 7748. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
 
Theoremmulcom 7717 Alias for ax-mulcom 7689, for naming consistency with mulcomi 7740. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
 
Theoremaddass 7718 Alias for ax-addass 7690, for naming consistency with addassi 7742. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
 
Theoremmulass 7719 Alias for ax-mulass 7691, for naming consistency with mulassi 7743. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
 
Theoremadddi 7720 Alias for ax-distr 7692, for naming consistency with adddii 7744. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
 
Theoremrecn 7721 A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
(𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
 
Theoremreex 7722 The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
ℝ ∈ V
 
Theoremreelprrecn 7723 Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
ℝ ∈ {ℝ, ℂ}
 
Theoremcnelprrecn 7724 Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
ℂ ∈ {ℝ, ℂ}
 
Theoremadddir 7725 Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
 
Theorem0cn 7726 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
0 ∈ ℂ
 
Theorem0cnd 7727 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
(𝜑 → 0 ∈ ℂ)
 
Theoremc0ex 7728 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
0 ∈ V
 
Theorem1ex 7729 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
1 ∈ V
 
Theoremcnre 7730* Alias for ax-cnre 7699, for naming consistency. (Contributed by NM, 3-Jan-2013.)
(𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
 
Theoremmulid1 7731 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
(𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
 
Theoremmulid2 7732 Identity law for multiplication. Note: see mulid1 7731 for commuted version. (Contributed by NM, 8-Oct-1999.)
(𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
 
Theorem1re 7733 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
1 ∈ ℝ
 
Theorem0re 7734 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
0 ∈ ℝ
 
Theorem0red 7735 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
(𝜑 → 0 ∈ ℝ)
 
Theoremmulid1i 7736 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ ℂ       (𝐴 · 1) = 𝐴
 
Theoremmulid2i 7737 Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
𝐴 ∈ ℂ       (1 · 𝐴) = 𝐴
 
Theoremaddcli 7738 Closure law for addition. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 + 𝐵) ∈ ℂ
 
Theoremmulcli 7739 Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 · 𝐵) ∈ ℂ
 
Theoremmulcomi 7740 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ       (𝐴 · 𝐵) = (𝐵 · 𝐴)
 
Theoremmulcomli 7741 Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   (𝐴 · 𝐵) = 𝐶       (𝐵 · 𝐴) = 𝐶
 
Theoremaddassi 7742 Associative law for addition. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   𝐶 ∈ ℂ       ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
 
Theoremmulassi 7743 Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   𝐶 ∈ ℂ       ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
 
Theoremadddii 7744 Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   𝐶 ∈ ℂ       (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))
 
Theoremadddiri 7745 Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
𝐴 ∈ ℂ    &   𝐵 ∈ ℂ    &   𝐶 ∈ ℂ       ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))
 
Theoremrecni 7746 A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
𝐴 ∈ ℝ       𝐴 ∈ ℂ
 
Theoremreaddcli 7747 Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 + 𝐵) ∈ ℝ
 
Theoremremulcli 7748 Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 · 𝐵) ∈ ℝ
 
Theorem1red 7749 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(𝜑 → 1 ∈ ℝ)
 
Theorem1cnd 7750 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(𝜑 → 1 ∈ ℂ)
 
Theoremmulid1d 7751 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (𝐴 · 1) = 𝐴)
 
Theoremmulid2d 7752 Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (1 · 𝐴) = 𝐴)
 
Theoremaddcld 7753 Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
 
Theoremmulcld 7754 Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
 
Theoremmulcomd 7755 Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
 
Theoremaddassd 7756 Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
 
Theoremmulassd 7757 Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
 
Theoremadddid 7758 Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
 
Theoremadddird 7759 Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
 
Theoremadddirp1d 7760 Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
 
Theoremjoinlmuladdmuld 7761 Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)       (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
 
Theoremrecnd 7762 Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ∈ ℂ)
 
Theoremreaddcld 7763 Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
 
Theoremremulcld 7764 Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
 
4.2.2  Infinity and the extended real number system
 
Syntaxcpnf 7765 Plus infinity.
class +∞
 
Syntaxcmnf 7766 Minus infinity.
class -∞
 
Syntaxcxr 7767 The set of extended reals (includes plus and minus infinity).
class *
 
Syntaxclt 7768 'Less than' predicate (extended to include the extended reals).
class <
 
Syntaxcle 7769 Extend wff notation to include the 'less than or equal to' relation.
class
 
Definitiondf-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.)

+∞ = 𝒫
 
Definitiondf-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.)
-∞ = 𝒫 +∞
 
Definitiondf-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.)
* = (ℝ ∪ {+∞, -∞})
 
Definitiondf-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.)
< = ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
 
Definitiondf-le 7774 Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
≤ = ((ℝ* × ℝ*) ∖ < )
 
Theorempnfnre 7775 Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
+∞ ∉ ℝ
 
Theoremmnfnre 7776 Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
-∞ ∉ ℝ
 
Theoremressxr 7777 The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
ℝ ⊆ ℝ*
 
Theoremrexpssxrxp 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.)
(ℝ × ℝ) ⊆ (ℝ* × ℝ*)
 
Theoremrexr 7779 A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
 
Theorem0xr 7780 Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
0 ∈ ℝ*
 
Theoremrenepnf 7781 No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(𝐴 ∈ ℝ → 𝐴 ≠ +∞)
 
Theoremrenemnf 7782 No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(𝐴 ∈ ℝ → 𝐴 ≠ -∞)
 
Theoremrexrd 7783 A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ∈ ℝ*)
 
Theoremrenepnfd 7784 No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ≠ +∞)
 
Theoremrenemnfd 7785 No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ≠ -∞)
 
Theorempnfxr 7786 Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
+∞ ∈ ℝ*
 
Theorempnfex 7787 Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
+∞ ∈ V
 
Theorempnfnemnf 7788 Plus and minus infinity are different elements of *. (Contributed by NM, 14-Oct-2005.)
+∞ ≠ -∞
 
Theoremmnfnepnf 7789 Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ ≠ +∞
 
Theoremmnfxr 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.)
-∞ ∈ ℝ*
 
Theoremrexri 7791 A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
𝐴 ∈ ℝ       𝐴 ∈ ℝ*
 
Theoremrenfdisj 7792 The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(ℝ ∩ {+∞, -∞}) = ∅
 
Theoremltrelxr 7793 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
< ⊆ (ℝ* × ℝ*)
 
Theoremltrel 7794 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
Rel <
 
Theoremlerelxr 7795 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
≤ ⊆ (ℝ* × ℝ*)
 
Theoremlerel 7796 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
Rel ≤
 
Theoremxrlenlt 7797 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
 
Theoremltxrlt 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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴 < 𝐵))
 
4.2.3  Restate the ordering postulates with extended real "less than"
 
Theoremaxltirr 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.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
 
Theoremaxltwlin 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 >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13145
  Copyright terms: Public domain < Previous  Next >