Home | Metamath
Proof Explorer Theorem List (p. 118 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rpnnen1OLD 11701* | One half of rpnnen 14795, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number 𝑥 to the sequence (𝐹‘𝑥):ℕ⟶ℚ such that ((𝐹‘𝑥)‘𝑘) is the largest rational number with denominator 𝑘 that is strictly less than 𝑥. In this manner, we get a monotonically increasing sequence that converges to 𝑥, and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) Obsolete version of rpnnen1 11696 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑇 = {𝑛 ∈ ℤ ∣ (𝑛 / 𝑘) < 𝑥} & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (𝑘 ∈ ℕ ↦ (sup(𝑇, ℝ, < ) / 𝑘))) ⇒ ⊢ ℝ ≼ (ℚ ↑𝑚 ℕ) | ||
Theorem | reexALT 11702 | Alternate proof of reex 9906. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℝ ∈ V | ||
Theorem | cnref1o 11703* | There is a natural one-to-one mapping from (ℝ × ℝ) to ℂ, where we map 〈𝑥, 𝑦〉 to (𝑥 + (i · 𝑦)). In our construction of the complex numbers, this is in fact our definition of ℂ (see df-c 9821), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ | ||
Theorem | cnexALT 11704 | The set of complex numbers exists. This theorem shows that ax-cnex 9871 is redundant if we assume ax-rep 4699. See also ax-cnex 9871. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ℂ ∈ V | ||
Theorem | xrex 11705 | The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
⊢ ℝ* ∈ V | ||
Theorem | addex 11706 | The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ + ∈ V | ||
Theorem | mulex 11707 | The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ · ∈ V | ||
Syntax | crp 11708 | Extend class notation to include the class of positive reals. |
class ℝ+ | ||
Definition | df-rp 11709 | Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ℝ+ = {𝑥 ∈ ℝ ∣ 0 < 𝑥} | ||
Theorem | elrp 11710 | Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | elrpii 11711 | Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.) |
⊢ 𝐴 ∈ ℝ & ⊢ 0 < 𝐴 ⇒ ⊢ 𝐴 ∈ ℝ+ | ||
Theorem | 1rp 11712 | 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.) |
⊢ 1 ∈ ℝ+ | ||
Theorem | 2rp 11713 | 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ 2 ∈ ℝ+ | ||
Theorem | 3rp 11714 | 3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ 3 ∈ ℝ+ | ||
Theorem | rpre 11715 | A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ) | ||
Theorem | rpxr 11716 | A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*) | ||
Theorem | rpcn 11717 | A positive real is a complex number. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ) | ||
Theorem | nnrp 11718 | A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+) | ||
Theorem | rpssre 11719 | The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.) |
⊢ ℝ+ ⊆ ℝ | ||
Theorem | rpgt0 11720 | A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴) | ||
Theorem | rpge0 11721 | A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.) |
⊢ (𝐴 ∈ ℝ+ → 0 ≤ 𝐴) | ||
Theorem | rpregt0 11722 | A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | rprege0 11723 | A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | ||
Theorem | rpne0 11724 | A positive real is nonzero. (Contributed by NM, 18-Jul-2008.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0) | ||
Theorem | rprene0 11725 | A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpcnne0 11726 | A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpcndif0 11727 | A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.) |
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ {0})) | ||
Theorem | ralrp 11728 | Quantification over positive reals. (Contributed by NM, 12-Feb-2008.) |
⊢ (∀𝑥 ∈ ℝ+ 𝜑 ↔ ∀𝑥 ∈ ℝ (0 < 𝑥 → 𝜑)) | ||
Theorem | rexrp 11729 | Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.) |
⊢ (∃𝑥 ∈ ℝ+ 𝜑 ↔ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ 𝜑)) | ||
Theorem | rpaddcl 11730 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 + 𝐵) ∈ ℝ+) | ||
Theorem | rpmulcl 11731 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 · 𝐵) ∈ ℝ+) | ||
Theorem | rpdivcl 11732 | Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ+) | ||
Theorem | rpreccl 11733 | Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.) |
⊢ (𝐴 ∈ ℝ+ → (1 / 𝐴) ∈ ℝ+) | ||
Theorem | rphalfcl 11734 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) ∈ ℝ+) | ||
Theorem | rpgecl 11735 | A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ+) | ||
Theorem | rphalflt 11736 | Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.) |
⊢ (𝐴 ∈ ℝ+ → (𝐴 / 2) < 𝐴) | ||
Theorem | rerpdivcl 11737 | Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | ge0p1rp 11738 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 + 1) ∈ ℝ+) | ||
Theorem | rpneg 11739 | Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20. (Contributed by NM, 7-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 ∈ ℝ+ ↔ ¬ -𝐴 ∈ ℝ+)) | ||
Theorem | negelrp 11740 | Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
⊢ (𝐴 ∈ ℝ → (-𝐴 ∈ ℝ+ ↔ 𝐴 < 0)) | ||
Theorem | 0nrp 11741 | Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
⊢ ¬ 0 ∈ ℝ+ | ||
Theorem | ltsubrp 11742 | Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (𝐴 − 𝐵) < 𝐴) | ||
Theorem | ltaddrp 11743 | Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵)) | ||
Theorem | difrp 11744 | Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℝ+)) | ||
Theorem | elrpd 11745 | Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | nnrpd 11746 | A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | zgt1rpn0n1 11747 | An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g. base 2, base 3 or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) |
⊢ (𝐵 ∈ (ℤ≥‘2) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) | ||
Theorem | rpred 11748 | A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ) | ||
Theorem | rpxrd 11749 | A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ*) | ||
Theorem | rpcnd 11750 | A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℂ) | ||
Theorem | rpgt0d 11751 | A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | rpge0d 11752 | A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | rpne0d 11753 | A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | rpregt0d 11754 | A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) | ||
Theorem | rprege0d 11755 | A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | ||
Theorem | rprene0d 11756 | A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpcnne0d 11757 | A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) | ||
Theorem | rpreccld 11758 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ+) | ||
Theorem | rprecred 11759 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | rphalfcld 11760 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ+) | ||
Theorem | reclt1d 11761 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) | ||
Theorem | recgt1d 11762 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ (1 / 𝐴) < 1)) | ||
Theorem | rpaddcld 11763 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ+) | ||
Theorem | rpmulcld 11764 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℝ+) | ||
Theorem | rpdivcld 11765 | Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ+) | ||
Theorem | ltrecd 11766 | The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) | ||
Theorem | lerecd 11767 | The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (1 / 𝐵) ≤ (1 / 𝐴))) | ||
Theorem | ltrec1d 11768 | Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → (1 / 𝐴) < 𝐵) ⇒ ⊢ (𝜑 → (1 / 𝐵) < 𝐴) | ||
Theorem | lerec2d 11769 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≤ (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐵 ≤ (1 / 𝐴)) | ||
Theorem | lediv2ad 11770 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐶) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)) | ||
Theorem | ltdiv2d 11771 | Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 / 𝐵) < (𝐶 / 𝐴))) | ||
Theorem | lediv2d 11772 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 / 𝐵) ≤ (𝐶 / 𝐴))) | ||
Theorem | ledivdivd 11773 | Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐷 ∈ ℝ+) & ⊢ (𝜑 → (𝐴 / 𝐵) ≤ (𝐶 / 𝐷)) ⇒ ⊢ (𝜑 → (𝐷 / 𝐶) ≤ (𝐵 / 𝐴)) | ||
Theorem | divge1 11774 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 1 ≤ (𝐵 / 𝐴)) | ||
Theorem | divlt1lt 11775 | 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 ↔ 𝐴 < 𝐵)) | ||
Theorem | divle1le 11776 | 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 ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | ledivge1le 11777 | 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 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐴 / 𝐶) ≤ 𝐵)) | ||
Theorem | ge0p1rpd 11778 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐴 + 1) ∈ ℝ+) | ||
Theorem | rerpdivcld 11779 | Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | ltsubrpd 11780 | Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) < 𝐴) | ||
Theorem | ltaddrpd 11781 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵)) | ||
Theorem | ltaddrp2d 11782 | Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐴)) | ||
Theorem | ltmulgt11d 11783 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐵 · 𝐴))) | ||
Theorem | ltmulgt12d 11784 | Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (1 < 𝐴 ↔ 𝐵 < (𝐴 · 𝐵))) | ||
Theorem | gt0divd 11785 | Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) | ||
Theorem | ge0divd 11786 | Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) | ||
Theorem | rpgecld 11787 | A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℝ+) | ||
Theorem | divge0d 11788 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴 / 𝐵)) | ||
Theorem | ltmul1d 11789 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) | ||
Theorem | ltmul2d 11790 | 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.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) | ||
Theorem | lemul1d 11791 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) | ||
Theorem | lemul2d 11792 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) | ||
Theorem | ltdiv1d 11793 | Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) | ||
Theorem | lediv1d 11794 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) | ||
Theorem | ltmuldivd 11795 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltmuldiv2d 11796 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | lemuldivd 11797 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | lemuldiv2d 11798 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | ltdivmuld 11799 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) | ||
Theorem | ltdivmul2d 11800 | 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |