Home | Metamath
Proof Explorer Theorem List (p. 115 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 | divmul13i 11401 | Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ & ⊢ 𝐵 ≠ 0 & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷)) | ||
Theorem | divadddivi 11402 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by NM, 21-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ & ⊢ 𝐵 ≠ 0 & ⊢ 𝐷 ≠ 0 ⇒ ⊢ ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷)) | ||
Theorem | divdivdivi 11403 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by NM, 22-Feb-1995.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈ ℂ & ⊢ 𝐵 ≠ 0 & ⊢ 𝐷 ≠ 0 & ⊢ 𝐶 ≠ 0 ⇒ ⊢ ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)) | ||
Theorem | rerecclzi 11404 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 0 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | rereccli 11405 | Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ (1 / 𝐴) ∈ ℝ | ||
Theorem | redivclzi 11406 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ (𝐵 ≠ 0 → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | redivcli 11407 | Closure law for division of reals. (Contributed by NM, 9-May-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐵 ≠ 0 ⇒ ⊢ (𝐴 / 𝐵) ∈ ℝ | ||
Theorem | div1d 11408 | A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 / 1) = 𝐴) | ||
Theorem | reccld 11409 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ) | ||
Theorem | recne0d 11410 | The reciprocal of a nonzero number is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) ≠ 0) | ||
Theorem | recidd 11411 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (1 / 𝐴)) = 1) | ||
Theorem | recid2d 11412 | Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴) · 𝐴) = 1) | ||
Theorem | recrecd 11413 | A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴) | ||
Theorem | dividd 11414 | A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐴) = 1) | ||
Theorem | div0d 11415 | Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (0 / 𝐴) = 0) | ||
Theorem | divcld 11416 | Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ) | ||
Theorem | divcan1d 11417 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴) | ||
Theorem | divcan2d 11418 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴) | ||
Theorem | divrecd 11419 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))) | ||
Theorem | divrec2d 11420 | Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴)) | ||
Theorem | divcan3d 11421 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴) | ||
Theorem | divcan4d 11422 | A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴) | ||
Theorem | diveq0d 11423 | A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | diveq1d 11424 | Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐵) = 1) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | diveq1ad 11425 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 11331. Generalization of diveq1d 11424. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵)) | ||
Theorem | diveq0ad 11426 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 11308. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0)) | ||
Theorem | divne1d 11427 | If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 11424. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 1) | ||
Theorem | divne0bd 11428 | A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0)) | ||
Theorem | divnegd 11429 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵)) | ||
Theorem | divneg2d 11430 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵)) | ||
Theorem | div2negd 11431 | Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵)) | ||
Theorem | divne0d 11432 | The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 0) | ||
Theorem | recdivd 11433 | The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴)) | ||
Theorem | recdiv2d 11434 | Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵))) | ||
Theorem | divcan6d 11435 | Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1) | ||
Theorem | ddcand 11436 | Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵) | ||
Theorem | rec11d 11437 | Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | divmuld 11438 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)) | ||
Theorem | div32d 11439 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵))) | ||
Theorem | div13d 11440 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴)) | ||
Theorem | divdiv32d 11441 | Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)) | ||
Theorem | divcan5d 11442 | Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵)) | ||
Theorem | divcan5rd 11443 | Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵)) | ||
Theorem | divcan7d 11444 | Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵)) | ||
Theorem | dmdcand 11445 | Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶)) | ||
Theorem | dmdcan2d 11446 | Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶)) | ||
Theorem | divdiv1d 11447 | Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶))) | ||
Theorem | divdiv2d 11448 | Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵)) | ||
Theorem | divmul2d 11449 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵))) | ||
Theorem | divmul3d 11450 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶))) | ||
Theorem | divassd 11451 | An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))) | ||
Theorem | div12d 11452 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶))) | ||
Theorem | div23d 11453 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) | ||
Theorem | divdird 11454 | Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
Theorem | divsubdird 11455 | Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶))) | ||
Theorem | div11d 11456 | One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | divmuldivd 11457 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))) | ||
Theorem | divmul13d 11458 | Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))) | ||
Theorem | divmul24d 11459 | Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 / 𝐷) · (𝐶 / 𝐵))) | ||
Theorem | divadddivd 11460 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))) | ||
Theorem | divsubdivd 11461 | Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) − (𝐶 / 𝐷)) = (((𝐴 · 𝐷) − (𝐶 · 𝐵)) / (𝐵 · 𝐷))) | ||
Theorem | divmuleqd 11462 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐶 · 𝐵))) | ||
Theorem | divdivdivd 11463 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))) | ||
Theorem | diveq1bd 11464 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 11331. Converse of diveq1d 11424. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) = 1) | ||
Theorem | div2sub 11465 | Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷)) → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶))) | ||
Theorem | div2subd 11466 | Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 11465. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶))) | ||
Theorem | rereccld 11467 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | redivcld 11468 | Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | subrec 11469 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))) | ||
Theorem | subreci 11470 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ≠ 0 ⇒ ⊢ ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)) | ||
Theorem | subrecd 11471 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))) | ||
Theorem | mvllmuld 11472 | Move LHS left multiplication to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴)) | ||
Theorem | mvllmuli 11473 | Move LHS left multiplication to RHS. Uses divcan4i 11387. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 / 𝐴) | ||
Theorem | ldiv 11474 | Left-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 / 𝐵))) | ||
Theorem | rdiv 11475 | Right-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | mdiv 11476 | A division law. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 = (𝐶 / 𝐵) ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | lineq 11477 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (((𝐴 · 𝑋) + 𝐵) = 𝑌 ↔ 𝑋 = ((𝑌 − 𝐵) / 𝐴))) | ||
Theorem | elimgt0 11478 | Hypothesis for weak deduction theorem to eliminate 0 < 𝐴. (Contributed by NM, 15-May-1999.) |
⊢ 0 < if(0 < 𝐴, 𝐴, 1) | ||
Theorem | elimge0 11479 | Hypothesis for weak deduction theorem to eliminate 0 ≤ 𝐴. (Contributed by NM, 30-Jul-1999.) |
⊢ 0 ≤ if(0 ≤ 𝐴, 𝐴, 0) | ||
Theorem | ltp1 11480 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
Theorem | lep1 11481 | A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1)) | ||
Theorem | ltm1 11482 | A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴) | ||
Theorem | lem1 11483 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴) | ||
Theorem | letrp1 11484 | A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1)) | ||
Theorem | p1le 11485 | A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | recgt0 11486 | The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (1 / 𝐴)) | ||
Theorem | prodgt0 11487 | Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵) | ||
Theorem | prodgt02 11488 | Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴) | ||
Theorem | ltmul1a 11489 | Lemma for ltmul1 11490. Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) ∧ 𝐴 < 𝐵) → (𝐴 · 𝐶) < (𝐵 · 𝐶)) | ||
Theorem | ltmul1 11490 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 · 𝐶) < (𝐵 · 𝐶))) | ||
Theorem | ltmul2 11491 | Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐶 · 𝐴) < (𝐶 · 𝐵))) | ||
Theorem | lemul1 11492 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) | ||
Theorem | lemul2 11493 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) | ||
Theorem | lemul1a 11494 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) | ||
Theorem | lemul2a 11495 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) | ||
Theorem | ltmul12a 11496 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷)) | ||
Theorem | lemul12b 11497 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | lemul12a 11498 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | mulgt1 11499 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵)) | ||
Theorem | ltmulgt11 11500 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |