![]() |
Metamath
Proof Explorer Theorem List (p. 132 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mul2lt0rgt0 13101 | If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (๐ด ยท ๐ต) < 0) โ โข ((๐ โง 0 < ๐ต) โ ๐ด < 0) | ||
Theorem | mul2lt0llt0 13102 | If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (๐ด ยท ๐ต) < 0) โ โข ((๐ โง ๐ด < 0) โ 0 < ๐ต) | ||
Theorem | mul2lt0lgt0 13103 | If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 2-Oct-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ (๐ด ยท ๐ต) < 0) โ โข ((๐ โง 0 < ๐ด) โ ๐ต < 0) | ||
Theorem | mul2lt0bi 13104 | If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) โ โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0)))) | ||
Theorem | prodge0rd 13105 | Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.) (Revised by AV, 9-Jul-2022.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค (๐ด ยท ๐ต)) โ โข (๐ โ 0 โค ๐ต) | ||
Theorem | prodge0ld 13106 | Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by AV, 9-Jul-2022.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ 0 โค (๐ด ยท ๐ต)) โ โข (๐ โ 0 โค ๐ด) | ||
Theorem | ltdiv23d 13107 | Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) < ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) < ๐ต) | ||
Theorem | lediv23d 13108 | Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ+) & โข (๐ โ (๐ด / ๐ต) โค ๐ถ) โ โข (๐ โ (๐ด / ๐ถ) โค ๐ต) | ||
Theorem | lt2mul2divd 13109 | The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ+) & โข (๐ โ ๐ถ โ โ) & โข (๐ โ ๐ท โ โ+) โ โข (๐ โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ (๐ด / ๐ท) < (๐ถ / ๐ต))) | ||
Theorem | nnledivrp 13110 | Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ+) โ (1 โค ๐ต โ (๐ด / ๐ต) โค ๐ด)) | ||
Theorem | nn0ledivnn 13111 | Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.) |
โข ((๐ด โ โ0 โง ๐ต โ โ) โ (๐ด / ๐ต) โค ๐ด) | ||
Theorem | addlelt 13112 | If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021.) |
โข ((๐ โ โ โง ๐ โ โ โง ๐ด โ โ+) โ ((๐ + ๐ด) โค ๐ โ ๐ < ๐)) | ||
Syntax | cxne 13113 | Extend class notation to include the negative of an extended real. |
class -๐๐ด | ||
Syntax | cxad 13114 | Extend class notation to include addition of extended reals. |
class +๐ | ||
Syntax | cxmu 13115 | Extend class notation to include multiplication of extended reals. |
class ยทe | ||
Definition | df-xneg 13116 | Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.) |
โข -๐๐ด = if(๐ด = +โ, -โ, if(๐ด = -โ, +โ, -๐ด)) | ||
Definition | df-xadd 13117* | Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข +๐ = (๐ฅ โ โ*, ๐ฆ โ โ* โฆ if(๐ฅ = +โ, if(๐ฆ = -โ, 0, +โ), if(๐ฅ = -โ, if(๐ฆ = +โ, 0, -โ), if(๐ฆ = +โ, +โ, if(๐ฆ = -โ, -โ, (๐ฅ + ๐ฆ)))))) | ||
Definition | df-xmul 13118* | Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ยทe = (๐ฅ โ โ*, ๐ฆ โ โ* โฆ if((๐ฅ = 0 โจ ๐ฆ = 0), 0, if((((0 < ๐ฆ โง ๐ฅ = +โ) โจ (๐ฆ < 0 โง ๐ฅ = -โ)) โจ ((0 < ๐ฅ โง ๐ฆ = +โ) โจ (๐ฅ < 0 โง ๐ฆ = -โ))), +โ, if((((0 < ๐ฆ โง ๐ฅ = -โ) โจ (๐ฆ < 0 โง ๐ฅ = +โ)) โจ ((0 < ๐ฅ โง ๐ฆ = -โ) โจ (๐ฅ < 0 โง ๐ฆ = +โ))), -โ, (๐ฅ ยท ๐ฆ))))) | ||
Theorem | ltxr 13119 | The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ((((๐ด โ โ โง ๐ต โ โ) โง ๐ด <โ ๐ต) โจ (๐ด = -โ โง ๐ต = +โ)) โจ ((๐ด โ โ โง ๐ต = +โ) โจ (๐ด = -โ โง ๐ต โ โ))))) | ||
Theorem | elxr 13120 | Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) | ||
Theorem | xrnemnf 13121 | An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ -โ) โ (๐ด โ โ โจ ๐ด = +โ)) | ||
Theorem | xrnepnf 13122 | An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง ๐ด โ +โ) โ (๐ด โ โ โจ ๐ด = -โ)) | ||
Theorem | xrltnr 13123 | The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ ๐ด < ๐ด) | ||
Theorem | ltpnf 13124 | Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ ๐ด < +โ) | ||
Theorem | ltpnfd 13125 | Any (finite) real is less than plus infinity. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด < +โ) | ||
Theorem | 0ltpnf 13126 | Zero is less than plus infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 0 < +โ | ||
Theorem | mnflt 13127 | Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.) |
โข (๐ด โ โ โ -โ < ๐ด) | ||
Theorem | mnfltd 13128 | Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ -โ < ๐ด) | ||
Theorem | mnflt0 13129 | Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข -โ < 0 | ||
Theorem | mnfltpnf 13130 | Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
โข -โ < +โ | ||
Theorem | mnfltxr 13131 | Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.) |
โข ((๐ด โ โ โจ ๐ด = +โ) โ -โ < ๐ด) | ||
Theorem | pnfnlt 13132 | No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ +โ < ๐ด) | ||
Theorem | nltmnf 13133 | No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.) |
โข (๐ด โ โ* โ ยฌ ๐ด < -โ) | ||
Theorem | pnfge 13134 | Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.) |
โข (๐ด โ โ* โ ๐ด โค +โ) | ||
Theorem | xnn0n0n1ge2b 13135 | An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by AV, 5-Apr-2021.) |
โข (๐ โ โ0* โ ((๐ โ 0 โง ๐ โ 1) โ 2 โค ๐)) | ||
Theorem | 0lepnf 13136 | 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.) |
โข 0 โค +โ | ||
Theorem | xnn0ge0 13137 | An extended nonnegative integer is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 10-Dec-2020.) |
โข (๐ โ โ0* โ 0 โค ๐) | ||
Theorem | mnfle 13138 | Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.) |
โข (๐ด โ โ* โ -โ โค ๐ด) | ||
Theorem | mnfled 13139 | Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ -โ โค ๐ด) | ||
Theorem | xrltnsym 13140 | Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ ๐ต < ๐ด)) | ||
Theorem | xrltnsym2 13141 | 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ ยฌ (๐ด < ๐ต โง ๐ต < ๐ด)) | ||
Theorem | xrlttri 13142 | Ordering on the extended reals satisfies strict trichotomy. New proofs should generally use this instead of ax-pre-lttri 11204 or axlttri 11307. (Contributed by NM, 14-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | xrlttr 13143 | Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ((๐ด < ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | xrltso 13144 | 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.) |
โข < Or โ* | ||
Theorem | xrlttri2 13145 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 10-Dec-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โ ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) | ||
Theorem | xrlttri3 13146 | Trichotomy law for 'less than' for extended reals. (Contributed by NM, 9-Feb-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด = ๐ต โ (ยฌ ๐ด < ๐ต โง ยฌ ๐ต < ๐ด))) | ||
Theorem | xrleloe 13147 | 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค ๐ต โ (๐ด < ๐ต โจ ๐ด = ๐ต))) | ||
Theorem | xrleltne 13148 | 'Less than or equal to' implies 'less than' is not 'equals', for extended reals. (Contributed by NM, 9-Feb-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ด โค ๐ต) โ (๐ด < ๐ต โ ๐ต โ ๐ด)) | ||
Theorem | xrltlen 13149 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ต โ ๐ด))) | ||
Theorem | dfle2 13150 | Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข โค = ( < โช ( I โพ โ*)) | ||
Theorem | dflt2 13151 | Alternative definition of 'less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015.) |
โข < = ( โค โ I ) | ||
Theorem | xrltle 13152 | 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด < ๐ต โ ๐ด โค ๐ต)) | ||
Theorem | xrltled 13153 | 'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 13152. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ด < ๐ต) โ โข (๐ โ ๐ด โค ๐ต) | ||
Theorem | xrleid 13154 | 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.) |
โข (๐ด โ โ* โ ๐ด โค ๐ด) | ||
Theorem | xrleidd 13155 | 'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 13154. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ*) โ โข (๐ โ ๐ด โค ๐ด) | ||
Theorem | xrletri 13156 | Trichotomy law for extended reals. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด โค ๐ต โจ ๐ต โค ๐ด)) | ||
Theorem | xrletri3 13157 | Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) | ||
Theorem | xrletrid 13158 | Trichotomy law for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต โค ๐ด) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | xrlelttr 13159 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ((๐ด โค ๐ต โง ๐ต < ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | xrltletr 13160 | Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ((๐ด < ๐ต โง ๐ต โค ๐ถ) โ ๐ด < ๐ถ)) | ||
Theorem | xrletr 13161 | Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โ ๐ด โค ๐ถ)) | ||
Theorem | xrlttrd 13162 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ*) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ ๐ต < ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | xrlelttrd 13163 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ*) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต < ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | xrltletrd 13164 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ*) & โข (๐ โ ๐ด < ๐ต) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ ๐ด < ๐ถ) | ||
Theorem | xrletrd 13165 | Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.) |
โข (๐ โ ๐ด โ โ*) & โข (๐ โ ๐ต โ โ*) & โข (๐ โ ๐ถ โ โ*) & โข (๐ โ ๐ด โค ๐ต) & โข (๐ โ ๐ต โค ๐ถ) โ โข (๐ โ ๐ด โค ๐ถ) | ||
Theorem | xrltne 13166 | 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ด < ๐ต) โ ๐ต โ ๐ด) | ||
Theorem | nltpnft 13167 | An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.) |
โข (๐ด โ โ* โ (๐ด = +โ โ ยฌ ๐ด < +โ)) | ||
Theorem | xgepnf 13168 | An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.) |
โข (๐ด โ โ* โ (+โ โค ๐ด โ ๐ด = +โ)) | ||
Theorem | ngtmnft 13169 | An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.) |
โข (๐ด โ โ* โ (๐ด = -โ โ ยฌ -โ < ๐ด)) | ||
Theorem | xlemnf 13170 | An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
โข (๐ด โ โ* โ (๐ด โค -โ โ ๐ด = -โ)) | ||
Theorem | xrrebnd 13171 | An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.) |
โข (๐ด โ โ* โ (๐ด โ โ โ (-โ < ๐ด โง ๐ด < +โ))) | ||
Theorem | xrre 13172 | A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.) |
โข (((๐ด โ โ* โง ๐ต โ โ) โง (-โ < ๐ด โง ๐ด โค ๐ต)) โ ๐ด โ โ) | ||
Theorem | xrre2 13173 | An extended real between two others is real. (Contributed by NM, 6-Feb-2007.) |
โข (((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โง (๐ด < ๐ต โง ๐ต < ๐ถ)) โ ๐ต โ โ) | ||
Theorem | xrre3 13174 | A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.) |
โข (((๐ด โ โ* โง ๐ต โ โ) โง (๐ต โค ๐ด โง ๐ด < +โ)) โ ๐ด โ โ) | ||
Theorem | ge0gtmnf 13175 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง 0 โค ๐ด) โ -โ < ๐ด) | ||
Theorem | ge0nemnf 13176 | A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข ((๐ด โ โ* โง 0 โค ๐ด) โ ๐ด โ -โ) | ||
Theorem | xrrege0 13177 | A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.) |
โข (((๐ด โ โ* โง ๐ต โ โ) โง (0 โค ๐ด โง ๐ด โค ๐ต)) โ ๐ด โ โ) | ||
Theorem | xrmax1 13178 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ ๐ด โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | xrmax2 13179 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ ๐ต โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | xrmin1 13180 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ด) | ||
Theorem | xrmin2 13181 | The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ*) โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ต) | ||
Theorem | xrmaxeq 13182 | The maximum of two extended reals is equal to the first if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ต โค ๐ด) โ if(๐ด โค ๐ต, ๐ต, ๐ด) = ๐ด) | ||
Theorem | xrmineq 13183 | The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ต โค ๐ด) โ if(๐ด โค ๐ต, ๐ด, ๐ต) = ๐ต) | ||
Theorem | xrmaxlt 13184 | Two ways of saying the maximum of two extended reals is less than a third. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ (if(๐ด โค ๐ต, ๐ต, ๐ด) < ๐ถ โ (๐ด < ๐ถ โง ๐ต < ๐ถ))) | ||
Theorem | xrltmin 13185 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ (๐ด < if(๐ต โค ๐ถ, ๐ต, ๐ถ) โ (๐ด < ๐ต โง ๐ด < ๐ถ))) | ||
Theorem | xrmaxle 13186 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ (if(๐ด โค ๐ต, ๐ต, ๐ด) โค ๐ถ โ (๐ด โค ๐ถ โง ๐ต โค ๐ถ))) | ||
Theorem | xrlemin 13187 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ (๐ด โค if(๐ต โค ๐ถ, ๐ต, ๐ถ) โ (๐ด โค ๐ต โง ๐ด โค ๐ถ))) | ||
Theorem | max1 13188 | A number is less than or equal to the maximum of it and another. See also max1ALT 13189. (Contributed by NM, 3-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | max1ALT 13189 | A number is less than or equal to the maximum of it and another. This version of max1 13188 omits the ๐ต โ โ antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 13188 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005.) |
โข (๐ด โ โ โ ๐ด โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | max2 13190 | A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โค if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | 2resupmax 13191 | The supremum of two real numbers is the maximum of these two numbers. (Contributed by AV, 8-Jun-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ sup({๐ด, ๐ต}, โ, < ) = if(๐ด โค ๐ต, ๐ต, ๐ด)) | ||
Theorem | min1 13192 | The minimum of two numbers is less than or equal to the first. (Contributed by NM, 3-Aug-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ด) | ||
Theorem | min2 13193 | The minimum of two numbers is less than or equal to the second. (Contributed by NM, 3-Aug-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ if(๐ด โค ๐ต, ๐ด, ๐ต) โค ๐ต) | ||
Theorem | maxle 13194 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by NM, 29-Sep-2005.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (if(๐ด โค ๐ต, ๐ต, ๐ด) โค ๐ถ โ (๐ด โค ๐ถ โง ๐ต โค ๐ถ))) | ||
Theorem | lemin 13195 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โค if(๐ต โค ๐ถ, ๐ต, ๐ถ) โ (๐ด โค ๐ต โง ๐ด โค ๐ถ))) | ||
Theorem | maxlt 13196 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by NM, 3-Aug-2007.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (if(๐ด โค ๐ต, ๐ต, ๐ด) < ๐ถ โ (๐ด < ๐ถ โง ๐ต < ๐ถ))) | ||
Theorem | ltmin 13197 | Two ways of saying a number is less than the minimum of two others. (Contributed by NM, 1-Sep-2006.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < if(๐ต โค ๐ถ, ๐ต, ๐ถ) โ (๐ด < ๐ต โง ๐ด < ๐ถ))) | ||
Theorem | lemaxle 13198 | A real number which is less than or equal to a second real number is less than or equal to the maximum/supremum of the second real number and a third real number. (Contributed by AV, 8-Jun-2021.) |
โข (((๐ต โ โ โง ๐ถ โ โ) โง ๐ด โ โ โง ๐ด โค ๐ต) โ ๐ด โค if(๐ถ โค ๐ต, ๐ต, ๐ถ)) | ||
Theorem | max0sub 13199 | Decompose a real number into positive and negative parts. (Contributed by Mario Carneiro, 6-Aug-2014.) |
โข (๐ด โ โ โ (if(0 โค ๐ด, ๐ด, 0) โ if(0 โค -๐ด, -๐ด, 0)) = ๐ด) | ||
Theorem | ifle 13200 | An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014.) |
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ต โค ๐ด) โง (๐ โ ๐)) โ if(๐, ๐ด, ๐ต) โค if(๐, ๐ด, ๐ต)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |