HomeHome Intuitionistic Logic Explorer
Theorem List (p. 73 of 110)
< 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 - 7201-7300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmulcld 7201 Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (𝐴 · 𝐵) ∈ ℂ)
 
Theoremmulcomd 7202 Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴))
 
Theoremaddassd 7203 Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
 
Theoremmulassd 7204 Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
 
Theoremadddid 7205 Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
 
Theoremadddird 7206 Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶)))
 
Theoremadddirp1d 7207 Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)       (𝜑 → ((𝐴 + 1) · 𝐵) = ((𝐴 · 𝐵) + 𝐵))
 
Theoremjoinlmuladdmuld 7208 Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑 → ((𝐴 · 𝐵) + (𝐶 · 𝐵)) = 𝐷)       (𝜑 → ((𝐴 + 𝐶) · 𝐵) = 𝐷)
 
Theoremrecnd 7209 Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ∈ ℂ)
 
Theoremreaddcld 7210 Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
 
Theoremremulcld 7211 Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 · 𝐵) ∈ ℝ)
 
3.2.2  Infinity and the extended real number system
 
Syntaxcpnf 7212 Plus infinity.
class +∞
 
Syntaxcmnf 7213 Minus infinity.
class -∞
 
Syntaxcxr 7214 The set of extended reals (includes plus and minus infinity).
class *
 
Syntaxclt 7215 'Less than' predicate (extended to include the extended reals).
class <
 
Syntaxcle 7216 Extend wff notation to include the 'less than or equal to' relation.
class
 
Definitiondf-pnf 7217 Define plus infinity. Note that the definition is arbitrary, requiring only that +∞ be a set not in and different from -∞ (df-mnf 7218). 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 7222 and mnfnre 7223, 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 7218 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 7223). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.)
-∞ = 𝒫 +∞
 
Definitiondf-xr 7219 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 7220* 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 7221 Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.)
≤ = ((ℝ* × ℝ*) ∖ < )
 
Theorempnfnre 7222 Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
+∞ ∉ ℝ
 
Theoremmnfnre 7223 Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
-∞ ∉ ℝ
 
Theoremressxr 7224 The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.)
ℝ ⊆ ℝ*
 
Theoremrexpssxrxp 7225 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 7226 A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
 
Theorem0xr 7227 Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
0 ∈ ℝ*
 
Theoremrenepnf 7228 No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(𝐴 ∈ ℝ → 𝐴 ≠ +∞)
 
Theoremrenemnf 7229 No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(𝐴 ∈ ℝ → 𝐴 ≠ -∞)
 
Theoremrexrd 7230 A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ∈ ℝ*)
 
Theoremrenepnfd 7231 No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ≠ +∞)
 
Theoremrenemnfd 7232 No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑𝐴 ≠ -∞)
 
Theorempnfxr 7233 Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
+∞ ∈ ℝ*
 
Theorempnfex 7234 Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
+∞ ∈ V
 
Theorempnfnemnf 7235 Plus and minus infinity are different elements of *. (Contributed by NM, 14-Oct-2005.)
+∞ ≠ -∞
 
Theoremmnfnepnf 7236 Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ ≠ +∞
 
Theoremmnfxr 7237 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 7238 A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
𝐴 ∈ ℝ       𝐴 ∈ ℝ*
 
Theoremrenfdisj 7239 The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
(ℝ ∩ {+∞, -∞}) = ∅
 
Theoremltrelxr 7240 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
< ⊆ (ℝ* × ℝ*)
 
Theoremltrel 7241 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
Rel <
 
Theoremlerelxr 7242 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
≤ ⊆ (ℝ* × ℝ*)
 
Theoremlerel 7243 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
Rel ≤
 
Theoremxrlenlt 7244 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
 
Theoremltxrlt 7245 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.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴 < 𝐵))
 
3.2.3  Restate the ordering postulates with extended real "less than"
 
Theoremaxltirr 7246 Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7150 with ordering on the extended reals. New proofs should use ltnr 7255 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
 
Theoremaxltwlin 7247 Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7151 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐴 < 𝐶𝐶 < 𝐵)))
 
Theoremaxlttrn 7248 Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7152 with ordering on the extended reals. New proofs should use lttr 7252 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremaxltadd 7249 Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7154 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐶 + 𝐴) < (𝐶 + 𝐵)))
 
Theoremaxapti 7250 Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7153 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ (𝐴 < 𝐵𝐵 < 𝐴)) → 𝐴 = 𝐵)
 
Theoremaxmulgt0 7251 The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7155 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵)))
 
3.2.4  Ordering on reals
 
Theoremlttr 7252 Alias for axlttrn 7248, for naming consistency with lttri 7282. New proofs should generally use this instead of ax-pre-lttrn 7152. (Contributed by NM, 10-Mar-2008.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremmulgt0 7253 The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
(((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 · 𝐵))
 
Theoremlenlt 7254 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
 
Theoremltnr 7255 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
(𝐴 ∈ ℝ → ¬ 𝐴 < 𝐴)
 
Theoremltso 7256 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
< Or ℝ
 
Theoremgtso 7257 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
< Or ℝ
 
Theoremlttri3 7258 Tightness of real apartness. (Contributed by NM, 5-May-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
 
Theoremletri3 7259 Tightness of real apartness. (Contributed by NM, 14-May-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
 
Theoremltleletr 7260 Transitive law, weaker form of (𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶. (Contributed by AV, 14-Oct-2018.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremletr 7261 Transitive law. (Contributed by NM, 12-Nov-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremleid 7262 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
(𝐴 ∈ ℝ → 𝐴𝐴)
 
Theoremltne 7263 'Less than' implies not equal. See also ltap 7798 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
((𝐴 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵𝐴)
 
Theoremltnsym 7264 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))
 
Theoremltle 7265 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
 
Theoremlelttr 7266 Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
 
Theoremltletr 7267 Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))
 
Theoremltnsym2 7268 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ (𝐴 < 𝐵𝐵 < 𝐴))
 
Theoremeqle 7269 Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
((𝐴 ∈ ℝ ∧ 𝐴 = 𝐵) → 𝐴𝐵)
 
Theoremltnri 7270 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
𝐴 ∈ ℝ        ¬ 𝐴 < 𝐴
 
Theoremeqlei 7271 Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
𝐴 ∈ ℝ       (𝐴 = 𝐵𝐴𝐵)
 
Theoremeqlei2 7272 Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
𝐴 ∈ ℝ       (𝐵 = 𝐴𝐵𝐴)
 
Theoremgtneii 7273 'Less than' implies not equal. See also gtapii 7799 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
𝐴 ∈ ℝ    &   𝐴 < 𝐵       𝐵𝐴
 
Theoremltneii 7274 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
𝐴 ∈ ℝ    &   𝐴 < 𝐵       𝐴𝐵
 
Theoremlttri3i 7275 Tightness of real apartness. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴))
 
Theoremletri3i 7276 Tightness of real apartness. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
 
Theoremltnsymi 7277 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴)
 
Theoremlenlti 7278 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴)
 
Theoremltlei 7279 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 < 𝐵𝐴𝐵)
 
Theoremltleii 7280 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐴 < 𝐵       𝐴𝐵
 
Theoremltnei 7281 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       (𝐴 < 𝐵𝐵𝐴)
 
Theoremlttri 7282 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐶 ∈ ℝ       ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶)
 
Theoremlelttri 7283 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐶 ∈ ℝ       ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶)
 
Theoremltletri 7284 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐶 ∈ ℝ       ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶)
 
Theoremletri 7285 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐶 ∈ ℝ       ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
 
Theoremle2tri3i 7286 Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   𝐶 ∈ ℝ       ((𝐴𝐵𝐵𝐶𝐶𝐴) ↔ (𝐴 = 𝐵𝐵 = 𝐶𝐶 = 𝐴))
 
Theoremmulgt0i 7287 The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ       ((0 < 𝐴 ∧ 0 < 𝐵) → 0 < (𝐴 · 𝐵))
 
Theoremmulgt0ii 7288 The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
𝐴 ∈ ℝ    &   𝐵 ∈ ℝ    &   0 < 𝐴    &   0 < 𝐵       0 < (𝐴 · 𝐵)
 
Theoremltnrd 7289 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)       (𝜑 → ¬ 𝐴 < 𝐴)
 
Theoremgtned 7290 'Less than' implies not equal. See also gtapd 7802 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐵𝐴)
 
Theoremltned 7291 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐴𝐵)
 
Theoremlttri3d 7292 Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))
 
Theoremletri3d 7293 Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))
 
Theoremlenltd 7294 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)       (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
 
Theoremltled 7295 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑𝐴𝐵)
 
Theoremltnsymd 7296 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴 < 𝐵)       (𝜑 → ¬ 𝐵 < 𝐴)
 
Theoremnltled 7297 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → ¬ 𝐵 < 𝐴)       (𝜑𝐴𝐵)
 
Theoremlensymd 7298 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐴𝐵)       (𝜑 → ¬ 𝐵 < 𝐴)
 
Theoremmulgt0d 7299 The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑 → 0 < 𝐵)       (𝜑 → 0 < (𝐴 · 𝐵))
 
Theoremletrd 7300 Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
    < 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-10953
  Copyright terms: Public domain < Previous  Next >