P. 88 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	muladd 8701	Product of two sums. (Contributed by NM, 14-Jan-2006.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	subdi 8702	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
Theorem	subdir 8703	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 30-Dec-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) ) )
Theorem	mul02 8704	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 10-Aug-1999.)
|- ( A e. CC -> ( 0 x. A ) = 0 )
Theorem	mul02lem2 8705	Zero times a real is zero. Although we prove it as a corollary of mul02 8704, the name is for consistency with the Metamath Proof Explorer which proves it before mul02 8704. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. RR -> ( 0 x. A ) = 0 )
Theorem	mul01 8706	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 15-May-1999.) (Revised by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( A x. 0 ) = 0 )
Theorem	mul02i 8707	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   =>    |- ( 0 x. A ) = 0
Theorem	mul01i 8708	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>    |- ( A x. 0 ) = 0
Theorem	mul02d 8709	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 x. A ) = 0 )
Theorem	mul01d 8710	Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A x. 0 ) = 0 )
Theorem	ine0 8711	The imaginary unit _i is not zero. (Contributed by NM, 6-May-1999.)
|- _i =/= 0
Theorem	mulneg1 8712	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.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = -u ( A x. B ) )
Theorem	mulneg2 8713	The product with a negative is the negative of the product. (Contributed by NM, 30-Jul-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. -u B ) = -u ( A x. B ) )
Theorem	mulneg12 8714	Swap the negative sign in a product. (Contributed by NM, 30-Jul-2004.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. B ) = ( A x. -u B ) )
Theorem	mul2neg 8715	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.)
|- ( ( A e. CC /\ B e. CC ) -> ( -u A x. -u B ) = ( A x. B ) )
Theorem	submul2 8716	Convert a subtraction to addition using multiplication by a negative. (Contributed by NM, 2-Feb-2007.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B x. C ) ) = ( A + ( B x. -u C ) ) )
Theorem	mulm1 8717	Product with minus one is negative. (Contributed by NM, 16-Nov-1999.)
|- ( A e. CC -> ( -u 1 x. A ) = -u A )
Theorem	mulsub 8718	Product of two differences. (Contributed by NM, 14-Jan-2006.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	mulsub2 8719	Swap the order of subtraction in a multiplication. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A - B ) x. ( C - D ) ) = ( ( B - A ) x. ( D - C ) ) )
Theorem	mulm1i 8720	Product with minus one is negative. (Contributed by NM, 31-Jul-1999.)
|- A e. CC   =>    |- ( -u 1 x. A ) = -u A
Theorem	mulneg1i 8721	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.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A x. B ) = -u ( A x. B )
Theorem	mulneg2i 8722	Product with negative is negative of product. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. -u B ) = -u ( A x. B )
Theorem	mul2negi 8723	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by NM, 14-Feb-1995.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. CC   &    |- B e. CC   =>    |- ( -u A x. -u B ) = ( A x. B )
Theorem	subdii 8724	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 26-Nov-1994.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) )
Theorem	subdiri 8725	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by NM, 8-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) )
Theorem	muladdi 8726	Product of two sums. (Contributed by NM, 17-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) )
Theorem	mulm1d 8727	Product with minus one is negative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( -u 1 x. A ) = -u A )
Theorem	mulneg1d 8728	Product with negative is negative of product. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A x. B ) = -u ( A x. B ) )
Theorem	mulneg2d 8729	Product with negative is negative of product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. -u B ) = -u ( A x. B ) )
Theorem	mul2negd 8730	Product of two negatives. Theorem I.12 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( -u A x. -u B ) = ( A x. B ) )
Theorem	subdid 8731	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )
Theorem	subdird 8732	Distribution of multiplication over subtraction. Theorem I.5 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) ) )
Theorem	muladdd 8733	Product of two sums. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A + B ) x. ( C + D ) ) = ( ( ( A x. C ) + ( D x. B ) ) + ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	mulsubd 8734	Product of two differences. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) x. ( C - D ) ) = ( ( ( A x. C ) + ( D x. B ) ) - ( ( A x. D ) + ( C x. B ) ) ) )
Theorem	muls1d 8735	Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A x. ( B - 1 ) ) = ( ( A x. B ) - A ) )
Theorem	mulsubfacd 8736	Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) )
4.3.4  Ordering on reals (cont.)
Theorem	ltadd2 8737	Addition to both sides of 'less than'. (Contributed by NM, 12-Nov-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	ltadd2i 8738	Addition to both sides of 'less than'. (Contributed by NM, 21-Jan-1997.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( C + A ) < ( C + B ) )
Theorem	ltadd2d 8739	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( C + A ) < ( C + B ) ) )
Theorem	ltadd2dd 8740	Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C + A ) < ( C + B ) )
Theorem	ltletrd 8741	Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A < C )
Theorem	ltaddneg 8742	Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < B ) )
Theorem	ltaddnegr 8743	Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( A + B ) < B ) )
Theorem	lelttrdi 8744	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.)
|- ( ph -> ( A e. RR /\ B e. RR /\ C e. RR ) )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> ( A < B -> A < C ) )
Theorem	gt0ne0 8745	Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
Theorem	lt0ne0 8746	A number which is less than zero is not zero. See also lt0ap0 8966 which is similar but for apartness. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. RR /\ A < 0 ) -> A =/= 0 )
Theorem	ltadd1 8747	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.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( A + C ) < ( B + C ) ) )
Theorem	leadd1 8748	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.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( A + C ) <_ ( B + C ) ) )
Theorem	leadd2 8749	Addition to both sides of 'less than or equal to'. (Contributed by NM, 26-Oct-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( C + A ) <_ ( C + B ) ) )
Theorem	ltsubadd 8750	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) < C <-> A < ( C + B ) ) )
Theorem	ltsubadd2 8751	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) < C <-> A < ( B + C ) ) )
Theorem	lesubadd 8752	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( C + B ) ) )
Theorem	lesubadd2 8753	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 10-Aug-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> A <_ ( B + C ) ) )
Theorem	ltaddsub 8754	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) < C <-> A < ( C - B ) ) )
Theorem	ltaddsub2 8755	'Less than' relationship between addition and subtraction. (Contributed by NM, 17-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) < C <-> B < ( C - A ) ) )
Theorem	leaddsub 8756	'Less than or equal to' relationship between addition and subtraction. (Contributed by NM, 6-Apr-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) <_ C <-> A <_ ( C - B ) ) )
Theorem	leaddsub2 8757	'Less than or equal to' relationship between and addition and subtraction. (Contributed by NM, 6-Apr-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + B ) <_ C <-> B <_ ( C - A ) ) )
Theorem	suble 8758	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ C <-> ( A - C ) <_ B ) )
Theorem	lesub 8759	Swap subtrahends in an inequality. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ ( B - C ) <-> C <_ ( B - A ) ) )
Theorem	ltsub23 8760	'Less than' relationship between subtraction and addition. (Contributed by NM, 4-Oct-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) < C <-> ( A - C ) < B ) )
Theorem	ltsub13 8761	'Less than' relationship between subtraction and addition. (Contributed by NM, 17-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < ( B - C ) <-> C < ( B - A ) ) )
Theorem	le2add 8762	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.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) ) )
Theorem	lt2add 8763	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.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) ) )
Theorem	ltleadd 8764	Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B <_ D ) -> ( A + B ) < ( C + D ) ) )
Theorem	leltadd 8765	Adding both sides of two orderings. (Contributed by NM, 15-Aug-2008.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ B < D ) -> ( A + B ) < ( C + D ) ) )
Theorem	addgt0 8766	The sum of 2 positive numbers is positive. (Contributed by NM, 1-Jun-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A + B ) )
Theorem	addgegt0 8767	The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 < B ) ) -> 0 < ( A + B ) )
Theorem	addgtge0 8768	The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 <_ B ) ) -> 0 < ( A + B ) )
Theorem	addge0 8769	The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A + B ) )
Theorem	ltaddpos 8770	Adding a positive number to another number increases it. (Contributed by NM, 17-Nov-2004.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( B + A ) ) )
Theorem	ltaddpos2 8771	Adding a positive number to another number increases it. (Contributed by NM, 8-Apr-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> B < ( A + B ) ) )
Theorem	ltsubpos 8772	Subtracting a positive number from another number decreases it. (Contributed by NM, 17-Nov-2004.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> ( B - A ) < B ) )
Theorem	posdif 8773	Comparison of two numbers whose difference is positive. (Contributed by NM, 17-Nov-2004.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
Theorem	lesub1 8774	Subtraction from both sides of 'less than or equal to'. (Contributed by NM, 13-May-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( A - C ) <_ ( B - C ) ) )
Theorem	lesub2 8775	Subtraction of both sides of 'less than or equal to'. (Contributed by NM, 29-Sep-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( C - B ) <_ ( C - A ) ) )
Theorem	ltsub1 8776	Subtraction from both sides of 'less than'. (Contributed by FL, 3-Jan-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( A - C ) < ( B - C ) ) )
Theorem	ltsub2 8777	Subtraction of both sides of 'less than'. (Contributed by NM, 29-Sep-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B <-> ( C - B ) < ( C - A ) ) )
Theorem	lt2sub 8778	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ D < B ) -> ( A - B ) < ( C - D ) ) )
Theorem	le2sub 8779	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A <_ C /\ D <_ B ) -> ( A - B ) <_ ( C - D ) ) )
Theorem	ltneg 8780	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.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> -u B < -u A ) )
Theorem	ltnegcon1 8781	Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004.)
|- ( ( A e. RR /\ B e. RR ) -> ( -u A < B <-> -u B < A ) )
Theorem	ltnegcon2 8782	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < -u B <-> B < -u A ) )
Theorem	leneg 8783	Negative of both sides of 'less than or equal to'. (Contributed by NM, 12-Sep-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -u B <_ -u A ) )
Theorem	lenegcon1 8784	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004.)
|- ( ( A e. RR /\ B e. RR ) -> ( -u A <_ B <-> -u B <_ A ) )
Theorem	lenegcon2 8785	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ -u B <-> B <_ -u A ) )
Theorem	lt0neg1 8786	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- ( A e. RR -> ( A < 0 <-> 0 < -u A ) )
Theorem	lt0neg2 8787	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
|- ( A e. RR -> ( 0 < A <-> -u A < 0 ) )
Theorem	le0neg1 8788	Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004.)
|- ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) )
Theorem	le0neg2 8789	Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999.)
|- ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) )
Theorem	addge01 8790	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 21-Feb-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> A <_ ( A + B ) ) )
Theorem	addge02 8791	A number is less than or equal to itself plus a nonnegative number. (Contributed by NM, 27-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> A <_ ( B + A ) ) )
Theorem	add20 8792	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.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
Theorem	subge0 8793	Nonnegative subtraction. (Contributed by NM, 14-Mar-2005.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )
Theorem	suble0 8794	Nonpositive subtraction. (Contributed by NM, 20-Mar-2008.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A - B ) <_ 0 <-> A <_ B ) )
Theorem	leaddle0 8795	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.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) <_ A <-> B <_ 0 ) )
Theorem	subge02 8796	Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( A - B ) <_ A ) )
Theorem	lesub0 8797	Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 ) )
Theorem	mullt0 8798	The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009.)
|- ( ( ( A e. RR /\ A < 0 ) /\ ( B e. RR /\ B < 0 ) ) -> 0 < ( A x. B ) )
Theorem	0le1 8799	0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- 0 <_ 1
Theorem	ltordlem 8800*	Lemma for eqord1 8801. (Contributed by Mario Carneiro, 14-Jun-2014.)
|- ( x = y -> A = B )   &    |- ( x = C -> A = M )   &    |- ( x = D -> A = N )   &    |- S C_ RR   &    |- ( ( ph /\ x e. S ) -> A e. RR )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> A < B ) )   =>    |- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D -> M < N ) )