Theorem List for Intuitionistic Logic Explorer - 8001-8100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | subidi 8001 |
Subtraction of a number from itself. (Contributed by NM,
26-Nov-1994.)
|
|
|
Theorem | subid1i 8002 |
Identity law for subtraction. (Contributed by NM, 29-May-1999.)
|
|
|
Theorem | negne0bi 8003 |
A number is nonzero iff its negative is nonzero. (Contributed by NM,
10-Aug-1999.)
|
|
|
Theorem | negrebi 8004 |
The negative of a real is real. (Contributed by NM, 11-Aug-1999.)
|
|
|
Theorem | negne0i 8005 |
The negative of a nonzero number is nonzero. (Contributed by NM,
30-Jul-2004.)
|
|
|
Theorem | subcli 8006 |
Closure law for subtraction. (Contributed by NM, 26-Nov-1994.)
(Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | pncan3i 8007 |
Subtraction and addition of equals. (Contributed by NM,
26-Nov-1994.)
|
|
|
Theorem | negsubi 8008 |
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 8009 |
Relationship between subtraction and negative. (Contributed by NM,
1-Dec-2005.)
|
|
|
Theorem | subeq0i 8010 |
If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8-May-1999.)
|
|
|
Theorem | neg11i 8011 |
Negative is one-to-one. (Contributed by NM, 1-Aug-1999.)
|
|
|
Theorem | negcon1i 8012 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
|
|
Theorem | negcon2i 8013 |
Negative contraposition law. (Contributed by NM, 25-Aug-1999.)
|
|
|
Theorem | negdii 8014 |
Distribution of negative over addition. (Contributed by NM,
28-Jul-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | negsubdii 8015 |
Distribution of negative over subtraction. (Contributed by NM,
6-Aug-1999.)
|
|
|
Theorem | negsubdi2i 8016 |
Distribution of negative over subtraction. (Contributed by NM,
1-Oct-1999.)
|
|
|
Theorem | subaddi 8017 |
Relationship between subtraction and addition. (Contributed by NM,
26-Nov-1994.) (Revised by Mario Carneiro, 21-Dec-2013.)
|
|
|
Theorem | subadd2i 8018 |
Relationship between subtraction and addition. (Contributed by NM,
15-Dec-2006.)
|
|
|
Theorem | subaddrii 8019 |
Relationship between subtraction and addition. (Contributed by NM,
16-Dec-2006.)
|
|
|
Theorem | subsub23i 8020 |
Swap subtrahend and result of subtraction. (Contributed by NM,
7-Oct-1999.)
|
|
|
Theorem | addsubassi 8021 |
Associative-type law for subtraction and addition. (Contributed by NM,
16-Sep-1999.)
|
|
|
Theorem | addsubi 8022 |
Law for subtraction and addition. (Contributed by NM, 6-Aug-2003.)
|
|
|
Theorem | subcani 8023 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | subcan2i 8024 |
Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005.)
|
|
|
Theorem | pnncani 8025 |
Cancellation law for mixed addition and subtraction. (Contributed by
NM, 14-Jan-2006.)
|
|
|
Theorem | addsub4i 8026 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by NM, 17-Oct-1999.)
|
|
|
Theorem | 0reALT 8027 |
Alternate proof of 0re 7734. (Contributed by NM, 19-Feb-2005.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
|
|
Theorem | negcld 8028 |
Closure law for negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subidd 8029 |
Subtraction of a number from itself. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subid1d 8030 |
Identity law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negidd 8031 |
Addition of a number and its negative. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negnegd 8032 |
A number is equal to the negative of its negative. Theorem I.4 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negeq0d 8033 |
A number is zero iff its negative is zero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negne0bd 8034 |
A number is nonzero iff its negative is nonzero. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negcon1d 8035 |
Contraposition law for unary minus. Deduction form of negcon1 7982.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | negcon1ad 8036 |
Contraposition law for unary minus. One-way deduction form of
negcon1 7982. (Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | neg11ad 8037 |
The negatives of two complex numbers are equal iff they are equal.
Deduction form of neg11 7981. Generalization of neg11d 8053.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | negned 8038 |
If two complex numbers are unequal, so are their negatives.
Contrapositive of neg11d 8053. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | negne0d 8039 |
The negative of a nonzero number is nonzero. See also negap0d 8360 which
is similar but for apart from zero rather than not equal to zero.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negrebd 8040 |
The negative of a real is real. (Contributed by Mario Carneiro,
28-May-2016.)
|
|
|
Theorem | subcld 8041 |
Closure law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncand 8042 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncan2d 8043 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pncan3d 8044 |
Subtraction and addition of equals. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | npcand 8045 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nncand 8046 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negsubd 8047 |
Relationship between subtraction and negative. Theorem I.3 of [Apostol]
p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subnegd 8048 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subeq0d 8049 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subne0d 8050 |
Two unequal numbers have nonzero difference. See also subap0d 8373 which
is the same thing for apartness rather than negated equality.
(Contributed by Mario Carneiro, 1-Jan-2017.)
|
|
|
Theorem | subeq0ad 8051 |
The difference of two complex numbers is zero iff they are equal.
Deduction form of subeq0 7956. Generalization of subeq0d 8049.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | subne0ad 8052 |
If the difference of two complex numbers is nonzero, they are unequal.
Converse of subne0d 8050. Contrapositive of subeq0bd 8109. (Contributed
by David Moews, 28-Feb-2017.)
|
|
|
Theorem | neg11d 8053 |
If the difference between two numbers is zero, they are equal.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | negdid 8054 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negdi2d 8055 |
Distribution of negative over addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | negsubdid 8056 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | negsubdi2d 8057 |
Distribution of negative over subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | neg2subd 8058 |
Relationship between subtraction and negative. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subaddd 8059 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subadd2d 8060 |
Relationship between subtraction and addition. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubassd 8061 |
Associative-type law for subtraction and addition. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsubd 8062 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subadd23d 8063 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addsub12d 8064 |
Commutative/associative law for addition and subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | npncand 8065 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcand 8066 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcan2d 8067 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nppcan3d 8068 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsubd 8069 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub2d 8070 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub3d 8071 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subsub4d 8072 |
Law for double subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | sub32d 8073 |
Swap the second and third terms in a double subtraction. (Contributed
by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | nnncand 8074 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nnncan1d 8075 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | nnncan2d 8076 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | npncan3d 8077 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | pnpcand 8078 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnpcan2d 8079 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | pnncand 8080 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ppncand 8081 |
Cancellation law for mixed addition and subtraction. (Contributed by
Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subcand 8082 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subcan2d 8083 |
Cancellation law for subtraction. (Contributed by Mario Carneiro,
22-Sep-2016.)
|
|
|
Theorem | subcanad 8084 |
Cancellation law for subtraction. Deduction form of subcan 7985.
Generalization of subcand 8082. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subneintrd 8085 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcand 8082. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subcan2ad 8086 |
Cancellation law for subtraction. Deduction form of subcan2 7955.
Generalization of subcan2d 8083. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | subneintr2d 8087 |
Introducing subtraction on both sides of a statement of inequality.
Contrapositive of subcan2d 8083. (Contributed by David Moews,
28-Feb-2017.)
|
|
|
Theorem | addsub4d 8088 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subadd4d 8089 |
Rearrangement of 4 terms in a mixed addition and subtraction.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | sub4d 8090 |
Rearrangement of 4 terms in a subtraction. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | 2addsubd 8091 |
Law for subtraction and addition. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | addsubeq4d 8092 |
Relation between sums and differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subeqxfrd 8093 |
Transfer two terms of a subtraction in an equality. (Contributed by
Thierry Arnoux, 2-Feb-2020.)
|
|
|
Theorem | mvlraddd 8094 |
Move LHS right addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | mvlladdd 8095 |
Move LHS left addition to RHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | mvrraddd 8096 |
Move RHS right addition to LHS. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | mvrladdd 8097 |
Move RHS left addition to LHS. (Contributed by David A. Wheeler,
11-Oct-2018.)
|
|
|
Theorem | assraddsubd 8098 |
Associate RHS addition-subtraction. (Contributed by David A. Wheeler,
15-Oct-2018.)
|
|
|
Theorem | subaddeqd 8099 |
Transfer two terms of a subtraction to an addition in an equality.
(Contributed by Thierry Arnoux, 2-Feb-2020.)
|
|
|
Theorem | addlsub 8100 |
Left-subtraction: Subtraction of the left summand from the result of an
addition. (Contributed by BJ, 6-Jun-2019.)
|
|