 Home Intuitionistic Logic ExplorerTheorem List (p. 88 of 105) < 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 - 8701-8800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremrpreccld 8701 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)       (𝜑 → (1 / 𝐴) ∈ ℝ+)

Theoremrprecred 8702 Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)       (𝜑 → (1 / 𝐴) ∈ ℝ)

Theoremrphalfcld 8703 Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)       (𝜑 → (𝐴 / 2) ∈ ℝ+)

Theoremreclt1d 8704 The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)       (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴)))

Theoremrecgt1d 8705 The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)       (𝜑 → (1 < 𝐴 ↔ (1 / 𝐴) < 1))

Theoremrpaddcld 8706 Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴 + 𝐵) ∈ ℝ+)

Theoremrpmulcld 8707 Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴 · 𝐵) ∈ ℝ+)

Theoremrpdivcld 8708 Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴 / 𝐵) ∈ ℝ+)

Theoremltrecd 8709 The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴)))

Theoremlerecd 8710 The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴)))

Theoremltrec1d 8711 Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑 → (1 / 𝐴) < 𝐵)       (𝜑 → (1 / 𝐵) < 𝐴)

Theoremlerec2d 8712 Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐴 ≤ (1 / 𝐵))       (𝜑𝐵 ≤ (1 / 𝐴))

Theoremlediv2ad 8713 Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐶)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))

Theoremltdiv2d 8714 Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴)))

Theoremlediv2d 8715 Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))

Theoremledivdivd 8716 Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐷 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) ≤ (𝐶 / 𝐷))       (𝜑 → (𝐷 / 𝐶) ≤ (𝐵 / 𝐴))

Theoremdivge1 8717 The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
((𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐴𝐵) → 1 ≤ (𝐵 / 𝐴))

Theoremdivlt1lt 8718 A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < 𝐵))

Theoremdivle1le 8719 A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 / 𝐵) ≤ 1 ↔ 𝐴𝐵))

Theoremledivge1le 8720 If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 1 ≤ 𝐶)) → (𝐴𝐵 → (𝐴 / 𝐶) ≤ 𝐵))

Theoremge0p1rpd 8721 A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → (𝐴 + 1) ∈ ℝ+)

Theoremrerpdivcld 8722 Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴 / 𝐵) ∈ ℝ)

Theoremltsubrpd 8723 Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (𝐴𝐵) < 𝐴)

Theoremltaddrpd 8724 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑𝐴 < (𝐴 + 𝐵))

Theoremltaddrp2d 8725 Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑𝐴 < (𝐵 + 𝐴))

Theoremltmulgt11d 8726 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (1 < 𝐴𝐵 < (𝐵 · 𝐴)))

Theoremltmulgt12d 8727 Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (1 < 𝐴𝐵 < (𝐴 · 𝐵)))

Theoremgt0divd 8728 Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵)))

Theoremge0divd 8729 Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)       (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵)))

Theoremrpgecld 8730 A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐵𝐴)       (𝜑𝐴 ∈ ℝ+)

Theoremdivge0d 8731 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑 → 0 ≤ 𝐴)       (𝜑 → 0 ≤ (𝐴 / 𝐵))

Theoremltmul1d 8732 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶)))

Theoremltmul2d 8733 Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵)))

Theoremlemul1d 8734 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)))

Theoremlemul2d 8735 Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)))

Theoremltdiv1d 8736 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶)))

Theoremlediv1d 8737 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → (𝐴𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶)))

Theoremltmuldivd 8738 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐶) < 𝐵𝐴 < (𝐵 / 𝐶)))

Theoremltmuldiv2d 8739 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐶 · 𝐴) < 𝐵𝐴 < (𝐵 / 𝐶)))

Theoremlemuldivd 8740 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵𝐴 ≤ (𝐵 / 𝐶)))

Theoremlemuldiv2d 8741 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵𝐴 ≤ (𝐵 / 𝐶)))

Theoremltdivmuld 8742 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) < 𝐵𝐴 < (𝐶 · 𝐵)))

Theoremltdivmul2d 8743 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) < 𝐵𝐴 < (𝐵 · 𝐶)))

Theoremledivmuld 8744 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵𝐴 ≤ (𝐶 · 𝐵)))

Theoremledivmul2d 8745 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)       (𝜑 → ((𝐴 / 𝐶) ≤ 𝐵𝐴 ≤ (𝐵 · 𝐶)))

Theoremltmul1dd 8746 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐴 · 𝐶) < (𝐵 · 𝐶))

Theoremltmul2dd 8747 Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐶 · 𝐴) < (𝐶 · 𝐵))

Theoremltdiv1dd 8748 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴 < 𝐵)       (𝜑 → (𝐴 / 𝐶) < (𝐵 / 𝐶))

Theoremlediv1dd 8749 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))

Theoremlediv12ad 8750 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝐷 ∈ ℝ)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)    &   (𝜑𝐶𝐷)       (𝜑 → (𝐴 / 𝐷) ≤ (𝐵 / 𝐶))

Theoremltdiv23d 8751 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) < 𝐶)       (𝜑 → (𝐴 / 𝐶) < 𝐵)

Theoremlediv23d 8752 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑 → (𝐴 / 𝐵) ≤ 𝐶)       (𝜑 → (𝐴 / 𝐶) ≤ 𝐵)

