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