Theorem max1 11958

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

Assertion

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

Proof of Theorem max1

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1992  ifcif 4063   class class class wbr 4618  ℝcr 9880  ℝ^*cxr 10018   ≤ cle 10020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-pre-lttri 9955  ax-pre-lttrn 9956

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025

This theorem is referenced by:  z2ge  11971  ssfzunsnext  12325  uzsup  12599  expmulnbnd  12933  discr1  12937  rexuzre  14021  rexico  14022  caubnd  14027  limsupgre  14141  limsupbnd2  14143  rlim3  14158  lo1bdd2  14184  o1lo1  14197  rlimclim1  14205  lo1mul  14287  rlimno1  14313  cvgrat  14535  ruclem10  14888  bitsfzo  15076  1arith  15550  setsstruct2  15812  evth  22661  ioombl1lem1  23228  mbfi1flimlem  23390  itg2monolem3  23420  iblre  23461  itgreval  23464  iblss  23472  i1fibl  23475  itgitg1  23476  itgle  23477  itgeqa  23481  iblconst  23485  itgconst  23486  ibladdlem  23487  itgaddlem2  23491  iblabslem  23495  iblabsr  23497  iblmulc2  23498  itgmulc2lem2  23500  itgsplit  23503  plyaddlem1  23868  coeaddlem  23904  o1cxp  24596  cxp2lim  24598  cxploglim2  24600  ftalem1  24694  ftalem2  24695  chtppilim  25059  dchrisumlem3  25075  ostth2lem2  25218  ostth3  25222  knoppndvlem18  32154  ibladdnclem  33084  itgaddnclem2  33087  iblabsnclem  33091  iblmulc2nc  33093  itgmulc2nclem2  33095  ftc1anclem5  33107  irrapxlem4  36855  irrapxlem5  36856  rexabslelem  39096  uzublem  39108  climsuse  39231  limsupubuzlem  39335  limsupmnfuzlem  39349  limsupequzmptlem  39351  limsupre3uzlem  39358  ioodvbdlimc1lem2  39440  ioodvbdlimc2lem  39442