Home | Metamath
Proof Explorer Theorem List (p. 116 of 460) | < 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-28853) |
Hilbert Space Explorer
(28854-30376) |
Users' Mathboxes
(30377-45962) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diveq0d 11501 | A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐵) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | diveq1d 11502 | Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐵) = 1) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | diveq1ad 11503 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 11409. Generalization of diveq1d 11502. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵)) | ||
Theorem | diveq0ad 11504 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 11386. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0)) | ||
Theorem | divne1d 11505 | If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 11502. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 1) | ||
Theorem | divne0bd 11506 | A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 / 𝐵) ≠ 0)) | ||
Theorem | divnegd 11507 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵)) | ||
Theorem | divneg2d 11508 | Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵)) | ||
Theorem | div2negd 11509 | Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵)) | ||
Theorem | divne0d 11510 | The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ≠ 0) | ||
Theorem | recdivd 11511 | The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴)) | ||
Theorem | recdiv2d 11512 | Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵))) | ||
Theorem | divcan6d 11513 | Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1) | ||
Theorem | ddcand 11514 | Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵) | ||
Theorem | rec11d 11515 | Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | divmuld 11516 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)) | ||
Theorem | div32d 11517 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵))) | ||
Theorem | div13d 11518 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴)) | ||
Theorem | divdiv32d 11519 | Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)) | ||
Theorem | divcan5d 11520 | Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵)) | ||
Theorem | divcan5rd 11521 | Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵)) | ||
Theorem | divcan7d 11522 | Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵)) | ||
Theorem | dmdcand 11523 | Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶)) | ||
Theorem | dmdcan2d 11524 | Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶)) | ||
Theorem | divdiv1d 11525 | Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶))) | ||
Theorem | divdiv2d 11526 | Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵)) | ||
Theorem | divmul2d 11527 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵))) | ||
Theorem | divmul3d 11528 | Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶))) | ||
Theorem | divassd 11529 | An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))) | ||
Theorem | div12d 11530 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶))) | ||
Theorem | div23d 11531 | A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)) | ||
Theorem | divdird 11532 | Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
Theorem | divsubdird 11533 | Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶))) | ||
Theorem | div11d 11534 | One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | divmuldivd 11535 | Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))) | ||
Theorem | divmul13d 11536 | Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))) | ||
Theorem | divmul24d 11537 | Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 / 𝐷) · (𝐶 / 𝐵))) | ||
Theorem | divadddivd 11538 | Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))) | ||
Theorem | divsubdivd 11539 | Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) − (𝐶 / 𝐷)) = (((𝐴 · 𝐷) − (𝐶 · 𝐵)) / (𝐵 · 𝐷))) | ||
Theorem | divmuleqd 11540 | Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐶 · 𝐵))) | ||
Theorem | divdivdivd 11541 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐷 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))) | ||
Theorem | diveq1bd 11542 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 11409. Converse of diveq1d 11502. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) = 1) | ||
Theorem | div2sub 11543 | Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷)) → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶))) | ||
Theorem | div2subd 11544 | Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 11543. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶))) | ||
Theorem | rereccld 11545 | Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | redivcld 11546 | Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
Theorem | subrec 11547 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))) | ||
Theorem | subreci 11548 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ 𝐵 ≠ 0 ⇒ ⊢ ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)) | ||
Theorem | subrecd 11549 | Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))) | ||
Theorem | mvllmuld 11550 | Move the left term in a product on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴)) | ||
Theorem | mvllmuli 11551 | Move the left term in a product on the LHS to the RHS, inference form. Uses divcan4i 11465. (Contributed by David A. Wheeler, 11-Oct-2018.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐴 ≠ 0 & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ 𝐵 = (𝐶 / 𝐴) | ||
Theorem | ldiv 11552 | Left-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 / 𝐵))) | ||
Theorem | rdiv 11553 | Right-division. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | mdiv 11554 | A division law. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 = (𝐶 / 𝐵) ↔ 𝐵 = (𝐶 / 𝐴))) | ||
Theorem | lineq 11555 | Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝑌 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (((𝐴 · 𝑋) + 𝐵) = 𝑌 ↔ 𝑋 = ((𝑌 − 𝐵) / 𝐴))) | ||
Theorem | elimgt0 11556 | Hypothesis for weak deduction theorem to eliminate 0 < 𝐴. (Contributed by NM, 15-May-1999.) |
⊢ 0 < if(0 < 𝐴, 𝐴, 1) | ||
Theorem | elimge0 11557 | Hypothesis for weak deduction theorem to eliminate 0 ≤ 𝐴. (Contributed by NM, 30-Jul-1999.) |
⊢ 0 ≤ if(0 ≤ 𝐴, 𝐴, 0) | ||
Theorem | ltp1 11558 | A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.) |
⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1)) | ||
Theorem | lep1 11559 | A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1)) | ||
Theorem | ltm1 11560 | A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) < 𝐴) | ||
Theorem | lem1 11561 | A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ≤ 𝐴) | ||
Theorem | letrp1 11562 | A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ (𝐵 + 1)) | ||
Theorem | p1le 11563 | A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + 1) ≤ 𝐵) → 𝐴 ≤ 𝐵) | ||
Theorem | recgt0 11564 | 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 11565 | 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 11566 | Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐵 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴) | ||
Theorem | ltmul1a 11567 | Lemma for ltmul1 11568. 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 11568 | 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 11569 | 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 11570 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐶) ≤ (𝐵 · 𝐶))) | ||
Theorem | lemul2 11571 | Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐶 · 𝐴) ≤ (𝐶 · 𝐵))) | ||
Theorem | lemul1a 11572 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by NM, 21-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐶)) | ||
Theorem | lemul2a 11573 | Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) ∧ 𝐴 ≤ 𝐵) → (𝐶 · 𝐴) ≤ (𝐶 · 𝐵)) | ||
Theorem | ltmul12a 11574 | Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.) |
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) ∧ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) ∧ (0 ≤ 𝐶 ∧ 𝐶 < 𝐷))) → (𝐴 · 𝐶) < (𝐵 · 𝐷)) | ||
Theorem | lemul12b 11575 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷))) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | lemul12a 11576 | Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.) |
⊢ ((((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℝ) ∧ ((𝐶 ∈ ℝ ∧ 0 ≤ 𝐶) ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷) → (𝐴 · 𝐶) ≤ (𝐵 · 𝐷))) | ||
Theorem | mulgt1 11577 | The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → 1 < (𝐴 · 𝐵)) | ||
Theorem | ltmulgt11 11578 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐴 · 𝐵))) | ||
Theorem | ltmulgt12 11579 | Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴) → (1 < 𝐵 ↔ 𝐴 < (𝐵 · 𝐴))) | ||
Theorem | lemulge11 11580 | Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐴 · 𝐵)) | ||
Theorem | lemulge12 11581 | Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 1 ≤ 𝐵)) → 𝐴 ≤ (𝐵 · 𝐴)) | ||
Theorem | ltdiv1 11582 | Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 < 𝐵 ↔ (𝐴 / 𝐶) < (𝐵 / 𝐶))) | ||
Theorem | lediv1 11583 | Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐶) ≤ (𝐵 / 𝐶))) | ||
Theorem | gt0div 11584 | Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 < 𝐴 ↔ 0 < (𝐴 / 𝐵))) | ||
Theorem | ge0div 11585 | Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐵) → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 𝐵))) | ||
Theorem | divgt0 11586 | The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 < (𝐴 / 𝐵)) | ||
Theorem | divge0 11587 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) | ||
Theorem | mulge0b 11588 | A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 · 𝐵) ↔ ((𝐴 ≤ 0 ∧ 𝐵 ≤ 0) ∨ (0 ≤ 𝐴 ∧ 0 ≤ 𝐵)))) | ||
Theorem | mulle0b 11589 | A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) ≤ 0 ↔ ((𝐴 ≤ 0 ∧ 0 ≤ 𝐵) ∨ (0 ≤ 𝐴 ∧ 𝐵 ≤ 0)))) | ||
Theorem | mulsuble0b 11590 | A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 − 𝐵) · (𝐶 − 𝐵)) ≤ 0 ↔ ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) ∨ (𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴)))) | ||
Theorem | ltmuldiv 11591 | 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltmuldiv2 11592 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) < 𝐵 ↔ 𝐴 < (𝐵 / 𝐶))) | ||
Theorem | ltdivmul 11593 | 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐶 · 𝐵))) | ||
Theorem | ledivmul 11594 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐶 · 𝐵))) | ||
Theorem | ltdivmul2 11595 | 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) < 𝐵 ↔ 𝐴 < (𝐵 · 𝐶))) | ||
Theorem | lt2mul2div 11596 | 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.) |
⊢ (((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) ∧ (𝐶 ∈ ℝ ∧ (𝐷 ∈ ℝ ∧ 0 < 𝐷))) → ((𝐴 · 𝐵) < (𝐶 · 𝐷) ↔ (𝐴 / 𝐷) < (𝐶 / 𝐵))) | ||
Theorem | ledivmul2 11597 | 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 / 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 · 𝐶))) | ||
Theorem | lemuldiv 11598 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐴 · 𝐶) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | lemuldiv2 11599 | 'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (𝐵 / 𝐶))) | ||
Theorem | ltrec 11600 | The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 < 𝐵 ↔ (1 / 𝐵) < (1 / 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |