![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > max1 | Structured version Visualization version GIF version |
Description: A number is less than or equal to the maximum of it and another. See also max1ALT 12202. (Contributed by NM, 3-Apr-2005.) |
Ref | Expression |
---|---|
max1 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 10269 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 10269 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrmax1 12191 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | |
4 | 1, 2, 3 | syl2an 495 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2131 ifcif 4222 class class class wbr 4796 ℝcr 10119 ℝ*cxr 10257 ≤ cle 10259 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-cnex 10176 ax-resscn 10177 ax-pre-lttri 10194 ax-pre-lttrn 10195 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-nel 3028 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-po 5179 df-so 5180 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-er 7903 df-en 8114 df-dom 8115 df-sdom 8116 df-pnf 10260 df-mnf 10261 df-xr 10262 df-ltxr 10263 df-le 10264 |
This theorem is referenced by: z2ge 12214 ssfzunsnext 12571 uzsup 12848 expmulnbnd 13182 discr1 13186 rexuzre 14283 rexico 14284 caubnd 14289 limsupgre 14403 limsupbnd2 14405 rlim3 14420 lo1bdd2 14446 o1lo1 14459 rlimclim1 14467 lo1mul 14549 rlimno1 14575 cvgrat 14806 ruclem10 15159 bitsfzo 15351 1arith 15825 setsstruct2 16090 evth 22951 ioombl1lem1 23518 mbfi1flimlem 23680 itg2monolem3 23710 iblre 23751 itgreval 23754 iblss 23762 i1fibl 23765 itgitg1 23766 itgle 23767 itgeqa 23771 iblconst 23775 itgconst 23776 ibladdlem 23777 itgaddlem2 23781 iblabslem 23785 iblabsr 23787 iblmulc2 23788 itgmulc2lem2 23790 itgsplit 23793 plyaddlem1 24160 coeaddlem 24196 o1cxp 24892 cxp2lim 24894 cxploglim2 24896 ftalem1 24990 ftalem2 24991 chtppilim 25355 dchrisumlem3 25371 ostth2lem2 25514 ostth3 25518 knoppndvlem18 32818 ibladdnclem 33771 itgaddnclem2 33774 iblabsnclem 33778 iblmulc2nc 33780 itgmulc2nclem2 33782 ftc1anclem5 33794 irrapxlem4 37883 irrapxlem5 37884 rexabslelem 40135 uzublem 40147 max1d 40168 uzubioo 40289 climsuse 40335 limsupubuzlem 40439 limsupmnfuzlem 40453 limsupequzmptlem 40455 limsupre3uzlem 40462 liminflelimsuplem 40502 ioodvbdlimc1lem2 40642 ioodvbdlimc2lem 40644 |
Copyright terms: Public domain | W3C validator |