P. 91 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lemul1a 9001	Multiplication of both sides of 'less than or equal to' by a nonnegative number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 21-Feb-2005.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )
Theorem	lemul2a 9002	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C x. A ) <_ ( C x. B ) )
Theorem	ltmul12a 9003	Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.)
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) )
Theorem	lemul12b 9004	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
|- ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( C e. RR /\ ( D e. RR /\ 0 <_ D ) ) ) -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
Theorem	lemul12a 9005	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
|- ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( ( C e. RR /\ 0 <_ C ) /\ D e. RR ) ) -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
Theorem	mulgt1 9006	The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < ( A x. B ) )
Theorem	ltmulgt11 9007	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
Theorem	ltmulgt12 9008	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( B x. A ) ) )
Theorem	lemulge11 9009	Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( A x. B ) )
Theorem	lemulge12 9010	Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( B x. A ) )
Theorem	ltdiv1 9011	Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
Theorem	lediv1 9012	Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A / C ) <_ ( B / C ) ) )
Theorem	gt0div 9013	Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 < A <-> 0 < ( A / B ) ) )
Theorem	ge0div 9014	Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )
Theorem	divgt0 9015	The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A / B ) )
Theorem	divge0 9016	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
Theorem	ltmuldiv 9017	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> A < ( B / C ) ) )
Theorem	ltmuldiv2 9018	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. A ) < B <-> A < ( B / C ) ) )
Theorem	ltdivmul 9019	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( C x. B ) ) )
Theorem	ledivmul 9020	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )
Theorem	ltdivmul2 9021	'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( B x. C ) ) )
Theorem	lt2mul2div 9022	'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.)
|- ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A x. B ) < ( C x. D ) <-> ( A / D ) < ( C / B ) ) )
Theorem	ledivmul2 9023	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( B x. C ) ) )
Theorem	lemuldiv 9024	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ B <-> A <_ ( B / C ) ) )
Theorem	lemuldiv2 9025	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. A ) <_ B <-> A <_ ( B / C ) ) )
Theorem	ltrec 9026	The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lerec 9027	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	lt2msq1 9028	Lemma for lt2msq 9029. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )
Theorem	lt2msq 9029	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
Theorem	ltdiv2 9030	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C / B ) < ( C / A ) ) )
Theorem	ltrec1 9031	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < A ) )
Theorem	lerec2 9032	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> B <_ ( 1 / A ) ) )
Theorem	ledivdiv 9033	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )
Theorem	lediv2 9034	Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )
Theorem	ltdiv23 9035	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	lediv23 9036	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) <_ C <-> ( A / C ) <_ B ) )
Theorem	lediv12a 9037	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )
Theorem	lediv2a 9038	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C / B ) <_ ( C / A ) )
Theorem	reclt1 9039	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( A < 1 <-> 1 < ( 1 / A ) ) )
Theorem	recgt1 9040	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( 1 < A <-> ( 1 / A ) < 1 ) )
Theorem	recgt1i 9041	The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 1 < A ) -> ( 0 < ( 1 / A ) /\ ( 1 / A ) < 1 ) )
Theorem	recp1lt1 9042	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A / ( 1 + A ) ) < 1 )
Theorem	recreclt 9043	Given a positive number A, construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( ( 1 / ( 1 + ( 1 / A ) ) ) < 1 /\ ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )
Theorem	le2msq 9044	The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	msq11 9045	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
Theorem	ledivp1 9046	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ A )
Theorem	squeeze0 9047*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
|- ( ( A e. RR /\ 0 <_ A /\ A. x e. RR ( 0 < x -> A < x ) ) -> A = 0 )
Theorem	ltp1i 9048	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- A e. RR   =>    |- A < ( A + 1 )
Theorem	recgt0i 9049	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
|- A e. RR   =>    |- ( 0 < A -> 0 < ( 1 / A ) )
Theorem	recgt0ii 9050	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- 0 < A   =>    |- 0 < ( 1 / A )
Theorem	prodgt0i 9051	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 15-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 < ( A x. B ) ) -> 0 < B )
Theorem	prodge0i 9052	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 <_ ( A x. B ) ) -> 0 <_ B )
Theorem	divgt0i 9053	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A / B ) )
Theorem	divge0i 9054	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 12-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 < B ) -> 0 <_ ( A / B ) )
Theorem	ltreci 9055	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lereci 9056	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 16-Sep-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	lt2msqi 9057	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
Theorem	le2msqi 9058	The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	msq11i 9059	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
Theorem	divgt0i2i 9060	The ratio of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < B   =>    |- ( 0 < A -> 0 < ( A / B ) )
Theorem	ltrecii 9061	The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- ( A < B <-> ( 1 / B ) < ( 1 / A ) )
Theorem	divgt0ii 9062	The ratio of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A / B )
Theorem	ltmul1i 9063	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
Theorem	ltdiv1i 9064	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( A / C ) < ( B / C ) ) )
Theorem	ltmuldivi 9065	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( ( A x. C ) < B <-> A < ( B / C ) ) )
Theorem	ltmul2i 9066	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A < B <-> ( C x. A ) < ( C x. B ) ) )
Theorem	lemul1i 9067	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
Theorem	lemul2i 9068	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 1-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( 0 < C -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
Theorem	ltdiv23i 9069	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( 0 < B /\ 0 < C ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	ltdiv23ii 9070	Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < B   &    |- 0 < C   =>    |- ( ( A / B ) < C <-> ( A / C ) < B )
Theorem	ltmul1ii 9071	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 16-May-1999.) (Proof shortened by Paul Chapman, 25-Jan-2008.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < C   =>    |- ( A < B <-> ( A x. C ) < ( B x. C ) )
Theorem	ltdiv1ii 9072	Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- 0 < C   =>    |- ( A < B <-> ( A / C ) < ( B / C ) )
Theorem	ltp1d 9073	A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A < ( A + 1 ) )
Theorem	lep1d 9074	A number is less than or equal to itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ ( A + 1 ) )
Theorem	ltm1d 9075	A number minus 1 is less than itself. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A - 1 ) < A )
Theorem	lem1d 9076	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( A - 1 ) <_ A )
Theorem	recgt0d 9077	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 < A )   =>    |- ( ph -> 0 < ( 1 / A ) )
Theorem	divgt0d 9078	The ratio of two positive numbers is positive. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A / B ) )
Theorem	mulgt1d 9079	The product of two numbers greater than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 1 < A )   &    |- ( ph -> 1 < B )   =>    |- ( ph -> 1 < ( A x. B ) )
Theorem	lemulge11d 9080	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 1 <_ B )   =>    |- ( ph -> A <_ ( A x. B ) )
Theorem	lemulge12d 9081	Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 1 <_ B )   =>    |- ( ph -> A <_ ( B x. A ) )
Theorem	lemul1ad 9082	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A x. C ) <_ ( B x. C ) )
Theorem	lemul2ad 9083	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C x. A ) <_ ( C x. B ) )
Theorem	ltmul12ad 9084	Comparison of product of two positive numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A < B )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> C < D )   =>    |- ( ph -> ( A x. C ) < ( B x. D ) )
Theorem	lemul12ad 9085	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( A x. C ) <_ ( B x. D ) )
Theorem	lemul12bd 9086	Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> 0 <_ D )   &    |- ( ph -> A <_ B )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( A x. C ) <_ ( B x. D ) )
Theorem	mulle0r 9087	Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ 0 /\ 0 <_ B ) ) -> ( A x. B ) <_ 0 )
4.3.10  Suprema
Theorem	lbreu 9088*	If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )
Theorem	lbcl 9089*	If a set of reals contains a lower bound, it contains a unique lower bound that belongs to the set. (Contributed by NM, 9-Oct-2005.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. S )
Theorem	lble 9090*	If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A )
Theorem	lbinf 9091*	If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) )
Theorem	lbinfcl 9092*	If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) e. S )
Theorem	lbinfle 9093*	If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> inf ( S , RR , < ) <_ A )
Theorem	suprubex 9094*	A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. A )   =>    |- ( ph -> B <_ sup ( A , RR , < ) )
Theorem	suprlubex 9095*	The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) )
Theorem	suprnubex 9096*	An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )
Theorem	suprleubex 9097*	The supremum of a nonempty bounded set of reals is less than or equal to an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 6-Sep-2014.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( sup ( A , RR , < ) <_ B <-> A. z e. A z <_ B ) )
Theorem	negiso 9098	Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- F = ( x e. RR |-> -u x )   =>    |- ( F Isom < , `' < ( RR , RR ) /\ `' F = F )
Theorem	dfinfre 9099*	The infimum of a set of reals A. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.)
|- ( A C_ RR -> inf ( A , RR , < ) = U. { x e. RR | ( A. y e. A x <_ y /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) } )
Theorem	sup3exmid 9100*	If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)
|- ( ( u C_ RR /\ E. w w e. u /\ E. x e. RR A. y e. u y <_ x ) -> E. x e. RR ( A. y e. u -. x < y /\ A. y e. RR ( y < x -> E. z e. u y < z ) ) )   =>    |- DECID ph