P. 87 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8601-8700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltsub1 8601	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 8602	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 8603	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 8604	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 8605	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 8606	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 8607	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 8608	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 8609	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 8610	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 8611	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 8612	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 8613	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 8614	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 8615	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 8616	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 8617	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 8618	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 8619	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 8620	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 8621	Nonnegative subtraction. (Contributed by NM, 27-Jul-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( A - B ) <_ A ) )
Theorem	lesub0 8622	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 8623	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 8624	0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
|- 0 <_ 1
Theorem	ltordlem 8625*	Lemma for eqord1 8626. (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 ) )
Theorem	eqord1 8626*	A strictly increasing real function on a subset of RR is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
|- ( 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 ) )
Theorem	eqord2 8627*	A strictly decreasing real function on a subset of RR is one-to-one. (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 -> B < A ) )   =>    |- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C = D <-> M = N ) )
Theorem	leidi 8628	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- A <_ A
Theorem	gt0ne0i 8629	Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.)
|- A e. RR   =>    |- ( 0 < A -> A =/= 0 )
Theorem	gt0ne0ii 8630	Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- 0 < A   =>    |- A =/= 0
Theorem	addgt0i 8631	Addition of 2 positive numbers is positive. (Contributed by NM, 16-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A + B ) )
Theorem	addge0i 8632	Addition of 2 nonnegative numbers is nonnegative. (Contributed by NM, 28-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A + B ) )
Theorem	addgegt0i 8633	Addition of nonnegative and positive numbers is positive. (Contributed by NM, 25-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 < B ) -> 0 < ( A + B ) )
Theorem	addgt0ii 8634	Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A + B )
Theorem	add20i 8635	Two nonnegative numbers are zero iff their sum is zero. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A + B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
Theorem	ltnegi 8636	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> -u B < -u A )
Theorem	lenegi 8637	Negative of both sides of 'less than or equal to'. (Contributed by NM, 1-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> -u B <_ -u A )
Theorem	ltnegcon2i 8638	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < -u B <-> B < -u A )
Theorem	lesub0i 8639	Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 )
Theorem	ltaddposi 8640	Adding a positive number to another number increases it. (Contributed by NM, 25-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( 0 < A <-> B < ( B + A ) )
Theorem	posdifi 8641	Comparison of two numbers whose difference is positive. (Contributed by NM, 19-Aug-2001.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B <-> 0 < ( B - A ) )
Theorem	ltnegcon1i 8642	Contraposition of negative in 'less than'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( -u A < B <-> -u B < A )
Theorem	lenegcon1i 8643	Contraposition of negative in 'less than or equal to'. (Contributed by NM, 6-Apr-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( -u A <_ B <-> -u B <_ A )
Theorem	subge0i 8644	Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|- A e. RR   &    |- B e. RR   =>    |- ( 0 <_ ( A - B ) <-> B <_ A )
Theorem	ltadd1i 8645	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by NM, 21-Jan-1997.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A < B <-> ( A + C ) < ( B + C ) )
Theorem	leadd1i 8646	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A <_ B <-> ( A + C ) <_ ( B + C ) )
Theorem	leadd2i 8647	Addition to both sides of 'less than or equal to'. (Contributed by NM, 11-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( A <_ B <-> ( C + A ) <_ ( C + B ) )
Theorem	ltsubaddi 8648	'Less than' relationship between subtraction and addition. (Contributed by NM, 21-Jan-1997.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A - B ) < C <-> A < ( C + B ) )
Theorem	lesubaddi 8649	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 30-Sep-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A - B ) <_ C <-> A <_ ( C + B ) )
Theorem	ltsubadd2i 8650	'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	lesubadd2i 8651	'Less than or equal to' relationship between subtraction and addition. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A - B ) <_ C <-> A <_ ( B + C ) )
Theorem	ltaddsubi 8652	'Less than' relationship between subtraction and addition. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A + B ) < C <-> A < ( C - B ) )
Theorem	lt2addi 8653	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   =>    |- ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) )
Theorem	le2addi 8654	Adding both side of two inequalities. (Contributed by NM, 16-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   =>    |- ( ( A <_ C /\ B <_ D ) -> ( A + B ) <_ ( C + D ) )
Theorem	gt0ne0d 8655	Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> 0 < A )   =>    |- ( ph -> A =/= 0 )
Theorem	lt0ne0d 8656	Something less than zero is not zero. Deduction form. See also lt0ap0d 8792 which is similar but for apartness. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A < 0 )   =>    |- ( ph -> A =/= 0 )
Theorem	leidd 8657	'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ A )
Theorem	lt0neg1d 8658	Comparison of a number and its negative to zero. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A < 0 <-> 0 < -u A ) )
Theorem	lt0neg2d 8659	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( 0 < A <-> -u A < 0 ) )
Theorem	le0neg1d 8660	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A <_ 0 <-> 0 <_ -u A ) )
Theorem	le0neg2d 8661	Comparison of a number and its negative to zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( 0 <_ A <-> -u A <_ 0 ) )
Theorem	addgegt0d 8662	Addition of nonnegative and positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addgtge0d 8663	Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addgt0d 8664	Addition of 2 positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	addge0d 8665	Addition of 2 nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> 0 <_ ( A + B ) )
Theorem	ltnegd 8666	Negative of both sides of 'less than'. Theorem I.23 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> -u B < -u A ) )
Theorem	lenegd 8667	Negative of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B <-> -u B <_ -u A ) )
Theorem	ltnegcon1d 8668	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -u A < B )   =>    |- ( ph -> -u B < A )
Theorem	ltnegcon2d 8669	Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < -u B )   =>    |- ( ph -> B < -u A )
Theorem	lenegcon1d 8670	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -u A <_ B )   =>    |- ( ph -> -u B <_ A )
Theorem	lenegcon2d 8671	Contraposition of negative in 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ -u B )   =>    |- ( ph -> B <_ -u A )
Theorem	ltaddposd 8672	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> B < ( B + A ) ) )
Theorem	ltaddpos2d 8673	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> B < ( A + B ) ) )
Theorem	ltsubposd 8674	Subtracting a positive number from another number decreases it. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < A <-> ( B - A ) < B ) )
Theorem	posdifd 8675	Comparison of two numbers whose difference is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A < B <-> 0 < ( B - A ) ) )
Theorem	addge01d 8676	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> A <_ ( A + B ) ) )
Theorem	addge02d 8677	A number is less than or equal to itself plus a nonnegative number. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> A <_ ( B + A ) ) )
Theorem	subge0d 8678	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ ( A - B ) <-> B <_ A ) )
Theorem	suble0d 8679	Nonpositive subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( A - B ) <_ 0 <-> A <_ B ) )
Theorem	subge02d 8680	Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 <_ B <-> ( A - B ) <_ A ) )
Theorem	ltadd1d 8681	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A < B <-> ( A + C ) < ( B + C ) ) )
Theorem	leadd1d 8682	Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( A + C ) <_ ( B + C ) ) )
Theorem	leadd2d 8683	Addition to both sides of 'less than or equal to'. (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	ltsubaddd 8684	'Less than' relationship between subtraction and addition. (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	lesubaddd 8685	'Less than or equal to' relationship between subtraction and addition. (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	ltsubadd2d 8686	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) < C <-> A < ( B + C ) ) )
Theorem	lesubadd2d 8687	'Less than or equal to' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A - B ) <_ C <-> A <_ ( B + C ) ) )
Theorem	ltaddsubd 8688	'Less than' relationship between subtraction and addition. (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	ltaddsub2d 8689	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A + B ) < C <-> B < ( C - A ) ) )
Theorem	leaddsub2d 8690	'Less than or equal to' relationship between and addition and subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( A + B ) <_ C <-> B <_ ( C - A ) ) )
Theorem	subled 8691	Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( A - B ) <_ C )   =>    |- ( ph -> ( A - C ) <_ B )
Theorem	lesubd 8692	Swap subtrahends in an inequality. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ ( B - C ) )   =>    |- ( ph -> C <_ ( B - A ) )
Theorem	ltsub23d 8693	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( A - B ) < C )   =>    |- ( ph -> ( A - C ) < B )
Theorem	ltsub13d 8694	'Less than' relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < ( B - C ) )   =>    |- ( ph -> C < ( B - A ) )
Theorem	lesub1d 8695	Subtraction from both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( A - C ) <_ ( B - C ) ) )
Theorem	lesub2d 8696	Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( A <_ B <-> ( C - B ) <_ ( C - A ) ) )
Theorem	ltsub1d 8697	Subtraction from 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 <-> ( A - C ) < ( B - C ) ) )
Theorem	ltsub2d 8698	Subtraction of 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 - B ) < ( C - A ) ) )
Theorem	ltadd1dd 8699	Addition to both sides of 'less than'. Theorem I.18 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A + C ) < ( B + C ) )
Theorem	ltsub1dd 8700	Subtraction from 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 -> ( A - C ) < ( B - C ) )