HomeTheorem List (p. 82 of 141)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 82 of 141) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | addneintr2d 8101 | Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8099. Consequence of addcan2d 8097. (Contributed by David Moews, 28-Feb-2017.) |
             
| ||
| Theorem | 0cnALT 8102 | Alternate proof of 0cn 7905. (Contributed by NM, 19-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
 | ||
| Theorem | negeu 8103* | Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18. (Contributed by NM, 22-Nov-1994.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
![/\](wedge.gif "/\"){kind=small}  
 | ||
| Theorem | subval 8104* |
Value of subtraction, which is the (unique) element such that
.
(Contributed by NM, 4-Aug-2007.) (Revised by Mario
Carneiro, 2-Nov-2013.)
|
| ||
| Theorem | negeq 8105 | Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
 | ||
| Theorem | negeqi 8106 | Equality inference for negatives. (Contributed by NM, 14-Feb-1995.) |
| | ||
| Theorem | negeqd 8107 | Equality deduction for negatives. (Contributed by NM, 14-May-1999.) |
| | ||
| Theorem | nfnegd 8108 | Deduction version of nfneg 8109. (Contributed by NM, 29-Feb-2008.) (Revised by Mario Carneiro, 15-Oct-2016.) |
 | ||
| Theorem | nfneg 8109 | Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
| | ||
| Theorem | csbnegg 8110 | Move class substitution in and out of the negative of a number. (Contributed by NM, 1-Mar-2008.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
   ![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | subcl 8111 | Closure law for subtraction. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 21-Dec-2013.) |
|
| ||
| Theorem | negcl 8112 | Closure law for negative. (Contributed by NM, 6-Aug-2003.) |
| | ||
| Theorem | negicn 8113 |
 is a complex number
(common case). (Contributed by David A.
Wheeler, 7-Dec-2018.)
|
| | ||
| Theorem | subf 8114 | Subtraction is an operation on the complex numbers. (Contributed by NM, 4-Aug-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
   | ||
| Theorem | subadd 8115 | Relationship between subtraction and addition. (Contributed by NM, 20-Jan-1997.) (Revised by Mario Carneiro, 21-Dec-2013.) |
 | ||
| Theorem | subadd2 8116 | Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subsub23 8117 | Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007.) |
|
| ||
| Theorem | pncan 8118 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | pncan2 8119 | Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005.) |
|
| ||
| Theorem | pncan3 8120 | Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005.) |
|
| ||
| Theorem | npcan 8121 | Cancellation law for subtraction. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | addsubass 8122 | Associative-type law for addition and subtraction. (Contributed by NM, 6-Aug-2003.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | addsub 8123 | Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
|
| ||
| Theorem | subadd23 8124 | Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007.) |
|
| ||
| Theorem | addsub12 8125 | Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005.) |
|
| ||
| Theorem | 2addsub 8126 | Law for subtraction and addition. (Contributed by NM, 20-Nov-2005.) |
| ||
| Theorem | addsubeq4 8127 | Relation between sums and differences. (Contributed by Jeff Madsen, 17-Jun-2010.) |
|
| ||
| Theorem | pncan3oi 8128 | Subtraction and addition of equals. Almost but not exactly the same as pncan3i 8189 and pncan 8118, this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand 8224. (Contributed by David A. Wheeler, 11-Oct-2018.) |
|
| ||
| Theorem | mvrraddi 8129 | Move RHS right addition to LHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
|
| ||
| Theorem | mvlladdi 8130 | Move LHS left addition to RHS. (Contributed by David A. Wheeler, 11-Oct-2018.) |
|
| ||
| Theorem | subid 8131 | Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | subid1 8132 | Identity law for subtraction. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | npncan 8133 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
|
| ||
| Theorem | nppcan 8134 | Cancellation law for subtraction. (Contributed by NM, 1-Sep-2005.) |
|
| ||
| Theorem | nnpcan 8135 | Cancellation law for subtraction: ((a-b)-c)+b = a-c holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 24-Mar-2018.) |
|
| ||
| Theorem | nppcan3 8136 | Cancellation law for subtraction. (Contributed by Mario Carneiro, 14-Sep-2015.) |
|
| ||
| Theorem | subcan2 8137 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) |
|
| ||
| Theorem | subeq0 8138 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999.) |
|
| ||
| Theorem | npncan2 8139 | Cancellation law for subtraction. (Contributed by Scott Fenton, 21-Jun-2013.) |
|
| ||
| Theorem | subsub2 8140 | Law for double subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | nncan 8141 | Cancellation law for subtraction. (Contributed by NM, 21-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | subsub 8142 | Law for double subtraction. (Contributed by NM, 13-May-2004.) |
| | ||
| Theorem | nppcan2 8143 | Cancellation law for subtraction. (Contributed by NM, 29-Sep-2005.) |
|
| ||
| Theorem | subsub3 8144 | Law for double subtraction. (Contributed by NM, 27-Jul-2005.) |
| | ||
| Theorem | subsub4 8145 | Law for double subtraction. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | sub32 8146 | Swap the second and third terms in a double subtraction. (Contributed by NM, 19-Aug-2005.) |
|
| ||
| Theorem | nnncan 8147 | Cancellation law for subtraction. (Contributed by NM, 4-Sep-2005.) |
|
| ||
| Theorem | nnncan1 8148 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | nnncan2 8149 | Cancellation law for subtraction. (Contributed by NM, 1-Oct-2005.) |
|
| ||
| Theorem | npncan3 8150 | Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | pnpcan 8151 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | pnpcan2 8152 | Cancellation law for mixed addition and subtraction. (Contributed by Scott Fenton, 9-Jun-2006.) |
|
| ||
| Theorem | pnncan 8153 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | ppncan 8154 | Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005.) |
|
| ||
| Theorem | addsub4 8155 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 4-Mar-2005.) |
|
| ||
| Theorem | subadd4 8156 | Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by NM, 24-Aug-2006.) |
|
| ||
| Theorem | sub4 8157 | Rearrangement of 4 terms in a subtraction. (Contributed by NM, 23-Nov-2007.) |
|
| ||
| Theorem | neg0 8158 | Minus 0 equals 0. (Contributed by NM, 17-Jan-1997.) |
|
| ||
| Theorem | negid 8159 | Addition of a number and its negative. (Contributed by NM, 14-Mar-2005.) |
|
| ||
| Theorem | negsub 8160 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | subneg 8161 | Relationship between subtraction and negative. (Contributed by NM, 10-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | negneg 8162 | A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 12-Jan-2002.) (Revised by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | neg11 8163 | Negative is one-to-one. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | negcon1 8164 | Negative contraposition law. (Contributed by NM, 9-May-2004.) |
|
| ||
| Theorem | negcon2 8165 | Negative contraposition law. (Contributed by NM, 14-Nov-2004.) |
|
| ||
| Theorem | negeq0 8166 | A number is zero iff its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
| | ||
| Theorem | subcan 8167 | Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | negsubdi 8168 | Distribution of negative over subtraction. (Contributed by NM, 15-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | negdi 8169 | Distribution of negative over addition. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | negdi2 8170 | Distribution of negative over addition. (Contributed by NM, 1-Jan-2006.) |
|
| ||
| Theorem | negsubdi2 8171 | Distribution of negative over subtraction. (Contributed by NM, 4-Oct-1999.) |
|
| ||
| Theorem | neg2sub 8172 | Relationship between subtraction and negative. (Contributed by Paul Chapman, 8-Oct-2007.) |
| | ||
| Theorem | renegcl 8173 | Closure law for negative of reals. (Contributed by NM, 20-Jan-1997.) |
 | ||
| Theorem | renegcli 8174 | Closure law for negative of reals. (Note: this inference proof style and the deduction theorem usage in renegcl 8173 is deprecated, but is retained for its demonstration value.) (Contributed by NM, 17-Jan-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| | ||
| Theorem | resubcli 8175 | Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997.) (Revised by Mario Carneiro, 27-May-2016.) |
|
| ||
| Theorem | resubcl 8176 | Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.) |
|
| ||
| Theorem | negreb 8177 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
| | ||
| Theorem | peano2cnm 8178 | "Reverse" second Peano postulate analog for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
  | ||
| Theorem | peano2rem 8179 | "Reverse" second Peano postulate analog for reals. (Contributed by NM, 6-Feb-2007.) |
| | ||
| Theorem | negcli 8180 | Closure law for negative. (Contributed by NM, 26-Nov-1994.) |
| | ||
| Theorem | negidi 8181 | Addition of a number and its negative. (Contributed by NM, 26-Nov-1994.) |
| | ||
| Theorem | negnegi 8182 | A number is equal to the negative of its negative. Theorem I.4 of [Apostol] p. 18. (Contributed by NM, 8-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
| | ||
| Theorem | subidi 8183 | Subtraction of a number from itself. (Contributed by NM, 26-Nov-1994.) |
|
| ||
| Theorem | subid1i 8184 | Identity law for subtraction. (Contributed by NM, 29-May-1999.) |
|
| ||
| Theorem | negne0bi 8185 | A number is nonzero iff its negative is nonzero. (Contributed by NM, 10-Aug-1999.) |
|
| ||
| Theorem | negrebi 8186 | The negative of a real is real. (Contributed by NM, 11-Aug-1999.) |
|
| ||
| Theorem | negne0i 8187 | The negative of a nonzero number is nonzero. (Contributed by NM, 30-Jul-2004.) |
|
| ||
| Theorem | subcli 8188 | Closure law for subtraction. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
|
| ||
| Theorem | pncan3i 8189 | Subtraction and addition of equals. (Contributed by NM, 26-Nov-1994.) |
| | ||
| Theorem | negsubi 8190 | Relationship between subtraction and negative. Theorem I.3 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
|
| ||
| Theorem | subnegi 8191 | Relationship between subtraction and negative. (Contributed by NM, 1-Dec-2005.) |
|
| ||
| Theorem | subeq0i 8192 | If the difference between two numbers is zero, they are equal. (Contributed by NM, 8-May-1999.) |
|
| ||
| Theorem | neg11i 8193 | Negative is one-to-one. (Contributed by NM, 1-Aug-1999.) |
| | ||
| Theorem | negcon1i 8194 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
|
| ||
| Theorem | negcon2i 8195 | Negative contraposition law. (Contributed by NM, 25-Aug-1999.) |
| | ||
| Theorem | negdii 8196 | Distribution of negative over addition. (Contributed by NM, 28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
|
| ||
| Theorem | negsubdii 8197 | Distribution of negative over subtraction. (Contributed by NM, 6-Aug-1999.) |
|
| ||
| Theorem | negsubdi2i 8198 | Distribution of negative over subtraction. (Contributed by NM, 1-Oct-1999.) |
|
| ||
| Theorem | subaddi 8199 | Relationship between subtraction and addition. (Contributed by NM, 26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.) |
|
| ||
| Theorem | subadd2i 8200 | Relationship between subtraction and addition. (Contributed by NM, 15-Dec-2006.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |