Theorem max2 12263

Description: A number is less than or equal to the maximum of it and another. (Contributed by NM, 3-Apr-2005.)

Assertion

Ref	Expression
max2	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))

Proof of Theorem max2

Step	Hyp	Ref	Expression
1		rexr 10372	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 10372	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrmax2 12252	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
4	1, 2, 3	syl2an 590	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))

Syntax hints:   → wi 4   ∧ wa 385   ∈ wcel 2157  ifcif 4275   class class class wbr 4841  ℝcr 10221  ℝ^*cxr 10360   ≤ cle 10362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181  ax-cnex 10278  ax-resscn 10279  ax-pre-lttri 10296  ax-pre-lttrn 10297

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-nel 3073  df-ral 3092  df-rex 3093  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-op 4373  df-uni 4627  df-br 4842  df-opab 4904  df-mpt 4921  df-id 5218  df-po 5231  df-so 5232  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-er 7980  df-en 8194  df-dom 8195  df-sdom 8196  df-pnf 10363  df-mnf 10364  df-xr 10365  df-ltxr 10366  df-le 10367

This theorem is referenced by:  lemaxle  12271  z2ge  12274  ssfzunsnext  12636  uzsup  12913  expmulnbnd  13246  discr1  13250  rexuzre  14430  caubnd  14436  limsupgre  14550  limsupbnd2  14552  rlim3  14567  lo1bdd2  14593  o1lo1  14606  rlimclim1  14614  lo1mul  14696  rlimno1  14722  cvgrat  14949  ruclem10  15301  bitsfzo  15489  1arith  15961  evth  23083  ioombl1lem4  23666  itg2monolem3  23857  itgle  23914  ibladdlem  23924  plyaddlem1  24307  coeaddlem  24343  o1cxp  25050  cxp2lim  25052  cxploglim2  25054  ftalem1  25148  ftalem2  25149  chtppilim  25513  dchrisumlem3  25529  ostth2lem2  25672  ostth2lem3  25673  ostth2lem4  25674  ostth3  25676  knoppndvlem18  33020  ibladdnclem  33946  ftc1anclem5  33969  irrapxlem4  38163  irrapxlem5  38164  rexabslelem  40376  uzublem  40388  max2d  40419  climsuse  40572  limsupubuzlem  40676  limsupmnfuzlem  40690  limsupequzmptlem  40692  limsupre3uzlem  40699  liminflelimsuplem  40739  ioodvbdlimc1lem2  40879  ioodvbdlimc2lem  40881  hoidifhspdmvle  41568