Theorem List for Intuitionistic Logic Explorer - 7501-7600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nppcan2d 7501 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 + 𝐶)) + 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | nppcan3d 7502 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 + 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subsubd 7503 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 − 𝐵) + 𝐶)) |
|
Theorem | subsub2d 7504 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = (𝐴 + (𝐶 − 𝐵))) |
|
Theorem | subsub3d 7505 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 − (𝐵 − 𝐶)) = ((𝐴 + 𝐶) − 𝐵)) |
|
Theorem | subsub4d 7506 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = (𝐴 − (𝐵 + 𝐶))) |
|
Theorem | sub32d 7507 |
Swap the second and third terms in a double subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − 𝐶) = ((𝐴 − 𝐶) − 𝐵)) |
|
Theorem | nnncand 7508 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − (𝐵 − 𝐶)) − 𝐶) = (𝐴 − 𝐵)) |
|
Theorem | nnncan1d 7509 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐴 − 𝐶)) = (𝐶 − 𝐵)) |
|
Theorem | nnncan2d 7510 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) − (𝐵 − 𝐶)) = (𝐴 − 𝐵)) |
|
Theorem | npncan3d 7511 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) + (𝐶 − 𝐴)) = (𝐶 − 𝐵)) |
|
Theorem | pnpcand 7512 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶)) |
|
Theorem | pnpcan2d 7513 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) |
|
Theorem | pnncand 7514 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) |
|
Theorem | ppncand 7515 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subcand 7516 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | subcan2d 7517 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
22-Sep-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | subcanad 7518 |
Cancellation law for subtraction. Deduction form of subcan 7419.
Generalization of subcand 7516. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | subneintrd 7519 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcand 7516. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≠ (𝐴 − 𝐶)) |
|
Theorem | subcan2ad 7520 |
Cancellation law for subtraction. Deduction form of subcan2 7389.
Generalization of subcan2d 7517. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | subneintr2d 7521 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcan2d 7517. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶)) |
|
Theorem | addsub4d 7522 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) |
|
Theorem | subadd4d 7523 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) |
|
Theorem | sub4d 7524 |
Rearrangement of 4 terms in a subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) |
|
Theorem | 2addsubd 7525 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) |
|
Theorem | addsubeq4d 7526 |
Relation between sums and differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) |
|
Theorem | mvlraddd 7527 |
Move LHS right addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 − 𝐵)) |
|
Theorem | mvrraddd 7528 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵) |
|
Theorem | subaddeqd 7529 |
Transfer two terms of a subtraction to an addition in an equality.
(Contributed by Thierry Arnoux, 2-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐶 − 𝐵)) |
|
Theorem | addlsub 7530 |
Left-subtraction: Subtraction of the left summand from the result of an
addition. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 − 𝐵))) |
|
Theorem | addrsub 7531 |
Right-subtraction: Subtraction of the right summand from the result of
an addition. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | subexsub 7532 |
A subtraction law: Exchanging the subtrahend and the result of the
subtraction. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 = (𝐶 − 𝐵) ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | addid0 7533 |
If adding a number to a another number yields the other number, the added
number must be 0. This shows that 0 is the unique (right)
identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ) → ((𝑋 + 𝑌) = 𝑋 ↔ 𝑌 = 0)) |
|
Theorem | addn0nid 7534 |
Adding a nonzero number to a complex number does not yield the complex
number. (Contributed by AV, 17-Jan-2021.)
|
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0) → (𝑋 + 𝑌) ≠ 𝑋) |
|
Theorem | pnpncand 7535 |
Addition/subtraction cancellation law. (Contributed by Scott Fenton,
14-Dec-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + (𝐵 − 𝐶)) + (𝐶 − 𝐵)) = 𝐴) |
|
Theorem | subeqrev 7536 |
Reverse the order of subtraction in an equality. (Contributed by Scott
Fenton, 8-Jul-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) = (𝐶 − 𝐷) ↔ (𝐵 − 𝐴) = (𝐷 − 𝐶))) |
|
Theorem | pncan1 7537 |
Cancellation law for addition and subtraction with 1. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴) |
|
Theorem | npcan1 7538 |
Cancellation law for subtraction and addition with 1. (Contributed by
Alexander van der Vekens, 5-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴) |
|
Theorem | subeq0bd 7539 |
If two complex numbers are equal, their difference is zero. Consequence
of subeq0ad 7485. Converse of subeq0d 7483. Contrapositive of subne0ad 7486.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = 0) |
|
Theorem | renegcld 7540 |
Closure law for negative of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ) |
|
Theorem | resubcld 7541 |
Closure law for subtraction of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
|
Theorem | negf1o 7542* |
Negation is an isomorphism of a subset of the real numbers to the
negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
|
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) |
|
3.3.3 Multiplication
|
|
Theorem | kcnktkm1cn 7543 |
k times k minus 1 is a complex number if k is a complex number.
(Contributed by Alexander van der Vekens, 11-Mar-2018.)
|
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
|
Theorem | muladd 7544 |
Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened
by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | subdi 7545 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdir 7546 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 30-Dec-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | mul02 7547 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 10-Aug-1999.)
|
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) |
|
Theorem | mul02lem2 7548 |
Zero times a real is zero. Although we prove it as a corollary of
mul02 7547, the name is for consistency with the
Metamath Proof Explorer
which proves it before mul02 7547. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) |
|
Theorem | mul01 7549 |
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 | mul02i 7550 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
NM, 23-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 · 𝐴) = 0 |
|
Theorem | mul01i 7551 |
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 | mul02d 7552 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 · 𝐴) = 0) |
|
Theorem | mul01d 7553 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · 0) = 0) |
|
Theorem | ine0 7554 |
The imaginary unit i is not zero. (Contributed by NM,
6-May-1999.)
|
⊢ i ≠ 0 |
|
Theorem | mulneg1 7555 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 14-May-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg2 7556 |
The product with a negative is the negative of the product. (Contributed
by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg12 7557 |
Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵)) |
|
Theorem | mul2neg 7558 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed
by NM, 30-Jul-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
|
Theorem | submul2 7559 |
Convert a subtraction to addition using multiplication by a negative.
(Contributed by NM, 2-Feb-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶))) |
|
Theorem | mulm1 7560 |
Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulsub 7561 |
Product of two differences. (Contributed by NM, 14-Jan-2006.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsub2 7562 |
Swap the order of subtraction in a multiplication. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))) |
|
Theorem | mulm1i 7563 |
Product with minus one is negative. (Contributed by NM,
31-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (-1 · 𝐴) = -𝐴 |
|
Theorem | mulneg1i 7564 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by NM, 10-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 · 𝐵) = -(𝐴 · 𝐵) |
|
Theorem | mulneg2i 7565 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵) |
|
Theorem | mul2negi 7566 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (-𝐴 · -𝐵) = (𝐴 · 𝐵) |
|
Theorem | subdii 7567 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)) |
|
Theorem | subdiri 7568 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) |
|
Theorem | muladdi 7569 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))) |
|
Theorem | mulm1d 7570 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulneg1d 7571 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg2d 7572 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mul2negd 7573 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
|
Theorem | subdid 7574 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdird 7575 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | muladdd 7576 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubd 7577 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubfacd 7578 |
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28-Aug-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵)) |
|
3.3.4 Ordering on reals (cont.)
|
|
Theorem | ltadd2 7579 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2i 7580 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltadd2d 7581 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2dd 7582 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltletrd 7583 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | ltaddneg 7584 |
Adding a negative number to another number decreases it. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) |
|
Theorem | ltaddnegr 7585 |
Adding a negative number to another number decreases it. (Contributed by
AV, 19-Mar-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵)) |
|
Theorem | lelttrdi 7586 |
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 | gt0ne0 7587 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
|
Theorem | lt0ne0 7588 |
A number which is less than zero is not zero. (Contributed by Stefan
O'Rear, 13-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0) |
|
Theorem | ltadd1 7589 |
Addition to both sides of 'less than'. Part of definition 11.2.7(vi) of
[HoTT], p. (varies). (Contributed by NM,
12-Nov-1999.) (Proof shortened
by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶))) |
|
Theorem | leadd1 7590 |
Addition to both sides of 'less than or equal to'. Part of definition
11.2.7(vi) of [HoTT], p. (varies).
(Contributed by NM, 18-Oct-1999.)
(Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))) |
|
Theorem | leadd2 7591 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) |
|
Theorem | ltsubadd 7592 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
|
Theorem | ltsubadd2 7593 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) |
|
Theorem | lesubadd 7594 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 + 𝐵))) |
|
Theorem | lesubadd2 7595 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) |
|
Theorem | ltaddsub 7596 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
|
Theorem | ltaddsub2 7597 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) |
|
Theorem | leaddsub 7598 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) |
|
Theorem | leaddsub2 7599 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) |
|
Theorem | suble 7600 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) |