Home | Metamath
Proof Explorer Theorem List (p. 109 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | peano2cn 10801 | A theorem for complex numbers analogous the second Peano postulate peano2nn 11639. (Contributed by NM, 17-Aug-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) | ||
Theorem | peano2re 10802 | A theorem for reals analogous the second Peano postulate peano2nn 11639. (Contributed by NM, 5-Jul-2005.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) | ||
Theorem | readdcan 10803 | Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 00id 10804 | 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (0 + 0) = 0 | ||
Theorem | mul02lem1 10805 | Lemma for mul02 10807. If any real does not produce 0 when multiplied by 0, then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (((𝐴 ∈ ℝ ∧ (0 · 𝐴) ≠ 0) ∧ 𝐵 ∈ ℂ) → 𝐵 = (𝐵 + 𝐵)) | ||
Theorem | mul02lem2 10806 | Lemma for mul02 10807. Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
Theorem | mul02 10807 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. Based on ideas by Eric Schmidt. (Contributed by NM, 10-Aug-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) | ||
Theorem | mul01 10808 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0) | ||
Theorem | addid1 10809 | 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | ||
Theorem | cnegex 10810* | Existence of the negative of a complex number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝐴 + 𝑥) = 0) | ||
Theorem | cnegex2 10811* | Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0) | ||
Theorem | addid2 10812 | 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | ||
Theorem | addcan 10813 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | addcan2 10814 | Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addcom 10815 | Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | addid1i 10816 | 0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + 0) = 𝐴 | ||
Theorem | addid2i 10817 | 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (0 + 𝐴) = 𝐴 | ||
Theorem | mul02i 10818 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (0 · 𝐴) = 0 | ||
Theorem | mul01i 10819 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 0) = 0 | ||
Theorem | addcomi 10820 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
Theorem | addcomli 10821 | Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | addcani 10822 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 27-Oct-1999.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶) | ||
Theorem | addcan2i 10823 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by NM, 14-May-2003.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵) | ||
Theorem | mul12i 10824 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)) | ||
Theorem | mul32i 10825 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) | ||
Theorem | mul4i 10826 | Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) | ||
Theorem | mul02d 10827 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (0 · 𝐴) = 0) | ||
Theorem | mul01d 10828 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 0) = 0) | ||
Theorem | addid1d 10829 | 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) | ||
Theorem | addid2d 10830 | 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) | ||
Theorem | addcomd 10831 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | addcand 10832 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | addcan2d 10833 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addcanad 10834 | Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 10832. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | addcan2ad 10835 | Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 10833. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | addneintrd 10836 | Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 10834. Consequence of addcand 10832. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) | ||
Theorem | addneintr2d 10837 | Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 10835. Consequence of addcan2d 10833. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) | ||
Theorem | mul12d 10838 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) | ||
Theorem | mul32d 10839 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | ||
Theorem | mul31d 10840 | Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) | ||
Theorem | mul4d 10841 | Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | ||
Theorem | muladd11r 10842 | A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) | ||
Theorem | comraddd 10843 | Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐵)) | ||
Theorem | ltaddneg 10844 | Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) | ||
Theorem | ltaddnegr 10845 | Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵)) | ||
Theorem | add12 10846 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) | ||
Theorem | add32 10847 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) | ||
Theorem | add32r 10848 | Commutative/associative law that swaps the last two terms in a triple sum, rearranging the parentheses. (Contributed by Paul Chapman, 18-May-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = ((𝐴 + 𝐶) + 𝐵)) | ||
Theorem | add4 10849 | Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) | ||
Theorem | add42 10850 | Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) | ||
Theorem | add12i 10851 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) | ||
Theorem | add32i 10852 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) | ||
Theorem | add4i 10853 | Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) | ||
Theorem | add42i 10854 | Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) | ||
Theorem | add12d 10855 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) | ||
Theorem | add32d 10856 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) | ||
Theorem | add4d 10857 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) | ||
Theorem | add42d 10858 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) | ||
Syntax | cmin 10859 | Extend class notation to include subtraction. |
class − | ||
Syntax | cneg 10860 | Extend class notation to include unary minus. The symbol - is not a class by itself but part of a compound class definition. We do this rather than making it a formal function since it is so commonly used. Note: We use different symbols for unary minus (-) and subtraction cmin 10859 (−) to prevent syntax ambiguity. For example, looking at the syntax definition co 7145, if we used the same symbol then "( − 𝐴 − 𝐵) " could mean either "− 𝐴 " minus "𝐵", or it could represent the (meaningless) operation of classes "− " and "− 𝐵 " connected with "operation" "𝐴". On the other hand, "(-𝐴 − 𝐵) " is unambiguous. |
class -𝐴 | ||
Definition | df-sub 10861* | Define subtraction. Theorem subval 10866 shows its value (and describes how this definition works), theorem subaddi 10962 relates it to addition, and theorems subcli 10951 and resubcli 10937 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) | ||
Definition | df-neg 10862 | Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 10860 for a discussion of this. (Contributed by NM, 10-Feb-1995.) |
⊢ -𝐴 = (0 − 𝐴) | ||
Theorem | 0cnALT 10863 | Alternate proof of 0cn 10622 which does not reference ax-1cn 10584. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 7-Jan-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | 0cnALT2 10864 | Alternate proof of 0cnALT 10863 which is shorter, but depends on ax-8 2107, ax-13 2383, ax-sep 5195, ax-nul 5202, ax-pow 5258, ax-pr 5321, ax-un 7450, and every complex number axiom except ax-pre-mulgt0 10603 and ax-pre-sup 10604. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | negeu 10865* | Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | subval 10866* | Value of subtraction, which is the (unique) element 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 2-Nov-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) = (℩𝑥 ∈ ℂ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | negeq 10867 | Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | ||
Theorem | negeqi 10868 | Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝐴 = -𝐵 | ||
Theorem | negeqd 10869 | Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐴 = -𝐵) | ||
Theorem | nfnegd 10870 | Deduction version of nfneg 10871. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝐴) | ||
Theorem | nfneg 10871 | Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥-𝐴 | ||
Theorem | csbnegg 10872 | Move class substitution in and out of the negative of a number. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌-𝐵 = -⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | negex 10873 | A negative is a set. (Contributed by NM, 4-Apr-2005.) |
⊢ -𝐴 ∈ V | ||
Theorem | subcl 10874 | Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | negcl 10875 | Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) | ||
Theorem | negicn 10876 | -i is a complex number. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ -i ∈ ℂ | ||
Theorem | subf 10877 | Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ − :(ℂ × ℂ)⟶ℂ | ||
Theorem | subadd 10878 | Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | subadd2 10879 | Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) | ||
Theorem | subsub23 10880 | Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | pncan 10881 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | pncan2 10882 | Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
Theorem | pncan3 10883 | Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
Theorem | npcan 10884 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | addsubass 10885 | Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) | ||
Theorem | addsub 10886 | Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) | ||
Theorem | subadd23 10887 | Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | addsub12 10888 | Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) | ||
Theorem | 2addsub 10889 | Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) | ||
Theorem | addsubeq4 10890 | Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) | ||
Theorem | pncan3oi 10891 | Subtraction and addition of equals. Almost but not exactly the same as pncan3i 10952 and pncan 10881, this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand 10987. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) − 𝐵) = 𝐴 | ||
Theorem | mvrraddi 10892 | Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐴 = (𝐵 + 𝐶) ⇒ ⊢ (𝐴 − 𝐶) = 𝐵 | ||
Theorem | mvlladdi 10893 | Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 − 𝐴) | ||
Theorem | subid 10894 | Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) | ||
Theorem | subid1 10895 | Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) | ||
Theorem | npncan 10896 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐵 − 𝐶)) = (𝐴 − 𝐶)) | ||
Theorem | nppcan 10897 | Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) + 𝐵) = (𝐴 + 𝐶)) | ||
Theorem | nnpcan 10898 | Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) − 𝐶) + 𝐵) = (𝐴 − 𝐶)) | ||
Theorem | nppcan3 10899 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) | ||
Theorem | subcan2 10900 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |