Home | Metamath
Proof Explorer Theorem List (p. 109 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lttrd 10801 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) | ||
Theorem | lelttrdi 10802 | If a number is less than another number, and the other number is less than or equal to a third number, the first number is less than the third number. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 < 𝐶)) | ||
Theorem | dedekind 10803* | The Dedekind cut theorem. This theorem, which may be used to replace ax-pre-sup 10615 with appropriate adjustments, states that, if 𝐴 completely preceeds 𝐵, then there is some number separating the two of them. (Contributed by Scott Fenton, 13-Jun-2013.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 < 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) | ||
Theorem | dedekindle 10804* | The Dedekind cut theorem, with the hypothesis weakened to only require non-strict less than. (Contributed by Scott Fenton, 2-Jul-2013.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥 ≤ 𝑦) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)) | ||
Theorem | mul12 10805 | Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) | ||
Theorem | mul32 10806 | Commutative/associative law. (Contributed by NM, 8-Oct-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | ||
Theorem | mul31 10807 | Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) | ||
Theorem | mul4 10808 | Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | ||
Theorem | mul4r 10809 | Rearrangement of 4 factors: swap the right factors in the factors of a product of two products. (Contributed by AV, 4-Mar-2023.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐷) · (𝐶 · 𝐵))) | ||
Theorem | muladd11 10810 | A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((1 + 𝐴) · (1 + 𝐵)) = ((1 + 𝐴) + (𝐵 + (𝐴 · 𝐵)))) | ||
Theorem | 1p1times 10811 | Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | peano2cn 10812 | A theorem for complex numbers analogous the second Peano postulate peano2nn 11650. (Contributed by NM, 17-Aug-2005.) |
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) | ||
Theorem | peano2re 10813 | A theorem for reals analogous the second Peano postulate peano2nn 11650. (Contributed by NM, 5-Jul-2005.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) | ||
Theorem | readdcan 10814 | Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐶 + 𝐴) = (𝐶 + 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | 00id 10815 | 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (0 + 0) = 0 | ||
Theorem | mul02lem1 10816 | Lemma for mul02 10818. 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 10817 | Lemma for mul02 10818. Zero times a real is zero. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) | ||
Theorem | mul02 10818 | 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 10819 | 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 10820 | 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 10821* | 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 10822* | Existence of a left inverse for addition. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ (𝑥 + 𝐴) = 0) | ||
Theorem | addid2 10823 | 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 10824 | 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 10825 | Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addcom 10826 | 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 10827 | 0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 + 0) = 𝐴 | ||
Theorem | addid2i 10828 | 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (0 + 𝐴) = 𝐴 | ||
Theorem | mul02i 10829 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (0 · 𝐴) = 0 | ||
Theorem | mul01i 10830 | 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 10831 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴) | ||
Theorem | addcomli 10832 | Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
Theorem | addcani 10833 | 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 10834 | 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 10835 | 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 10836 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵) | ||
Theorem | mul4i 10837 | Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷)) | ||
Theorem | mul02d 10838 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (0 · 𝐴) = 0) | ||
Theorem | mul01d 10839 | Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 0) = 0) | ||
Theorem | addid1d 10840 | 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 0) = 𝐴) | ||
Theorem | addid2d 10841 | 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (0 + 𝐴) = 𝐴) | ||
Theorem | addcomd 10842 | Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | addcand 10843 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | addcan2d 10844 | Cancellation law for addition. Theorem I.1 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addcanad 10845 | Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 10843. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐴 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) | ||
Theorem | addcan2ad 10846 | Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 10844. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐶) = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | addneintrd 10847 | Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 10845. Consequence of addcand 10843. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐴 + 𝐶)) | ||
Theorem | addneintr2d 10848 | Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 10846. Consequence of addcan2d 10844. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) ≠ (𝐵 + 𝐶)) | ||
Theorem | mul12d 10849 | Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))) | ||
Theorem | mul32d 10850 | Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐴 · 𝐶) · 𝐵)) | ||
Theorem | mul31d 10851 | Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = ((𝐶 · 𝐵) · 𝐴)) | ||
Theorem | mul4d 10852 | Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) · (𝐶 · 𝐷)) = ((𝐴 · 𝐶) · (𝐵 · 𝐷))) | ||
Theorem | muladd11r 10853 | A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 1) · (𝐵 + 1)) = (((𝐴 · 𝐵) + (𝐴 + 𝐵)) + 1)) | ||
Theorem | comraddd 10854 | Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 + 𝐵)) | ||
Theorem | ltaddneg 10855 | Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) | ||
Theorem | ltaddnegr 10856 | Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵)) | ||
Theorem | add12 10857 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 11-May-2004.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) | ||
Theorem | add32 10858 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 13-Nov-1999.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) | ||
Theorem | add32r 10859 | 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 10860 | Rearrangement of 4 terms in a sum. (Contributed by NM, 13-Nov-1999.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) | ||
Theorem | add42 10861 | Rearrangement of 4 terms in a sum. (Contributed by NM, 12-May-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) | ||
Theorem | add12i 10862 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶)) | ||
Theorem | add32i 10863 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by NM, 21-Jan-1997.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵) | ||
Theorem | add4i 10864 | Rearrangement of 4 terms in a sum. (Contributed by NM, 9-May-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷)) | ||
Theorem | add42i 10865 | Rearrangement of 4 terms in a sum. (Contributed by NM, 22-Aug-1999.) (Proof shortened by OpenAI, 25-Mar-2020.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵)) | ||
Theorem | add12d 10866 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 + (𝐵 + 𝐶)) = (𝐵 + (𝐴 + 𝐶))) | ||
Theorem | add32d 10867 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = ((𝐴 + 𝐶) + 𝐵)) | ||
Theorem | add4d 10868 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐵 + 𝐷))) | ||
Theorem | add42d 10869 | Rearrangement of 4 terms in a sum. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 + 𝐷)) = ((𝐴 + 𝐶) + (𝐷 + 𝐵))) | ||
Syntax | cmin 10870 | Extend class notation to include subtraction. |
class − | ||
Syntax | cneg 10871 | 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 10870 (−) to prevent syntax ambiguity. For example, looking at the syntax definition co 7156, 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 10872* | Define subtraction. Theorem subval 10877 shows its value (and describes how this definition works), theorem subaddi 10973 relates it to addition, and theorems subcli 10962 and resubcli 10948 prove its closure laws. (Contributed by NM, 26-Nov-1994.) |
⊢ − = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (℩𝑧 ∈ ℂ (𝑦 + 𝑧) = 𝑥)) | ||
Definition | df-neg 10873 | Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 10871 for a discussion of this. (Contributed by NM, 10-Feb-1995.) |
⊢ -𝐴 = (0 − 𝐴) | ||
Theorem | 0cnALT 10874 | Alternate proof of 0cn 10633 which does not reference ax-1cn 10595. (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 10875 | Alternate proof of 0cnALT 10874 which is shorter, but depends on ax-8 2116, ax-13 2390, ax-sep 5203, ax-nul 5210, ax-pow 5266, ax-pr 5330, ax-un 7461, and every complex number axiom except ax-pre-mulgt0 10614 and ax-pre-sup 10615. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 0 ∈ ℂ | ||
Theorem | negeu 10876* | 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 10877* | 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 10878 | Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) | ||
Theorem | negeqi 10879 | Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ -𝐴 = -𝐵 | ||
Theorem | negeqd 10880 | Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → -𝐴 = -𝐵) | ||
Theorem | nfnegd 10881 | Deduction version of nfneg 10882. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥-𝐴) | ||
Theorem | nfneg 10882 | 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 10883 | 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 10884 | A negative is a set. (Contributed by NM, 4-Apr-2005.) |
⊢ -𝐴 ∈ V | ||
Theorem | subcl 10885 | Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ) | ||
Theorem | negcl 10886 | Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
⊢ (𝐴 ∈ ℂ → -𝐴 ∈ ℂ) | ||
Theorem | negicn 10887 | -i is a complex number. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ -i ∈ ℂ | ||
Theorem | subf 10888 | Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ − :(ℂ × ℂ)⟶ℂ | ||
Theorem | subadd 10889 | Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | subadd2 10890 | Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐶 + 𝐵) = 𝐴)) | ||
Theorem | subsub23 10891 | Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
Theorem | pncan 10892 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐵) = 𝐴) | ||
Theorem | pncan2 10893 | Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐴) = 𝐵) | ||
Theorem | pncan3 10894 | Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + (𝐵 − 𝐴)) = 𝐵) | ||
Theorem | npcan 10895 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐵) = 𝐴) | ||
Theorem | addsubass 10896 | Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = (𝐴 + (𝐵 − 𝐶))) | ||
Theorem | addsub 10897 | Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴 − 𝐶) + 𝐵)) | ||
Theorem | subadd23 10898 | Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) + 𝐶) = (𝐴 + (𝐶 − 𝐵))) | ||
Theorem | addsub12 10899 | Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 + (𝐵 − 𝐶)) = (𝐵 + (𝐴 − 𝐶))) | ||
Theorem | 2addsub 10900 | Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |