Theorem List for Intuitionistic Logic Explorer - 8301-8400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mulneg2d 8301 |
Product with negative is negative of product. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | mul2negd 8302 |
Product of two negatives. Theorem I.12 of [Apostol] p. 18.
(Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | subdid 8303 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | subdird 8304 |
Distribution of multiplication over subtraction. Theorem I.5 of
[Apostol] p. 18. (Contributed by Mario
Carneiro, 27-May-2016.)
|
|
|
Theorem | muladdd 8305 |
Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mulsubd 8306 |
Product of two differences. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | mulsubfacd 8307 |
Multiplication followed by the subtraction of a factor. (Contributed by
Alexander van der Vekens, 28-Aug-2018.)
|
|
|
4.3.4 Ordering on reals (cont.)
|
|
Theorem | ltadd2 8308 |
Addition to both sides of 'less than'. (Contributed by NM,
12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltadd2i 8309 |
Addition to both sides of 'less than'. (Contributed by NM,
21-Jan-1997.)
|
|
|
Theorem | ltadd2d 8310 |
Addition to both sides of 'less than'. (Contributed by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltadd2dd 8311 |
Addition to both sides of 'less than'. (Contributed by Mario
Carneiro, 30-May-2016.)
|
|
|
Theorem | ltletrd 8312 |
Transitive law deduction for 'less than', 'less than or equal to'.
(Contributed by NM, 9-Jan-2006.)
|
|
|
Theorem | ltaddneg 8313 |
Adding a negative number to another number decreases it. (Contributed by
Glauco Siliprandi, 11-Dec-2019.)
|
|
|
Theorem | ltaddnegr 8314 |
Adding a negative number to another number decreases it. (Contributed by
AV, 19-Mar-2021.)
|
|
|
Theorem | lelttrdi 8315 |
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 8316 |
Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt0ne0 8317 |
A number which is less than zero is not zero. See also lt0ap0 8537 which is
similar but for apartness. (Contributed by Stefan O'Rear,
13-Sep-2014.)
|
|
|
Theorem | ltadd1 8318 |
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 8319 |
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 8320 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
26-Oct-1999.)
|
|
|
Theorem | ltsubadd 8321 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsubadd2 8322 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | lesubadd 8323 |
'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 8324 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 10-Aug-1999.)
|
|
|
Theorem | ltaddsub 8325 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddsub2 8326 |
'Less than' relationship between addition and subtraction. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | leaddsub 8327 |
'Less than or equal to' relationship between addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | leaddsub2 8328 |
'Less than or equal to' relationship between and addition and subtraction.
(Contributed by NM, 6-Apr-2005.)
|
|
|
Theorem | suble 8329 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|
|
|
Theorem | lesub 8330 |
Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
(Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltsub23 8331 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 4-Oct-1999.)
|
|
|
Theorem | ltsub13 8332 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 17-Nov-2004.)
|
|
|
Theorem | le2add 8333 |
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 8334 |
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 8335 |
Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|
|
|
Theorem | leltadd 8336 |
Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|
|
|
Theorem | addgt0 8337 |
The sum of 2 positive numbers is positive. (Contributed by NM,
1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0 8338 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgtge0 8339 |
The sum of nonnegative and positive numbers is positive. (Contributed by
NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addge0 8340 |
The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM,
17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddpos 8341 |
Adding a positive number to another number increases it. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | ltaddpos2 8342 |
Adding a positive number to another number increases it. (Contributed by
NM, 8-Apr-2005.)
|
|
|
Theorem | ltsubpos 8343 |
Subtracting a positive number from another number decreases it.
(Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
|
|
Theorem | posdif 8344 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 17-Nov-2004.)
|
|
|
Theorem | lesub1 8345 |
Subtraction from both sides of 'less than or equal to'. (Contributed by
NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lesub2 8346 |
Subtraction of both sides of 'less than or equal to'. (Contributed by NM,
29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsub1 8347 |
Subtraction from both sides of 'less than'. (Contributed by FL,
3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | ltsub2 8348 |
Subtraction of both sides of 'less than'. (Contributed by NM,
29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lt2sub 8349 |
Subtracting both sides of two 'less than' relations. (Contributed by
Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | le2sub 8350 |
Subtracting both sides of two 'less than or equal to' relations.
(Contributed by Mario Carneiro, 14-Apr-2016.)
|
|
|
Theorem | ltneg 8351 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 27-Aug-1999.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | ltnegcon1 8352 |
Contraposition of negative in 'less than'. (Contributed by NM,
8-Nov-2004.)
|
|
|
Theorem | ltnegcon2 8353 |
Contraposition of negative in 'less than'. (Contributed by Mario
Carneiro, 25-Feb-2015.)
|
|
|
Theorem | leneg 8354 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | lenegcon1 8355 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 10-May-2004.)
|
|
|
Theorem | lenegcon2 8356 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 8-Oct-2005.)
|
|
|
Theorem | lt0neg1 8357 |
Comparison of a number and its negative to zero. Theorem I.23 of
[Apostol] p. 20. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lt0neg2 8358 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg1 8359 |
Comparison of a number and its negative to zero. (Contributed by NM,
10-May-2004.)
|
|
|
Theorem | le0neg2 8360 |
Comparison of a number and its negative to zero. (Contributed by NM,
24-Aug-1999.)
|
|
|
Theorem | addge01 8361 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 21-Feb-2005.)
|
|
|
Theorem | addge02 8362 |
A number is less than or equal to itself plus a nonnegative number.
(Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | add20 8363 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro,
27-May-2016.)
|
|
|
Theorem | subge0 8364 |
Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | suble0 8365 |
Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof
shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | leaddle0 8366 |
The sum of a real number and a second real number is less then the real
number iff the second real number is negative. (Contributed by Alexander
van der Vekens, 30-May-2018.)
|
|
|
Theorem | subge02 8367 |
Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|
|
|
Theorem | lesub0 8368 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | mullt0 8369 |
The product of two negative numbers is positive. (Contributed by Jeff
Hankins, 8-Jun-2009.)
|
|
|
Theorem | 0le1 8370 |
0 is less than or equal to 1. (Contributed by Mario Carneiro,
29-Apr-2015.)
|
|
|
Theorem | ltordlem 8371* |
Lemma for eqord1 8372. (Contributed by Mario Carneiro,
14-Jun-2014.)
|
|
|
Theorem | eqord1 8372* |
A strictly increasing real function on a subset of is
one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised
by Jim Kingdon, 20-Dec-2022.)
|
|
|
Theorem | eqord2 8373* |
A strictly decreasing real function on a subset of is one-to-one.
(Contributed by Mario Carneiro, 14-Jun-2014.)
|
|
|
Theorem | leidi 8374 |
'Less than or equal to' is reflexive. (Contributed by NM,
18-Aug-1999.)
|
|
|
Theorem | gt0ne0i 8375 |
Positive means nonzero (useful for ordering theorems involving
division). (Contributed by NM, 16-Sep-1999.)
|
|
|
Theorem | gt0ne0ii 8376 |
Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|
|
|
Theorem | addgt0i 8377 |
Addition of 2 positive numbers is positive. (Contributed by NM,
16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addge0i 8378 |
Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM,
28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | addgegt0i 8379 |
Addition of nonnegative and positive numbers is positive. (Contributed
by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|
|
|
Theorem | addgt0ii 8380 |
Addition of 2 positive numbers is positive. (Contributed by NM,
18-May-1999.)
|
|
|
Theorem | add20i 8381 |
Two nonnegative numbers are zero iff their sum is zero. (Contributed by
NM, 28-Jul-1999.)
|
|
|
Theorem | ltnegi 8382 |
Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | lenegi 8383 |
Negative of both sides of 'less than or equal to'. (Contributed by NM,
1-Aug-1999.)
|
|
|
Theorem | ltnegcon2i 8384 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lesub0i 8385 |
Lemma to show a nonnegative number is zero. (Contributed by NM,
8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|
|
|
Theorem | ltaddposi 8386 |
Adding a positive number to another number increases it. (Contributed
by NM, 25-Aug-1999.)
|
|
|
Theorem | posdifi 8387 |
Comparison of two numbers whose difference is positive. (Contributed by
NM, 19-Aug-2001.)
|
|
|
Theorem | ltnegcon1i 8388 |
Contraposition of negative in 'less than'. (Contributed by NM,
14-May-1999.)
|
|
|
Theorem | lenegcon1i 8389 |
Contraposition of negative in 'less than or equal to'. (Contributed by
NM, 6-Apr-2005.)
|
|
|
Theorem | subge0i 8390 |
Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|
|
|
Theorem | ltadd1i 8391 |
Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | leadd1i 8392 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
|
|
Theorem | leadd2i 8393 |
Addition to both sides of 'less than or equal to'. (Contributed by NM,
11-Aug-1999.)
|
|
|
Theorem | ltsubaddi 8394 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
|
|
Theorem | lesubaddi 8395 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon,
19-Nov-2011.)
|
|
|
Theorem | ltsubadd2i 8396 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 21-Jan-1997.)
|
|
|
Theorem | lesubadd2i 8397 |
'Less than or equal to' relationship between subtraction and addition.
(Contributed by NM, 3-Aug-1999.)
|
|
|
Theorem | ltaddsubi 8398 |
'Less than' relationship between subtraction and addition. (Contributed
by NM, 14-May-1999.)
|
|
|
Theorem | lt2addi 8399 |
Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20.
(Contributed by NM, 14-May-1999.)
|
|
|
Theorem | le2addi 8400 |
Adding both side of two inequalities. (Contributed by NM,
16-Sep-1999.)
|
|