Theorem List for Intuitionistic Logic Explorer - 8301-8400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pnpcand 8301 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 + 𝐶)) = (𝐵 − 𝐶)) |
|
Theorem | pnpcan2d 8302 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐶) − (𝐵 + 𝐶)) = (𝐴 − 𝐵)) |
|
Theorem | pnncand 8303 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐴 − 𝐶)) = (𝐵 + 𝐶)) |
|
Theorem | ppncand 8304 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) + (𝐶 − 𝐵)) = (𝐴 + 𝐶)) |
|
Theorem | subcand 8305 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐴 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = 𝐶) |
|
Theorem | subcan2d 8306 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
22-Sep-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) |
|
Theorem | subcanad 8307 |
Cancellation law for subtraction. Deduction form of subcan 8208.
Generalization of subcand 8305. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) = (𝐴 − 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | subneintrd 8308 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcand 8305. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ≠ (𝐴 − 𝐶)) |
|
Theorem | subcan2ad 8309 |
Cancellation law for subtraction. Deduction form of subcan2 8178.
Generalization of subcan2d 8306. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐶) = (𝐵 − 𝐶) ↔ 𝐴 = 𝐵)) |
|
Theorem | subneintr2d 8310 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcan2d 8306. (Contributed by David Moews,
28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) ≠ (𝐵 − 𝐶)) |
|
Theorem | addsub4d 8311 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) − (𝐶 + 𝐷)) = ((𝐴 − 𝐶) + (𝐵 − 𝐷))) |
|
Theorem | subadd4d 8312 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 + 𝐷) − (𝐵 + 𝐶))) |
|
Theorem | sub4d 8313 |
Rearrangement of 4 terms in a subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) − (𝐶 − 𝐷)) = ((𝐴 − 𝐶) − (𝐵 − 𝐷))) |
|
Theorem | 2addsubd 8314 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → (((𝐴 + 𝐵) + 𝐶) − 𝐷) = (((𝐴 + 𝐶) − 𝐷) + 𝐵)) |
|
Theorem | addsubeq4d 8315 |
Relation between sums and differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐶 − 𝐴) = (𝐵 − 𝐷))) |
|
Theorem | subeqxfrd 8316 |
Transfer two terms of a subtraction in an equality. (Contributed by
Thierry Arnoux, 2-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = (𝐵 − 𝐷)) |
|
Theorem | mvlraddd 8317 |
Move LHS right addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 = (𝐶 − 𝐵)) |
|
Theorem | mvlladdd 8318 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 − 𝐴)) |
|
Theorem | mvrraddd 8319 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵) |
|
Theorem | mvrladdd 8320 |
Move RHS left addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) |
|
Theorem | assraddsubd 8321 |
Associate RHS addition-subtraction. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = ((𝐵 + 𝐶) − 𝐷)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐵 + (𝐶 − 𝐷))) |
|
Theorem | subaddeqd 8322 |
Transfer two terms of a subtraction to an addition in an equality.
(Contributed by Thierry Arnoux, 2-Feb-2020.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = (𝐶 + 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐷) = (𝐶 − 𝐵)) |
|
Theorem | addlsub 8323 |
Left-subtraction: Subtraction of the left summand from the result of an
addition. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐴 = (𝐶 − 𝐵))) |
|
Theorem | addrsub 8324 |
Right-subtraction: Subtraction of the right summand from the result of
an addition. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) = 𝐶 ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | subexsub 8325 |
A subtraction law: Exchanging the subtrahend and the result of the
subtraction. (Contributed by BJ, 6-Jun-2019.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 = (𝐶 − 𝐵) ↔ 𝐵 = (𝐶 − 𝐴))) |
|
Theorem | addid0 8326 |
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 8327 |
Adding a nonzero number to a complex number does not yield the complex
number. (Contributed by AV, 17-Jan-2021.)
|
⊢ ((𝑋 ∈ ℂ ∧ 𝑌 ∈ ℂ ∧ 𝑌 ≠ 0) → (𝑋 + 𝑌) ≠ 𝑋) |
|
Theorem | pnpncand 8328 |
Addition/subtraction cancellation law. (Contributed by Scott Fenton,
14-Dec-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + (𝐵 − 𝐶)) + (𝐶 − 𝐵)) = 𝐴) |
|
Theorem | subeqrev 8329 |
Reverse the order of subtraction in an equality. (Contributed by Scott
Fenton, 8-Jul-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) = (𝐶 − 𝐷) ↔ (𝐵 − 𝐴) = (𝐷 − 𝐶))) |
|
Theorem | pncan1 8330 |
Cancellation law for addition and subtraction with 1. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1) − 1) = 𝐴) |
|
Theorem | npcan1 8331 |
Cancellation law for subtraction and addition with 1. (Contributed by
Alexander van der Vekens, 5-Oct-2018.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴) |
|
Theorem | subeq0bd 8332 |
If two complex numbers are equal, their difference is zero. Consequence
of subeq0ad 8274. Converse of subeq0d 8272. Contrapositive of subne0ad 8275.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) = 0) |
|
Theorem | renegcld 8333 |
Closure law for negative of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ)
⇒ ⊢ (𝜑 → -𝐴 ∈ ℝ) |
|
Theorem | resubcld 8334 |
Closure law for subtraction of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ) |
|
Theorem | negf1o 8335* |
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→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) |
|
4.3.3 Multiplication
|
|
Theorem | kcnktkm1cn 8336 |
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 8337 |
Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened
by Andrew Salmon, 19-Nov-2011.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | subdi 8338 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 18-Nov-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdir 8339 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 30-Dec-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | mul02 8340 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 10-Aug-1999.)
|
⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0) |
|
Theorem | mul02lem2 8341 |
Zero times a real is zero. Although we prove it as a corollary of
mul02 8340, the name is for consistency with the
Metamath Proof Explorer
which proves it before mul02 8340. (Contributed by Scott Fenton,
3-Jan-2013.)
|
⊢ (𝐴 ∈ ℝ → (0 · 𝐴) = 0) |
|
Theorem | mul01 8342 |
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 8343 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
NM, 23-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (0 · 𝐴) = 0 |
|
Theorem | mul01i 8344 |
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 8345 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (0 · 𝐴) = 0) |
|
Theorem | mul01d 8346 |
Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed
by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · 0) = 0) |
|
Theorem | ine0 8347 |
The imaginary unit i is not zero. (Contributed by NM,
6-May-1999.)
|
⊢ i ≠ 0 |
|
Theorem | mulneg1 8348 |
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 8349 |
The product with a negative is the negative of the product. (Contributed
by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg12 8350 |
Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (-𝐴 · 𝐵) = (𝐴 · -𝐵)) |
|
Theorem | mul2neg 8351 |
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 8352 |
Convert a subtraction to addition using multiplication by a negative.
(Contributed by NM, 2-Feb-2007.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 − (𝐵 · 𝐶)) = (𝐴 + (𝐵 · -𝐶))) |
|
Theorem | mulm1 8353 |
Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|
⊢ (𝐴 ∈ ℂ → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulsub 8354 |
Product of two differences. (Contributed by NM, 14-Jan-2006.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsub2 8355 |
Swap the order of subtraction in a multiplication. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = ((𝐵 − 𝐴) · (𝐷 − 𝐶))) |
|
Theorem | mulm1i 8356 |
Product with minus one is negative. (Contributed by NM,
31-Jul-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (-1 · 𝐴) = -𝐴 |
|
Theorem | mulneg1i 8357 |
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 8358 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ (𝐴 · -𝐵) = -(𝐴 · 𝐵) |
|
Theorem | mul2negi 8359 |
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 8360 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶)) |
|
Theorem | subdiri 8361 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶)) |
|
Theorem | muladdi 8362 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℂ & ⊢ 𝐷 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵))) |
|
Theorem | mulm1d 8363 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (-1 · 𝐴) = -𝐴) |
|
Theorem | mulneg1d 8364 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · 𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mulneg2d 8365 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · -𝐵) = -(𝐴 · 𝐵)) |
|
Theorem | mul2negd 8366 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → (-𝐴 · -𝐵) = (𝐴 · 𝐵)) |
|
Theorem | subdid 8367 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴 · (𝐵 − 𝐶)) = ((𝐴 · 𝐵) − (𝐴 · 𝐶))) |
|
Theorem | subdird 8368 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · 𝐶) = ((𝐴 · 𝐶) − (𝐵 · 𝐶))) |
|
Theorem | muladdd 8369 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) + ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubd 8370 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐷 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 − 𝐷)) = (((𝐴 · 𝐶) + (𝐷 · 𝐵)) − ((𝐴 · 𝐷) + (𝐶 · 𝐵)))) |
|
Theorem | mulsubfacd 8371 |
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28-Aug-2018.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ)
⇒ ⊢ (𝜑 → ((𝐴 · 𝐵) − 𝐵) = ((𝐴 − 1) · 𝐵)) |
|
4.3.4 Ordering on reals (cont.)
|
|
Theorem | ltadd2 8372 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2i 8373 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐶 ∈
ℝ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltadd2d 8374 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ)
⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐶 + 𝐴) < (𝐶 + 𝐵))) |
|
Theorem | ltadd2dd 8375 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐶 + 𝐴) < (𝐶 + 𝐵)) |
|
Theorem | ltletrd 8376 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐵)
& ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 < 𝐶) |
|
Theorem | ltaddneg 8377 |
Adding a negative number to another number decreases it. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐵 + 𝐴) < 𝐵)) |
|
Theorem | ltaddnegr 8378 |
Adding a negative number to another number decreases it. (Contributed by
AV, 19-Mar-2021.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 0 ↔ (𝐴 + 𝐵) < 𝐵)) |
|
Theorem | lelttrdi 8379 |
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 8380 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0) |
|
Theorem | lt0ne0 8381 |
A number which is less than zero is not zero. See also lt0ap0 8601 which is
similar but for apartness. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 ≠ 0) |
|
Theorem | ltadd1 8382 |
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 8383 |
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 8384 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))) |
|
Theorem | ltsubadd 8385 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 + 𝐵))) |
|
Theorem | ltsubadd2 8386 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) |
|
Theorem | lesubadd 8387 |
'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 8388 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐵 + 𝐶))) |
|
Theorem | ltaddsub 8389 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐴 < (𝐶 − 𝐵))) |
|
Theorem | ltaddsub2 8390 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) < 𝐶 ↔ 𝐵 < (𝐶 − 𝐴))) |
|
Theorem | leaddsub 8391 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐴 ≤ (𝐶 − 𝐵))) |
|
Theorem | leaddsub2 8392 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) ≤ 𝐶 ↔ 𝐵 ≤ (𝐶 − 𝐴))) |
|
Theorem | suble 8393 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) ≤ 𝐶 ↔ (𝐴 − 𝐶) ≤ 𝐵)) |
|
Theorem | lesub 8394 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ (𝐵 − 𝐶) ↔ 𝐶 ≤ (𝐵 − 𝐴))) |
|
Theorem | ltsub23 8395 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 𝐵) < 𝐶 ↔ (𝐴 − 𝐶) < 𝐵)) |
|
Theorem | ltsub13 8396 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < (𝐵 − 𝐶) ↔ 𝐶 < (𝐵 − 𝐴))) |
|
Theorem | le2add 8397 |
Adding both sides of two 'less than or equal to' relations. (Contributed
by NM, 17-Apr-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) |
|
Theorem | lt2add 8398 |
Adding both sides of two 'less than' relations. Theorem I.25 of [Apostol]
p. 20. (Contributed by NM, 15-Aug-1999.) (Proof shortened by Mario
Carneiro, 27-May-2016.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | ltleadd 8399 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |
|
Theorem | leltadd 8400 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 + 𝐵) < (𝐶 + 𝐷))) |