Theoremlt2mul2divd 8753 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑𝐷 ∈ ℝ+)       (𝜑 → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵)))

Theoremnnledivrp 8754 Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021.)
((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (1 ≤ 𝐵 ↔ (𝐴 / 𝐵) ≤ 𝐴))

Theoremnn0ledivnn 8755 Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.)
((𝐴 ∈ ℕ0𝐵 ∈ ℕ) → (𝐴 / 𝐵) ≤ 𝐴)

Theoremaddlelt 8756 If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021.)
((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → ((𝑀 + 𝐴) ≤ 𝑁𝑀 < 𝑁))

3.5.2  Infinity and the extended real number system (cont.)

Syntaxcxne 8757 Extend class notation to include the negative of an extended real.
class -𝑒𝐴

class +𝑒

Syntaxcxmu 8759 Extend class notation to include multiplication of extended reals.
class ·e

Definitiondf-xneg 8760 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
-𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))

Definitiondf-xadd 8761* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
+𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if(𝑥 = +∞, if(𝑦 = -∞, 0, +∞), if(𝑥 = -∞, if(𝑦 = +∞, 0, -∞), if(𝑦 = +∞, +∞, if(𝑦 = -∞, -∞, (𝑥 + 𝑦))))))

Definitiondf-xmul 8762* Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
·e = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, if((((0 < 𝑦𝑥 = +∞) ∨ (𝑦 < 0 ∧ 𝑥 = -∞)) ∨ ((0 < 𝑥𝑦 = +∞) ∨ (𝑥 < 0 ∧ 𝑦 = -∞))), +∞, if((((0 < 𝑦𝑥 = -∞) ∨ (𝑦 < 0 ∧ 𝑥 = +∞)) ∨ ((0 < 𝑥𝑦 = -∞) ∨ (𝑥 < 0 ∧ 𝑦 = +∞))), -∞, (𝑥 · 𝑦)))))

Theorempnfxr 8763 Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
+∞ ∈ ℝ*

Theorempnfex 8764 Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
+∞ ∈ V

Theoremmnfxr 8765 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.)
-∞ ∈ ℝ*

Theoremltxr 8766 The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 < 𝐵) ∨ (𝐴 = -∞ ∧ 𝐵 = +∞)) ∨ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) ∨ (𝐴 = -∞ ∧ 𝐵 ∈ ℝ)))))

Theoremelxr 8767 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Theorempnfnemnf 8768 Plus and minus infinity are different elements of *. (Contributed by NM, 14-Oct-2005.)
+∞ ≠ -∞

Theoremmnfnepnf 8769 Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ ≠ +∞

Theoremxrnemnf 8770 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ -∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞))

Theoremxrnepnf 8771 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
((𝐴 ∈ ℝ*𝐴 ≠ +∞) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = -∞))

Theoremxrltnr 8772 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < 𝐴)

Theoremltpnf 8773 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → 𝐴 < +∞)

Theorem0ltpnf 8774 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
0 < +∞

Theoremmnflt 8775 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
(𝐴 ∈ ℝ → -∞ < 𝐴)

Theoremmnflt0 8776 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-∞ < 0

Theoremmnfltpnf 8777 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-∞ < +∞

Theoremmnfltxr 8778 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
((𝐴 ∈ ℝ ∨ 𝐴 = +∞) → -∞ < 𝐴)

Theorempnfnlt 8779 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)

Theoremnltmnf 8780 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
(𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)

Theorempnfge 8781 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
(𝐴 ∈ ℝ*𝐴 ≤ +∞)

Theorem0lepnf 8782 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
0 ≤ +∞

Theoremnn0pnfge0 8783 If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
((𝑁 ∈ ℕ0𝑁 = +∞) → 0 ≤ 𝑁)

Theoremmnfle 8784 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
(𝐴 ∈ ℝ* → -∞ ≤ 𝐴)

Theoremxrltnsym 8785 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 → ¬ 𝐵 < 𝐴))

Theoremxrltnsym2 8786 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ¬ (𝐴 < 𝐵𝐵 < 𝐴))

Theoremxrlttr 8787 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremxrltso 8788 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
< Or ℝ*

Theoremxrlttri3 8789 Extended real version of lttri3 7127. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴)))

Theoremxrltle 8790 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵𝐴𝐵))

Theoremxrleid 8791 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
(𝐴 ∈ ℝ*𝐴𝐴)

Theoremxrletri3 8792 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴)))

Theoremxrlelttr 8793 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))

Theoremxrltletr 8794 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴 < 𝐵𝐵𝐶) → 𝐴 < 𝐶))

Theoremxrletr 8795 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Theoremxrlttrd 8796 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrlelttrd 8797 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵 < 𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrltletrd 8798 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴 < 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴 < 𝐶)

Theoremxrletrd 8799 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
(𝜑𝐴 ∈ ℝ*)    &   (𝜑𝐵 ∈ ℝ*)    &   (𝜑𝐶 ∈ ℝ*)    &   (𝜑𝐴𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)

Theoremxrltne 8800 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵) → 𝐵𝐴)

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-10454
 Copyright terms: Public domain < Previous  Next >