Theorem max1 12632

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

Assertion

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

Proof of Theorem max1

Step	Hyp	Ref	Expression
1		rexr 10738	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2		rexr 10738	. 2 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3		xrmax1 12622	. 2 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))
4	1, 2, 3	syl2an 598	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 𝐵, 𝐵, 𝐴))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ifcif 4423   class class class wbr 5036  ℝcr 10587  ℝ^*cxr 10725   ≤ cle 10727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-pre-lttri 10662  ax-pre-lttrn 10663

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732

This theorem is referenced by:  z2ge  12645  ssfzunsnext  13014  uzsup  13293  expmulnbnd  13659  discr1  13663  rexuzre  14773  rexico  14774  caubnd  14779  limsupgre  14899  limsupbnd2  14901  rlim3  14916  lo1bdd2  14942  o1lo1  14955  rlimclim1  14963  lo1mul  15045  rlimno1  15071  cvgrat  15300  ruclem10  15653  bitsfzo  15847  1arith  16331  setsstruct2  16592  evth  23673  ioombl1lem1  24271  mbfi1flimlem  24435  itg2monolem3  24465  iblre  24506  itgreval  24509  iblss  24517  i1fibl  24520  itgitg1  24521  itgle  24522  itgeqa  24526  iblconst  24530  itgconst  24531  ibladdlem  24532  itgaddlem2  24536  iblabslem  24540  iblabsr  24542  iblmulc2  24543  itgmulc2lem2  24545  itgsplit  24548  plyaddlem1  24922  coeaddlem  24958  o1cxp  25672  cxp2lim  25674  cxploglim2  25676  ftalem1  25770  ftalem2  25771  chtppilim  26171  dchrisumlem3  26187  ostth2lem2  26330  ostth3  26334  knoppndvlem18  34292  ibladdnclem  35427  itgaddnclem2  35430  iblabsnclem  35434  iblmulc2nc  35436  itgmulc2nclem2  35438  ftc1anclem5  35448  irrapxlem4  40174  irrapxlem5  40175  rexabslelem  42456  uzublem  42468  max1d  42489  uzubioo  42605  climsuse  42651  limsupubuzlem  42755  limsupmnfuzlem  42769  limsupequzmptlem  42771  limsupre3uzlem  42778  liminflelimsuplem  42818  ioodvbdlimc1lem2  42975  ioodvbdlimc2lem  42977