Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > max2 | Structured version Visualization version GIF version |
Description: A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.) |
Ref | Expression |
---|---|
max2 | ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexr 10681 | . 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*) | |
2 | rexr 10681 | . 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*) | |
3 | xrmax2 12563 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) | |
4 | 1, 2, 3 | syl2an 597 | 1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2110 ifcif 4466 class class class wbr 5058 ℝcr 10530 ℝ*cxr 10668 ≤ cle 10670 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-pre-lttri 10605 ax-pre-lttrn 10606 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-po 5468 df-so 5469 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-er 8283 df-en 8504 df-dom 8505 df-sdom 8506 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 |
This theorem is referenced by: lemaxle 12582 z2ge 12585 ssfzunsnext 12946 uzsup 13225 expmulnbnd 13590 discr1 13594 rexuzre 14706 caubnd 14712 limsupgre 14832 limsupbnd2 14834 rlim3 14849 lo1bdd2 14875 o1lo1 14888 rlimclim1 14896 lo1mul 14978 rlimno1 15004 cvgrat 15233 ruclem10 15586 bitsfzo 15778 1arith 16257 evth 23557 ioombl1lem4 24156 itg2monolem3 24347 itgle 24404 ibladdlem 24414 plyaddlem1 24797 coeaddlem 24833 o1cxp 25546 cxp2lim 25548 cxploglim2 25550 ftalem1 25644 ftalem2 25645 chtppilim 26045 dchrisumlem3 26061 ostth2lem2 26204 ostth2lem3 26205 ostth2lem4 26206 ostth3 26208 knoppndvlem18 33863 ibladdnclem 34942 ftc1anclem5 34965 irrapxlem4 39415 irrapxlem5 39416 rexabslelem 41685 uzublem 41697 max2d 41727 climsuse 41882 limsupubuzlem 41986 limsupmnfuzlem 42000 limsupequzmptlem 42002 limsupre3uzlem 42009 liminflelimsuplem 42049 ioodvbdlimc1lem2 42210 ioodvbdlimc2lem 42212 hoidifhspdmvle 42896 |
Copyright terms: Public domain | W3C validator |