| Metamath
Proof Explorer Theorem List (p. 120 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulcan2 11901 | Cancellation law for multiplication. (Contributed by NM, 21-Jan-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | mulcani 11902 | Cancellation law for multiplication. Theorem I.7 of [Apostol] p. 18. (Contributed by NM, 26-Jan-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐶 ≠ 0 ⇒ ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵) | ||
| Theorem | mul0or 11903 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0))) | ||
| Theorem | mulne0b 11904 | The product of two nonzero numbers is nonzero. (Contributed by NM, 1-Aug-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0)) | ||
| Theorem | mulne0 11905 | The product of two nonzero numbers is nonzero. (Contributed by NM, 30-Dec-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 · 𝐵) ≠ 0) | ||
| Theorem | mulne0i 11906 | The product of two nonzero numbers is nonzero. (Contributed by NM, 15-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ≠ 0 ⇒ ⊢ (𝐴 · 𝐵) ≠ 0 | ||
| Theorem | muleqadd 11907 | Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 13-Nov-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1)) | ||
| Theorem | receu 11908* | Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by NM, 29-Jan-1995.) (Revised by Mario Carneiro, 17-Feb-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) | ||
| Theorem | mulnzcnf 11909 | Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007.) |
| ⊢ ( · ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))):((ℂ ∖ {0}) × (ℂ ∖ {0}))⟶(ℂ ∖ {0}) | ||
| Theorem | msq0i 11910 | A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by NM, 28-Jul-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0) | ||
| Theorem | mul0ori 11911 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by NM, 7-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0)) | ||
| Theorem | msq0d 11912 | A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0)) | ||
| Theorem | mul0ord 11913 | If a product is zero, one of its factors must be zero. Theorem I.11 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 0 ↔ (𝐴 = 0 ∨ 𝐵 = 0))) | ||
| Theorem | mulne0bd 11914 | The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 ≠ 0 ∧ 𝐵 ≠ 0) ↔ (𝐴 · 𝐵) ≠ 0)) | ||
| Theorem | mulne0d 11915 | The product of two nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) | ||
| Theorem | mulcan1g 11916 | A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 · 𝐶) ↔ (𝐴 = 0 ∨ 𝐵 = 𝐶))) | ||
| Theorem | mulcan2g 11917 | A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ (𝐴 = 𝐵 ∨ 𝐶 = 0))) | ||
| Theorem | mulne0bad 11918 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11915 and consequence of mulne0bd 11914. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
| Theorem | mulne0bbd 11919 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 11915 and consequence of mulne0bd 11914. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 · 𝐵) ≠ 0) ⇒ ⊢ (𝜑 → 𝐵 ≠ 0) | ||
| Syntax | cdiv 11920 | Extend class notation to include division. |
| class / | ||
| Definition | df-div 11921* | Define division. Theorem divmuli 12021 relates it to multiplication, and divcli 12009 and redivcli 12034 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divval 11924 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) |
| ⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) | ||
| Theorem | 1div0 11922 | You can't divide by zero, because division explicitly excludes zero from the domain of the function. Thus, by the definition of function value, it evaluates to the empty set. (This theorem is for information only and normally is not referenced by other proofs. To be meaningful, it assumes that ∅ is not a complex number, which depends on the particular complex number construction that is used.) (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof shortened by SN, 5-Jun-2025.) (New usage is discouraged.) |
| ⊢ (1 / 0) = ∅ | ||
| Theorem | 1div0OLD 11923 | Obsolete version of 1div0 11922 as of 5-Jun-2025. (Contributed by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (1 / 0) = ∅ | ||
| Theorem | divval 11924* | Value of division: if 𝐴 and 𝐵 are complex numbers with 𝐵 nonzero, then (𝐴 / 𝐵) is the (unique) complex number such that (𝐵 · 𝑥) = 𝐴. (Contributed by NM, 8-May-1999.) (Revised by Mario Carneiro, 17-Feb-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) | ||
| Theorem | divmul 11925 | Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 17-Feb-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴)) | ||
| Theorem | divmul2 11926 | Relationship between division and multiplication. (Contributed by NM, 7-Feb-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵))) | ||
| Theorem | divmul3 11927 | Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶))) | ||
| Theorem | divcl 11928 | Closure law for division. (Contributed by NM, 21-Jul-2001.) (Proof shortened by Mario Carneiro, 17-Feb-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℂ) | ||
| Theorem | reccl 11929 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℂ) | ||
| Theorem | divcan2 11930 | A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴) | ||
| Theorem | divcan1 11931 | A cancellation law for division. (Contributed by NM, 5-Jun-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴) | ||
| Theorem | diveq0 11932 | A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0)) | ||
| Theorem | divne0b 11933 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0)) | ||
| Theorem | divne0 11934 | The ratio of nonzero numbers is nonzero. (Contributed by NM, 28-Dec-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / 𝐵) ≠ 0) | ||
| Theorem | recne0 11935 | The reciprocal of a nonzero number is nonzero. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ≠ 0) | ||
| Theorem | recid 11936 | Multiplication of a number and its reciprocal. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 · (1 / 𝐴)) = 1) | ||
| Theorem | recid2 11937 | Multiplication of a number and its reciprocal. (Contributed by NM, 22-Jun-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 𝐴) · 𝐴) = 1) | ||
| Theorem | divrec 11938 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))) | ||
| Theorem | divrec2 11939 | Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴)) | ||
| Theorem | divass 11940 | An associative law for division. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))) | ||
| Theorem | div23 11941 | A commutative/associative law for division. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) | ||
| Theorem | div32 11942 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵))) | ||
| Theorem | div13 11943 | A commutative/associative law for division. (Contributed by NM, 22-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴)) | ||
| Theorem | div12 11944 | A commutative/associative law for division. (Contributed by NM, 30-Apr-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶))) | ||
| Theorem | divmulass 11945 | An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷))) | ||
| Theorem | divmulasscom 11946 | An associative/commutative law for division and multiplication. (Contributed by AV, 10-Jul-2021.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷))) | ||
| Theorem | divdir 11947 | Distribution of division over addition. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
| Theorem | divcan3 11948 | A cancellation law for division. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴) | ||
| Theorem | divcan4 11949 | A cancellation law for division. (Contributed by NM, 8-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴) | ||
| Theorem | div11 11950 | One-to-one relationship for division. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) (Proof shortened by SN, 9-Jul-2025.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | div11OLD 11951 | Obsolete version of div11 11950 as of 9-Jul-2025. (Contributed by NM, 20-Apr-2006.) (Proof shortened by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | diveq1 11952 | Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵)) | ||
| Theorem | divid 11953 | A number divided by itself is one. (Contributed by NM, 1-Aug-2004.) (Proof shortened by SN, 9-Jul-2025.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1) | ||
| Theorem | dividOLD 11954 | Obsolete version of divid 11953 as of 9-Jul-2025. (Contributed by NM, 1-Aug-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1) | ||
| Theorem | div0 11955 | Division into zero is zero. (Contributed by NM, 14-Mar-2005.) (Proof shortened by SN, 9-Jul-2025.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0) | ||
| Theorem | div0OLD 11956 | Obsolete version of div0 11955 as of 9-Jul-2025. (Contributed by NM, 14-Mar-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (0 / 𝐴) = 0) | ||
| Theorem | div1 11957 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴) | ||
| Theorem | 1div1e1 11958 | 1 divided by 1 is 1. (Contributed by David A. Wheeler, 7-Dec-2018.) |
| ⊢ (1 / 1) = 1 | ||
| Theorem | divneg 11959 | Move negative sign inside of a division. (Contributed by NM, 17-Sep-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵)) | ||
| Theorem | muldivdir 11960 | Distribution of division over addition with a multiplication. (Contributed by AV, 1-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶))) | ||
| Theorem | divsubdir 11961 | Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶))) | ||
| Theorem | subdivcomb1 11962 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((𝐶 · 𝐴) − 𝐵) / 𝐶) = (𝐴 − (𝐵 / 𝐶))) | ||
| Theorem | subdivcomb2 11963 | Bring a term in a subtraction into the numerator. (Contributed by Scott Fenton, 3-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 − (𝐶 · 𝐵)) / 𝐶) = ((𝐴 / 𝐶) − 𝐵)) | ||
| Theorem | recrec 11964 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 26-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / (1 / 𝐴)) = 𝐴) | ||
| Theorem | rec11 11965 | Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rec11r 11966 | Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴)) | ||
| Theorem | divmuldiv 11967 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷))) | ||
| Theorem | divdivdiv 11968 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 2-Aug-2004.) |
| ⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))) | ||
| Theorem | divcan5 11969 | Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵)) | ||
| Theorem | divmul13 11970 | Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐵 / 𝐶) · (𝐴 / 𝐷))) | ||
| Theorem | divmul24 11971 | Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 / 𝐷) · (𝐵 / 𝐶))) | ||
| Theorem | divmuleq 11972 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 23-Feb-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) = (𝐵 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐵 · 𝐶))) | ||
| Theorem | recdiv 11973 | The reciprocal of a ratio. (Contributed by NM, 3-Aug-2004.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴)) | ||
| Theorem | divcan6 11974 | Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1) | ||
| Theorem | divdiv32 11975 | Swap denominators in a division. (Contributed by NM, 2-Aug-2004.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)) | ||
| Theorem | divcan7 11976 | Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵)) | ||
| Theorem | dmdcan 11977 | Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · (𝐶 / 𝐴)) = (𝐶 / 𝐵)) | ||
| Theorem | divdiv1 11978 | Division into a fraction. (Contributed by NM, 31-Dec-2007.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶))) | ||
| Theorem | divdiv2 11979 | Division by a fraction. (Contributed by NM, 27-Dec-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵)) | ||
| Theorem | recdiv2 11980 | Division into a reciprocal. (Contributed by NM, 19-Oct-2007.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵))) | ||
| Theorem | ddcan 11981 | Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵) | ||
| Theorem | divadddiv 11982 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 2-May-2016.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) + (𝐵 / 𝐷)) = (((𝐴 · 𝐷) + (𝐵 · 𝐶)) / (𝐶 · 𝐷))) | ||
| Theorem | divsubdiv 11983 | Subtraction of two ratios. (Contributed by Scott Fenton, 22-Apr-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 ≠ 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷))) | ||
| Theorem | conjmul 11984 | Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 12-Nov-2006.) |
| ⊢ (((𝑃 ∈ ℂ ∧ 𝑃 ≠ 0) ∧ (𝑄 ∈ ℂ ∧ 𝑄 ≠ 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1)) | ||
| Theorem | rereccl 11985 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈ ℝ) | ||
| Theorem | redivcl 11986 | Closure law for division of reals. (Contributed by NM, 27-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ) | ||
| Theorem | eqneg 11987 | A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0)) | ||
| Theorem | eqnegd 11988 | A complex number equals its negative iff it is zero. Deduction form of eqneg 11987. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0)) | ||
| Theorem | eqnegad 11989 | If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 11987. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = -𝐴) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
| Theorem | div2neg 11990 | Quotient of two negatives. (Contributed by Paul Chapman, 10-Nov-2012.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵)) | ||
| Theorem | divneg2 11991 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 15-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵)) | ||
| Theorem | recclzi 11992 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℂ) | ||
| Theorem | recne0zi 11993 | The reciprocal of a nonzero number is nonzero. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ≠ 0) | ||
| Theorem | recidzi 11994 | Multiplication of a number and its reciprocal. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 ≠ 0 → (𝐴 · (1 / 𝐴)) = 1) | ||
| Theorem | div1i 11995 | A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 / 1) = 𝐴 | ||
| Theorem | eqnegi 11996 | A number equal to its negative is zero. (Contributed by NM, 29-May-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0) | ||
| Theorem | reccli 11997 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ (1 / 𝐴) ∈ ℂ | ||
| Theorem | recidi 11998 | Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ (𝐴 · (1 / 𝐴)) = 1 | ||
| Theorem | recreci 11999 | A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ (1 / (1 / 𝐴)) = 𝐴 | ||
| Theorem | dividi 12000 | A number divided by itself is one. (Contributed by NM, 9-Feb-1995.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ (𝐴 / 𝐴) = 1 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |