Theorem max1 12581

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

Assertion

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

Proof of Theorem max1

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ifcif 4470   class class class wbr 5069  ℝcr 10539  ℝ^*cxr 10677   ≤ cle 10679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-cnex 10596  ax-resscn 10597  ax-pre-lttri 10614  ax-pre-lttrn 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-po 5477  df-so 5478  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684

This theorem is referenced by:  z2ge  12594  ssfzunsnext  12955  uzsup  13234  expmulnbnd  13599  discr1  13603  rexuzre  14715  rexico  14716  caubnd  14721  limsupgre  14841  limsupbnd2  14843  rlim3  14858  lo1bdd2  14884  o1lo1  14897  rlimclim1  14905  lo1mul  14987  rlimno1  15013  cvgrat  15242  ruclem10  15595  bitsfzo  15787  1arith  16266  setsstruct2  16524  evth  23566  ioombl1lem1  24162  mbfi1flimlem  24326  itg2monolem3  24356  iblre  24397  itgreval  24400  iblss  24408  i1fibl  24411  itgitg1  24412  itgle  24413  itgeqa  24417  iblconst  24421  itgconst  24422  ibladdlem  24423  itgaddlem2  24427  iblabslem  24431  iblabsr  24433  iblmulc2  24434  itgmulc2lem2  24436  itgsplit  24439  plyaddlem1  24806  coeaddlem  24842  o1cxp  25555  cxp2lim  25557  cxploglim2  25559  ftalem1  25653  ftalem2  25654  chtppilim  26054  dchrisumlem3  26070  ostth2lem2  26213  ostth3  26217  knoppndvlem18  33872  ibladdnclem  34952  itgaddnclem2  34955  iblabsnclem  34959  iblmulc2nc  34961  itgmulc2nclem2  34963  ftc1anclem5  34975  irrapxlem4  39428  irrapxlem5  39429  rexabslelem  41698  uzublem  41710  max1d  41731  uzubioo  41849  climsuse  41895  limsupubuzlem  41999  limsupmnfuzlem  42013  limsupequzmptlem  42015  limsupre3uzlem  42022  liminflelimsuplem  42062  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225