mmtheorems71 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 7001-7100 - Page 71 of 175

Type	Label	Description
Statement
Theorem	ltdiv1ii 7001	Division of both sides of 'less than' by a positive number.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- 0 < C   =>   |- (A < B <-> (A / C) < (B / C))
Theorem	ltdiv1i 7002	Division of both sides of 'less than' by a positive number.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A < B <-> (A / C) < (B / C)))
Theorem	ltmuldivi 7003	'Less than' relationship between division and multiplication.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> ((A x. C) < B <-> A < (B / C)))
Theorem	prodgt0 7004	Infer that a multiplicand is positive from a nonnegative muliplier and positive product.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 0 < (A x. B))) -> 0 < B)
Theorem	prodgt02 7005	Infer that a multiplier is positive from a nonnegative muliplicand and positive product.
|- (((A e. RR /\ B e. RR) /\ (0 <_ B /\ 0 < (A x. B))) -> 0 < A)
Theorem	prodge0 7006	Infer that a multiplicand is nonnegative from a positive muliplier and nonnegative product.
|- (((A e. RR /\ B e. RR) /\ (0 < A /\ 0 <_ (A x. B))) -> 0 <_ B)
Theorem	prodge02 7007	Infer that a multiplier is nonnegative from a positive muliplicand and nonnegative product.
|- (((A e. RR /\ B e. RR) /\ (0 < B /\ 0 <_ (A x. B))) -> 0 <_ A)
Theorem	ltmul1 7008	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A < B <-> (A x. C) < (B x. C)))
Theorem	ltmul2 7009	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A < B <-> (C x. A) < (C x. B)))
Theorem	ltmul2OLD 7010	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < C) -> (A < B <-> (C x. A) < (C x. B)))
Theorem	lemul1 7011	Multiplication of both sides of 'less than or equal to' by a positive number.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A <_ B <-> (A x. C) <_ (B x. C)))
Theorem	lemul1OLD 7012	Multiplication of both sides of 'less than or equal to' by a positive number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < C) -> (A <_ B <-> (A x. C) <_ (B x. C)))
Theorem	lemul2 7013	Multiplication of both sides of 'less than or equal to' by a positive number.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A <_ B <-> (C x. A) <_ (C x. B)))
Theorem	lemul2OLD 7014	Multiplication of both sides of 'less than or equal to' by a positive number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < C) -> (A <_ B <-> (C x. A) <_ (C x. B)))
Theorem	ltmul2i 7015	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A < B <-> (C x. A) < (C x. B)))
Theorem	ltmul2iOLD 7016	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A < B <-> (C x. A) < (C x. B)))
Theorem	lemul1i 7017	Multiplication of both sides of 'less than or equal to' by a positive number.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A <_ B <-> (A x. C) <_ (B x. C)))
Theorem	lemul2i 7018	Multiplication of both sides of 'less than or equal to' by a positive number.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- (0 < C -> (A <_ B <-> (C x. A) <_ (C x. B)))
Theorem	lemul1a 7019	Multiplication of both sides of 'less than or equal to' by a nonnegative number.
|- (((A e. RR /\ B e. RR /\ (C e. RR /\ 0 <_ C)) /\ A <_ B) -> (A x. C) <_ (B x. C))
Theorem	lemul1aOLD 7020	Multiplication of both sides of 'less than or equal to' by a nonnegative number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (0 <_ C /\ A <_ B)) -> (A x. C) <_ (B x. C))
Theorem	lemul2a 7021	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	lemul2aOLD 7022	Multiplication of both sides of 'less than or equal to' by a nonnegative number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (0 <_ C /\ A <_ B)) -> (C x. A) <_ (C x. B))
Theorem	ltmul12a 7023	Comparison of product of two positive numbers.
|- ((((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 7024	Comparison of product of two nonnegative numbers.
|- ((((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	lemul12aOLD 7025	Comparison of product of two nonnegative numbers.
|- ((((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	lemul12a 7026	Comparison of product of two nonnegative numbers.
|- ((((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 7027	The product of two numbers greater than 1 is greater than 1.
|- (((A e. RR /\ B e. RR) /\ (1 < A /\ 1 < B)) -> 1 < (A x. B))
Theorem	ltmulgt11 7028	Multiplication by a number greater than 1.
|- ((A e. RR /\ B e. RR /\ 0 < A) -> (1 < B <-> A < (A x. B)))
Theorem	ltmulgt12 7029	Multiplication by a number greater than 1.
|- ((A e. RR /\ B e. RR /\ 0 < A) -> (1 < B <-> A < (B x. A)))
Theorem	lemulge11 7030	Multiplication by a number greater than or equal to 1.
|- (((A e. RR /\ B e. RR) /\ (0 <_ A /\ 1 <_ B)) -> A <_ (A x. B))
Theorem	ltdiv1 7031	Division of both sides of 'less than' by a positive number.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A < B <-> (A / C) < (B / C)))
Theorem	ltdiv1OLD 7032	Division of both sides of 'less than' by a positive number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < C) -> (A < B <-> (A / C) < (B / C)))
Theorem	lediv1 7033	Division of both sides of a less than or equal to relation by a positive number.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> (A <_ B <-> (A / C) <_ (B / C)))
Theorem	lediv1OLD 7034	Division of both sides of a less than or equal to relation by a positive number.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < C) -> (A <_ B <-> (A / C) <_ (B / C)))
Theorem	gt0div 7035	Division of a positive number by a positive number.
|- ((A e. RR /\ B e. RR /\ 0 < B) -> (0 < A <-> 0 < (A / B)))
Theorem	ge0div 7036	Division of a nonnegative number by a positive number.
|- ((A e. RR /\ B e. RR /\ 0 < B) -> (0 <_ A <-> 0 <_ (A / B)))
Theorem	divgt0 7037	The ratio of two positive numbers is positive.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> 0 < (A / B))
Theorem	divge0 7038	The ratio of nonnegative and positive numbers is nonnegative.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 < B)) -> 0 <_ (A / B))
Theorem	divgt0i 7039	The ratio of two positive numbers is positive.
|- A e. RR   &   |- B e. RR   =>   |- ((0 < A /\ 0 < B) -> 0 < (A / B))
Theorem	divge0i 7040	The ratio of nonnegative and positive numbers is nonnegative.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 < B) -> 0 <_ (A / B))
Theorem	divgt0i2i 7041	The ratio of two positive numbers is positive.
|- A e. RR   &   |- B e. RR   &   |- 0 < B   =>   |- (0 < A -> 0 < (A / B))
Theorem	divgt0ii 7042	The ratio of two positive numbers is positive.
|- A e. RR   &   |- B e. RR   &   |- 0 < A   &   |- 0 < B   =>   |- 0 < (A / B)
Theorem	recgt0 7043	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21.
|- ((A e. RR /\ 0 < A) -> 0 < (1 / A))
Theorem	recgt0i 7044	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21.
|- A e. RR   =>   |- (0 < A -> 0 < (1 / A))
Theorem	ltmuldiv 7045	'Less than' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A x. C) < B <-> A < (B / C)))
Theorem	ltmuldivOLD 7046	'Less than' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < B) -> ((A x. B) < C <-> A < (C / B)))
Theorem	ltmuldiv2 7047	'Less than' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((C x. A) < B <-> A < (B / C)))
Theorem	ltmuldiv2OLD 7048	'Less than' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < A) -> ((A x. B) < C <-> B < (C / A)))
Theorem	ltdivmul 7049	'Less than' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A / C) < B <-> A < (C x. B)))
Theorem	ltdivmulOLD 7050	'Less than' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < B) -> ((A / B) < C <-> A < (B x. C)))
Theorem	ledivmul 7051	'Less than or equal to' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A / C) <_ B <-> A <_ (C x. B)))
Theorem	ledivmulOLD 7052	'Less than or equal to' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < B) -> ((A / B) <_ C <-> A <_ (B x. C)))
Theorem	ltdivmul2 7053	'Less than' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A / C) < B <-> A < (B x. C)))
Theorem	lt2mul2div 7054	'Less than' relationship between division and multiplication.
|- (((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	lt2mul2divOLD 7055	'Less than' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR) /\ (C e. RR /\ D e. RR) /\ (0 < B /\ 0 < D)) -> ((A x. B) < (C x. D) <-> (A / D) < (C / B)))
Theorem	ledivmul2 7056	'Less than or equal to' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A / C) <_ B <-> A <_ (B x. C)))
Theorem	ledivmul2OLD 7057	'Less than or equal to' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < B) -> ((A / B) <_ C <-> A <_ (C x. B)))
Theorem	lemuldiv 7058	'Less than or equal' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((A x. C) <_ B <-> A <_ (B / C)))
Theorem	lemuldiv2 7059	'Less than or equal' relationship between division and multiplication.
|- ((A e. RR /\ B e. RR /\ (C e. RR /\ 0 < C)) -> ((C x. A) <_ B <-> A <_ (B / C)))
Theorem	lemuldiv2OLD 7060	'Less than or equal' relationship between division and multiplication.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ 0 < A) -> ((A x. B) <_ C <-> B <_ (C / A)))
Theorem	ltrecii 7061	The reciprocal of both sides of 'less than'.
|- A e. RR   &   |- B e. RR   &   |- 0 < A   &   |- 0 < B   =>   |- (A < B <-> (1 / B) < (1 / A))
Theorem	ltreci 7062	The reciprocal of both sides of 'less than'.
|- A e. RR   &   |- B e. RR   =>   |- ((0 < A /\ 0 < B) -> (A < B <-> (1 / B) < (1 / A)))
Theorem	lereci 7063	The reciprocal of both sides of 'less than or equal to'.
|- A e. RR   &   |- B e. RR   =>   |- ((0 < A /\ 0 < B) -> (A <_ B <-> (1 / B) <_ (1 / A)))
Theorem	lt2msqi 7064	The square function on nonnegative reals is strictly monotonic.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A < B <-> (A x. A) < (B x. B)))
Theorem	le2msqi 7065	The square function on nonnegative reals is monotonic.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> (A <_ B <-> (A x. A) <_ (B x. B)))
Theorem	msq11i 7066	The square of a nonnegative number is a one-to-one function.
|- A e. RR   &   |- B e. RR   =>   |- ((0 <_ A /\ 0 <_ B) -> ((A x. A) = (B x. B) <-> A = B))
Theorem	ltrec 7067	The reciprocal of both sides of 'less than'.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> (A < B <-> (1 / B) < (1 / A)))
Theorem	lerec 7068	The reciprocal of both sides of 'less than or equal to'.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> (A <_ B <-> (1 / B) <_ (1 / A)))
Theorem	lt2msq 7069	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.)
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> (A < B <-> (A x. A) < (B x. B)))
Theorem	ltdiv2 7070	Division of a positive number by both sides of 'less than'.
|- (((A e. RR /\ B e. RR /\ C e. RR) /\ (0 < A /\ 0 < B /\ 0 < C)) -> (A < B <-> (C / B) < (C / A)))
Theorem	ltrec1 7071	Reciprocal swap in a 'less than' relation.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> ((1 / A) < B <-> (1 / B) < A))
Theorem	lerec2 7072	Reciprocal swap in a 'less than or equal to' relation.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B)) -> (A <_ (1 / B) <-> B <_ (1 / A)))
Theorem	ledivdiv 7073	Invert ratios of positive numbers and swap their ordering.
|- ((((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 7074	Division of a positive number by both sides of 'less than or equal to'.
|- (((A e. RR /\ 0 < A) /\ (B e. RR /\ 0 < B) /\ (C e. RR /\ 0 < C)) -> (A <_ B <-> (C / B) <_ (C / A)))
Theorem	ltdiv23 7075	Swap denominator with other side of 'less than'.
|- ((A e. RR /\ (B e. RR /\ 0 < B) /\ (C e. RR /\ 0 < C)) -> ((A / B) < C <-> (A / C) < B))
Theorem	lediv23 7076	Swap denominator with other side of 'less than or equal to'.
|- ((A e. RR /\ (B e. RR /\ 0 < B) /\ (C e. RR /\ 0 < C)) -> ((A / B) <_ C <-> (A / C) <_ B))
Theorem	ltdiv23i 7077	Swap denominator with other side of 'less than'.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((0 < B /\ 0 < C) -> ((A / B) < C <-> (A / C) < B))
Theorem	ltdiv23ii 7078	Swap denominator with other side of 'less than'.
|- A e. RR   &   |- B e. RR   &   |- C e. RR   &   |- 0 < B   &   |- 0 < C   =>   |- ((A / B) < C <-> (A / C) < B)
Theorem	lediv12a 7079	Comparison of ratio of two nonnegative numbers.
|- ((((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 7080	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 7081	The reciprocal of a positive number less than 1 is greater than 1.
|- ((A e. RR /\ 0 < A) -> (A < 1 <-> 1 < (1 / A)))
Theorem	recgt1 7082	The reciprocal of a positive number greater than 1 is less than 1.
|- ((A e. RR /\ 0 < A) -> (1 < A <-> (1 / A) < 1))
Theorem	recgt1i 7083	The reciprocal of a number greater than 1 is positive and less than 1.
|- ((A e. RR /\ 1 < A) -> (0 < (1 / A) /\ (1 / A) < 1))
Theorem	recp1lt1 7084	Construct a number less than 1 from any nonnegative number.
|- ((A e. RR /\ 0 <_ A) -> (A / (1 + A)) < 1)
Theorem	recreclt 7085	Given a positive number A, construct a new positive number less than both A and 1.
|- ((A e. RR /\ 0 < A) -> ((1 / (1 + (1 / A))) < 1 /\ (1 / (1 + (1 / A))) < A))
Theorem	le2msq 7086	The square function on nonnegative reals is monotonic.
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> (A <_ B <-> (A x. A) <_ (B x. B)))
Theorem	halfposi 7087	A positive number is greater than its half.
|- A e. RR   =>   |- (0 < A <-> (A / (1 + 1)) < A)
Theorem	ledivp1 7088	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.)
|- (((A e. RR /\ 0 <_ A) /\ (B e. RR /\ 0 <_ B)) -> ((A / (B + 1)) x. B) <_ A)
Theorem	ledivp1i 7089	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.)
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((0 <_ A /\ 0 <_ C /\ A <_ (B / (C + 1))) -> (A x. C) <_ B)
Theorem	ltdivp1i 7090	Less-than and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.)
|- A e. RR   &   |- B e. RR   &   |- C e. RR   =>   |- ((0 <_ A /\ 0 <_ C /\ A < (B / (C + 1))) -> (A x. C) < B)
Theorem	posexi 7091	There exists a positive number less than two others.
|- A e. RR   &   |- B e. RR   &   |- 0 < A   &   |- 0 < B   =>   |- E.x e. RR (0 < x /\ (x < A /\ x < B))
Theorem	xrmax1 7092	An extended real is less than or equal to the maximum of it and another.
|- ((A e. RR* /\ B e. RR*) -> A <_ if(A <_ B, B, A))
Theorem	xrmax2 7093	An extended real is less than or equal to the maximum of it and another.
|- ((A e. RR* /\ B e. RR*) -> B <_ if(A <_ B, B, A))
Theorem	xrmin1 7094	The minimum of two extended reals is less than or equal to one of them.
|- ((A e. RR* /\ B e. RR*) -> if(A <_ B, A, B) <_ A)
Theorem	xrmin2 7095	The minimum of two extended reals is less than or equal to one of them.
|- ((A e. RR* /\ B e. RR*) -> if(A <_ B, A, B) <_ B)
Theorem	xrmaxlt 7096	Two ways of saying the maximum of two extended reals is less than a third.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (if(A <_ B, B, A) < C <-> (A < C /\ B < C)))
Theorem	xrltmin 7097	Two ways of saying an extended real is less than the minimum of two others.
|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (A < if(B <_ C, B, C) <-> (A < B /\ A < C)))
Theorem	max1 7098	A number is less than or equal to the maximum of it and another.
|- ((A e. RR /\ B e. RR) -> A <_ if(A <_ B, B, A))
Theorem	max1ALT 7099	A number is less than or equal to the maximum of it and another.
|- (A e. RR -> A <_ if(A <_ B, B, A))
Theorem	max2 7100	A number is less than or equal to the maximum of it and another.
|- ((A e. RR /\ B e. RR) -> B <_ if(A <_ B, B, A))