![]() |
Metamath
Proof Explorer Theorem List (p. 109 of 437) | < 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: | ![]() (1-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pncan1 10801 | Cancellation law for addition and subtraction with 1. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴) | ||
Theorem | npcan1 10802 | Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴) | ||
Theorem | subeq0bd 10803 | If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 10746. Converse of subeq0d 10744. Contrapositive of subne0ad 10747. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = 0) | ||
Theorem | renegcld 10804 | Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ) | ||
Theorem | resubcld 10805 | Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | negn0 10806* | The image under negation of a nonempty set of reals is nonempty. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅) → {𝑧 ∈ ℝ ∣ -𝑧 ∈ 𝐴} ≠ ∅) | ||
Theorem | negf1o 10807* | Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) | ||
Theorem | kcnktkm1cn 10808 | k times k minus 1 is a complex number if k is a complex number. (Contributed by Alexander van der Vekens, 11-Mar-2018.) |
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈ ℂ) | ||
Theorem | muladd 10809 | Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) | ||
Theorem | subdi 10810 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) | ||
Theorem | subdir 10811 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) | ||
Theorem | ine0 10812 | The imaginary unit i is not zero. (Contributed by NM, 6-May-1999.) |
⊢ i ≠ 0 | ||
Theorem | mulneg1 10813 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) | ||
Theorem | mulneg2 10814 | The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) | ||
Theorem | mulneg12 10815 | Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵)) | ||
Theorem | mul2neg 10816 | Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) | ||
Theorem | submul2 10817 | Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶))) | ||
Theorem | mulm1 10818 | Product with minus one is negative. (Contributed by NM, 16-Nov-1999.) |
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) | ||
Theorem | addneg1mul 10819 | Addition with product with minus one is a subtraction. (Contributed by AV, 18-Oct-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (-1 · 𝐵)) = (𝐴 − 𝐵)) | ||
Theorem | mulsub 10820 | Product of two differences. (Contributed by NM, 14-Jan-2006.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) | ||
Theorem | mulsub2 10821 | Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))) | ||
Theorem | mulm1i 10822 | Product with minus one is negative. (Contributed by NM, 31-Jul-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (-1 · 𝐴) = -𝐴 | ||
Theorem | mulneg1i 10823 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 · 𝐵) = -(𝐴 · 𝐵) | ||
Theorem | mulneg2i 10824 | Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵) | ||
Theorem | mul2negi 10825 | Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (-𝐴 · -𝐵) = (𝐴 · 𝐵) | ||
Theorem | subdii 10826 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)) | ||
Theorem | subdiri 10827 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) | ||
Theorem | muladdi 10828 | Product of two sums. (Contributed by NM, 17-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))) | ||
Theorem | mulm1d 10829 | Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (-1 · 𝐴) = -𝐴) | ||
Theorem | mulneg1d 10830 | Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) | ||
Theorem | mulneg2d 10831 | Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) | ||
Theorem | mul2negd 10832 | Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) | ||
Theorem | subdid 10833 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) | ||
Theorem | subdird 10834 | Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) | ||
Theorem | muladdd 10835 | Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) | ||
Theorem | mulsubd 10836 | Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) | ||
Theorem | muls1d 10837 | Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 − 1)) = ((𝐴 · 𝐵) − 𝐴)) | ||
Theorem | mulsubfacd 10838 | Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵)) | ||
Theorem | addmulsub 10839 | The product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐵 · 𝐶)) − ((𝐴 · 𝐷) + (𝐵 · 𝐷)))) | ||
Theorem | subaddmulsub 10840 | The difference with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ 𝐸 ∈ ℂ) → (𝐸 − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐸 − (𝐴 · 𝐶)) − (𝐵 · 𝐶)) + ((𝐴 · 𝐷) + (𝐵 · 𝐷)))) | ||
Theorem | mulsubaddmulsub 10841 | A special difference of a product with a product of a sum and a difference. (Contributed by AV, 5-Mar-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐵 · 𝐶) − ((𝐴 + 𝐵) · (𝐶 − 𝐷))) = (((𝐴 · 𝐷) + (𝐵 · 𝐷)) − (𝐴 · 𝐶))) | ||
Theorem | gt0ne0 10842 | Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) | ||
Theorem | lt0ne0 10843 | A number which is less than zero is not zero. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0) | ||
Theorem | ltadd1 10844 | Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))) | ||
Theorem | leadd1 10845 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 18-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))) | ||
Theorem | leadd2 10846 | Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) | ||
Theorem | ltsubadd 10847 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) | ||
Theorem | ltsubadd2 10848 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | lesubadd 10849 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))) | ||
Theorem | lesubadd2 10850 | 'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) | ||
Theorem | ltaddsub 10851 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) | ||
Theorem | ltaddsub2 10852 | 'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) | ||
Theorem | leaddsub 10853 | 'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) | ||
Theorem | leaddsub2 10854 | 'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) | ||
Theorem | suble 10855 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) | ||
Theorem | lesub 10856 | Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴))) | ||
Theorem | ltsub23 10857 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵)) | ||
Theorem | ltsub13 10858 | 'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴))) | ||
Theorem | le2add 10859 | Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) | ||
Theorem | ltleadd 10860 | Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | leltadd 10861 | Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | lt2add 10862 | Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) | ||
Theorem | addgt0 10863 | The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgegt0 10864 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addgtge0 10865 | The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 < 𝐴 ∧ 0 ≤ 𝐵)) → 0 < (𝐴 + 𝐵)) | ||
Theorem | addge0 10866 | The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | ltaddpos 10867 | Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐵 + 𝐴))) | ||
Theorem | ltaddpos2 10868 | Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ 𝐵 < (𝐴 + 𝐵))) | ||
Theorem | ltsubpos 10869 | Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐴 ↔ (𝐵 − 𝐴) < 𝐵)) | ||
Theorem | posdif 10870 | Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) | ||
Theorem | lesub1 10871 | Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 − 𝐶) ≤ (𝐵 − 𝐶))) | ||
Theorem | lesub2 10872 | Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) | ||
Theorem | ltsub1 10873 | Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐶) < (𝐵 − 𝐶))) | ||
Theorem | ltsub2 10874 | Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 − 𝐵) < (𝐶 − 𝐴))) | ||
Theorem | lt2sub 10875 | Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐷 < 𝐵) → (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | le2sub 10876 | Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵) → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷))) | ||
Theorem | ltneg 10877 | Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ -𝐵 < -𝐴)) | ||
Theorem | ltnegcon1 10878 | Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 < 𝐵 ↔ -𝐵 < 𝐴)) | ||
Theorem | ltnegcon2 10879 | Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < -𝐵 ↔ 𝐵 < -𝐴)) | ||
Theorem | leneg 10880 | Negative of both sides of 'less than or equal to'. (Contributed by NM, 12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ -𝐵 ≤ -𝐴)) | ||
Theorem | lenegcon1 10881 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) | ||
Theorem | lenegcon2 10882 | Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ -𝐵 ↔ 𝐵 ≤ -𝐴)) | ||
Theorem | lt0neg1 10883 | Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
⊢ (𝐴 ∈ ℝ → (𝐴 < 0 ↔ 0 < -𝐴)) | ||
Theorem | lt0neg2 10884 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ -𝐴 < 0)) | ||
Theorem | le0neg1 10885 | Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.) |
⊢ (𝐴 ∈ ℝ → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) | ||
Theorem | le0neg2 10886 | Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.) |
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ -𝐴 ≤ 0)) | ||
Theorem | addge01 10887 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐴 + 𝐵))) | ||
Theorem | addge02 10888 | A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 + 𝐴))) | ||
Theorem | add20 10889 | Two nonnegative numbers are zero iff their sum is zero. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴 + 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) | ||
Theorem | subge0 10890 | Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) | ||
Theorem | suble0 10891 | Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 0 ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | leaddle0 10892 | The sum of a real number and a second real number is less than the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐴 ↔ 𝐵 ≤ 0)) | ||
Theorem | subge02 10893 | Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ 𝐵 ↔ (𝐴 − 𝐵) ≤ 𝐴)) | ||
Theorem | lesub0 10894 | Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 ≤ 𝐴 ∧ 𝐵 ≤ (𝐵 − 𝐴)) ↔ 𝐴 = 0)) | ||
Theorem | mulge0 10895 | The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵)) | ||
Theorem | mullt0 10896 | The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 𝐵 < 0)) → 0 < (𝐴 · 𝐵)) | ||
Theorem | msqgt0 10897 | A nonzero square is positive. Theorem I.20 of [Apostol] p. 20. (Contributed by NM, 6-May-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴 · 𝐴)) | ||
Theorem | msqge0 10898 | A square is nonnegative. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴)) | ||
Theorem | 0lt1 10899 | 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.) |
⊢ 0 < 1 | ||
Theorem | 0le1 10900 | 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ 0 ≤ 1 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |