Theorem List for Intuitionistic Logic Explorer - 8101-8200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | npcand 8101 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | nncand 8102 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negsubd 8103 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subnegd 8104 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subeq0d 8105 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![0 0](0.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subne0d 8106 |
Two unequal numbers have nonzero difference. See also subap0d 8430 which
is the same thing for apartness rather than negated equality.
(Contributed by Mario Carneiro, 1-Jan-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | subeq0ad 8107 |
The difference of two complex numbers is zero iff they are equal.
Deduction form of subeq0 8012. Generalization of subeq0d 8105.
(Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subne0ad 8108 |
If the difference of two complex numbers is nonzero, they are unequal.
Converse of subne0d 8106. Contrapositive of subeq0bd 8165. (Contributed
by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![0 0](0.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | neg11d 8109 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | negdid 8110 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negdi2d 8111 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negsubdid 8112 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | negsubdi2d 8113 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | neg2subd 8114 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subaddd 8115 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subadd2d 8116 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif)
![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsubassd 8117 |
Associative-type law for subtraction and addition. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsubd 8118 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subadd23d 8119 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsub12d 8120 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | npncand 8121 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcand 8122 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif)
![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcan2d 8123 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nppcan3d 8124 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsubd 8125 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsub2d 8126 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsub3d 8127 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subsub4d 8128 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | sub32d 8129 |
Swap the second and third terms in a double subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncand 8130 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncan1d 8131 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | nnncan2d 8132 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | npncan3d 8133 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnpcand 8134 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnpcan2d 8135 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pnncand 8136 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | ppncand 8137 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subcand 8138 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | subcan2d 8139 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
22-Sep-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subcanad 8140 |
Cancellation law for subtraction. Deduction form of subcan 8041.
Generalization of subcand 8138. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subneintrd 8141 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcand 8138. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subcan2ad 8142 |
Cancellation law for subtraction. Deduction form of subcan2 8011.
Generalization of subcan2d 8139. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subneintr2d 8143 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcan2d 8139. (Contributed by David Moews,
28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsub4d 8144 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subadd4d 8145 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | sub4d 8146 |
Rearrangement of 4 terms in a subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | 2addsubd 8147 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![D D](_cd.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addsubeq4d 8148 |
Relation between sums and differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subeqxfrd 8149 |
Transfer two terms of a subtraction in an equality. (Contributed by
Thierry Arnoux, 2-Feb-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mvlraddd 8150 |
Move LHS right addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mvlladdd 8151 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mvrraddd 8152 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | mvrladdd 8153 |
Move RHS left addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | assraddsubd 8154 |
Associate RHS addition-subtraction. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subaddeqd 8155 |
Transfer two terms of a subtraction to an addition in an equality.
(Contributed by Thierry Arnoux, 2-Feb-2020.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addlsub 8156 |
Left-subtraction: Subtraction of the left summand from the result of an
addition. (Contributed by BJ, 6-Jun-2019.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addrsub 8157 |
Right-subtraction: Subtraction of the right summand from the result of
an addition. (Contributed by BJ, 6-Jun-2019.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subexsub 8158 |
A subtraction law: Exchanging the subtrahend and the result of the
subtraction. (Contributed by BJ, 6-Jun-2019.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | addid0 8159 |
If adding a number to a another number yields the other number, the added
number must be .
This shows that is the
unique (right)
identity of the complex numbers. (Contributed by AV, 17-Jan-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![Y Y](_cy.gif)
![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
|
Theorem | addn0nid 8160 |
Adding a nonzero number to a complex number does not yield the complex
number. (Contributed by AV, 17-Jan-2021.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![( (](lp.gif) ![Y Y](_cy.gif) ![X X](_cx.gif) ![) )](rp.gif) |
|
Theorem | pnpncand 8161 |
Addition/subtraction cancellation law. (Contributed by Scott Fenton,
14-Dec-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subeqrev 8162 |
Reverse the order of subtraction in an equality. (Contributed by Scott
Fenton, 8-Jul-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | pncan1 8163 |
Cancellation law for addition and subtraction with 1. (Contributed by
Alexander van der Vekens, 3-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | npcan1 8164 |
Cancellation law for subtraction and addition with 1. (Contributed by
Alexander van der Vekens, 5-Oct-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | subeq0bd 8165 |
If two complex numbers are equal, their difference is zero. Consequence
of subeq0ad 8107. Converse of subeq0d 8105. Contrapositive of subne0ad 8108.
(Contributed by David Moews, 28-Feb-2017.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | renegcld 8166 |
Closure law for negative of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | resubcld 8167 |
Closure law for subtraction of reals. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
|
Theorem | negf1o 8168* |
Negation is an isomorphism of a subset of the real numbers to the
negated elements of the subset. (Contributed by AV, 9-Aug-2020.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![x x](_x.gif) ![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![{ {](lbrace.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
|
4.3.3 Multiplication
|
|
Theorem | kcnktkm1cn 8169 |
k times k minus 1 is a complex number if k is a complex number.
(Contributed by Alexander van der Vekens, 11-Mar-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
|
Theorem | muladd 8170 |
Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened
by Andrew Salmon, 19-Nov-2011.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subdi 8171 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 18-Nov-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subdir 8172 |
Distribution of multiplication over subtraction. Theorem I.5 of [Apostol]
p. 18. (Contributed by NM, 30-Dec-2005.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mul02 8173 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 10-Aug-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | mul02lem2 8174 |
Zero times a real is zero. Although we prove it as a corollary of
mul02 8173, the name is for consistency with the
Metamath Proof Explorer
which proves it before mul02 8173. (Contributed by Scott Fenton,
3-Jan-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | mul01 8175 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | mul02i 8176 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
NM, 23-Nov-1994.)
|
![( (](lp.gif) ![A A](_ca.gif) ![0 0](0.gif) |
|
Theorem | mul01i 8177 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|
![( (](lp.gif) ![0 0](0.gif)
![0 0](0.gif) |
|
Theorem | mul02d 8178 |
Multiplication by 0. Theorem I.6 of [Apostol]
p. 18. (Contributed by
Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | mul01d 8179 |
Multiplication by .
Theorem I.6 of [Apostol] p. 18. (Contributed
by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | ine0 8180 |
The imaginary unit
is not zero. (Contributed by NM,
6-May-1999.)
|
![0 0](0.gif) |
|
Theorem | mulneg1 8181 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulneg2 8182 |
The product with a negative is the negative of the product. (Contributed
by NM, 30-Jul-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulneg12 8183 |
Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mul2neg 8184 |
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.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | submul2 8185 |
Convert a subtraction to addition using multiplication by a negative.
(Contributed by NM, 2-Feb-2007.)
|
![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![-u -u](shortminus.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulm1 8186 |
Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mulsub 8187 |
Product of two differences. (Contributed by NM, 14-Jan-2006.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulsub2 8188 |
Swap the order of subtraction in a multiplication. (Contributed by Scott
Fenton, 24-Jun-2013.)
|
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulm1i 8189 |
Product with minus one is negative. (Contributed by NM,
31-Jul-1999.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) |
|
Theorem | mulneg1i 8190 |
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.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | mulneg2i 8191 |
Product with negative is negative of product. (Contributed by NM,
31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | mul2negi 8192 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | subdii 8193 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
26-Nov-1994.)
|
![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subdiri 8194 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by NM,
8-May-1999.)
|
![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | muladdi 8195 |
Product of two sums. (Contributed by NM, 17-May-1999.)
|
![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif)
![D D](_cd.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulm1d 8196 |
Product with minus one is negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | mulneg1d 8197 |
Product with negative is negative of product. Theorem I.12 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![B B](_cb.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mulneg2d 8198 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | mul2negd 8199 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![-u -u](shortminus.gif) ![B B](_cb.gif)
![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
|
Theorem | subdid 8200 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |