Theorem max1 13100

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

Assertion

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

Proof of Theorem max1

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ifcif 4479   class class class wbr 5098  ℝcr 11025  ℝ^*cxr 11165   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-pre-lttri 11100  ax-pre-lttrn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  z2ge  13113  ssfzunsnext  13485  uzsup  13783  expmulnbnd  14158  discr1  14162  rexuzre  15276  rexico  15277  caubnd  15282  limsupgre  15404  limsupbnd2  15406  rlim3  15421  lo1bdd2  15447  o1lo1  15460  rlimclim1  15468  lo1mul  15551  rlimno1  15577  cvgrat  15806  ruclem10  16164  bitsfzo  16362  1arith  16855  setsstruct2  17101  evth  24914  ioombl1lem1  25515  mbfi1flimlem  25679  itg2monolem3  25709  iblre  25751  itgreval  25754  iblss  25762  i1fibl  25765  itgitg1  25766  itgle  25767  itgeqa  25771  iblconst  25775  itgconst  25776  ibladdlem  25777  itgaddlem2  25781  iblabslem  25785  iblabsr  25787  iblmulc2  25788  itgmulc2lem2  25790  itgsplit  25793  plyaddlem1  26174  coeaddlem  26210  o1cxp  26941  cxp2lim  26943  cxploglim2  26945  ftalem1  27039  ftalem2  27040  chtppilim  27442  dchrisumlem3  27458  ostth2lem2  27601  ostth3  27605  knoppndvlem18  36729  ibladdnclem  37873  itgaddnclem2  37876  iblabsnclem  37880  iblmulc2nc  37882  itgmulc2nclem2  37884  ftc1anclem5  37894  irrapxlem4  43063  irrapxlem5  43064  rexabslelem  45658  uzublem  45670  max1d  45690  uzubioo  45807  climsuse  45850  limsupubuzlem  45952  limsupmnfuzlem  45966  limsupequzmptlem  45968  limsupre3uzlem  45975  liminflelimsuplem  46015  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174