P. 89 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eqord1 8801*	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 8802*	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 8803	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- A <_ A
Theorem	gt0ne0i 8804	Positive means nonzero (useful for ordering theorems involving division). (Contributed by NM, 16-Sep-1999.)
|- A e. RR   =>    |- ( 0 < A -> A =/= 0 )
Theorem	gt0ne0ii 8805	Positive implies nonzero. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- 0 < A   =>    |- A =/= 0
Theorem	addgt0i 8806	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 8807	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 8808	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 8809	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 8810	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 8811	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 8812	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 8813	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 8814	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 8815	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 8816	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 8817	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 8818	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 8819	Nonnegative subtraction. (Contributed by NM, 13-Aug-2000.)
|- A e. RR   &    |- B e. RR   =>    |- ( 0 <_ ( A - B ) <-> B <_ A )
Theorem	ltadd1i 8820	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 8821	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 8822	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 8823	'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 8824	'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 8825	'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 8826	'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 8827	'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 8828	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 8829	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 8830	Positive implies nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> 0 < A )   =>    |- ( ph -> A =/= 0 )
Theorem	lt0ne0d 8831	Something less than zero is not zero. Deduction form. See also lt0ap0d 8967 which is similar but for apartness. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A < 0 )   =>    |- ( ph -> A =/= 0 )
Theorem	leidd 8832	'Less than or equal to' is reflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ A )
Theorem	lt0neg1d 8833	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 8834	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 8835	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 8836	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 8837	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 8838	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 8839	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 8840	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 8841	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 8842	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 8843	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 8844	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 8845	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 8846	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 8847	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 8848	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 8849	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 8850	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 8851	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 8852	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 8853	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 8854	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 8855	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 8856	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 8857	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 8858	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 8859	'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 8860	'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 8861	'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 8862	'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 8863	'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 8864	'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 8865	'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 8866	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 8867	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 8868	'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 8869	'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 8870	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 8871	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 8872	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 8873	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 8874	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 8875	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 ) )
Theorem	ltsub2dd 8876	Subtraction of 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 - B ) < ( C - A ) )
Theorem	leadd1dd 8877	Addition to both sides of 'less than or equal to'. (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	leadd2dd 8878	Addition to both sides of 'less than or equal to'. (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	lesub1dd 8879	Subtraction from both sides of 'less than or equal to'. (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	lesub2dd 8880	Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C - B ) <_ ( C - A ) )
Theorem	le2addd 8881	Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A + B ) <_ ( C + D ) )
Theorem	le2subd 8882	Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A - D ) <_ ( C - B ) )
Theorem	ltleaddd 8883	Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	leltaddd 8884	Adding both sides of two orderings. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	lt2addd 8885	Adding both side of two inequalities. Theorem I.25 of [Apostol] p. 20. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	lt2subd 8886	Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A - D ) < ( C - B ) )
Theorem	possumd 8887	Condition for a positive sum. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( 0 < ( A + B ) <-> -u B < A ) )
Theorem	sublt0d 8888	When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( A - B ) < 0 <-> A < B ) )
Theorem	ltaddsublt 8889	Addition and subtraction on one side of 'less than'. (Contributed by AV, 24-Nov-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C <-> ( ( A + B ) - C ) < A ) )
Theorem	1le1 8890	1 <_ 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
|- 1 <_ 1
Theorem	gt0add 8891	A positive sum must have a positive addend. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ 0 < ( A + B ) ) -> ( 0 < A \/ 0 < B ) )
4.3.5  Real Apartness
Syntax	creap 8892	Class of real apartness relation.
class #ℝ
Definition	df-reap 8893*	Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #ℝ is an apartness relation on the reals (see df-ap 8900 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, #ℝ and # agree (apreap 8905). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- #ℝ = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( x < y \/ y < x ) ) }
Theorem	reapval 8894	Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 8906 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( A #ℝ B <-> ( A < B \/ B < A ) ) )
Theorem	reapirr 8895	Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 8923 instead. (Contributed by Jim Kingdon, 26-Jan-2020.)
|- ( A e. RR -> -. A #ℝ A )
Theorem	recexre 8896*	Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ A #ℝ 0 ) -> E. x e. RR ( A x. x ) = 1 )
Theorem	reapti 8897	Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 8940. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> -. A #ℝ B ) )
Theorem	recexgt0 8898*	Existence of reciprocal of positive real number. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ( ( A e. RR /\ 0 < A ) -> E. x e. RR ( 0 < x /\ ( A x. x ) = 1 ) )
4.3.6  Complex Apartness
Syntax	cap 8899	Class of complex apartness relation.
class #
Definition	df-ap 8900*	Define complex apartness. Definition 6.1 of [Geuvers], p. 17. Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 8999 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 8923), symmetry (apsym 8924), and cotransitivity (apcotr 8925). Apartness implies negated equality, as seen at apne 8941, and the converse would also follow if we assumed excluded middle. In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 8940). (Contributed by Jim Kingdon, 26-Jan-2020.)
|- # = { <. x , y >. | E. r e. RR E. s e. RR E. t e. RR E. u e. RR ( ( x = ( r + ( _i x. s ) ) /\ y = ( t + ( _i x. u ) ) ) /\ ( r #ℝ t \/ s #ℝ u ) ) }