Theorem max1 13345

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

Assertion

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

Proof of Theorem max1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ifcif 4485   class class class wbr 5106  ℝcr 11229  ℝ^*cxr 11372   ≤ cle 11374

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-pre-lttri 11304  ax-pre-lttrn 11305

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-po 5564  df-so 5565  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379

This theorem is used by:  z2ge  13358  ssfzunsnext  13733  uzsup  14033  expmulnbnd  14409  discr1  14413  rexuzre  15552  rexico  15553  caubnd  15558  limsupgre  15680  limsupbnd2  15682  rlim3  15697  lo1bdd2  15723  o1lo1  15736  rlimclim1  15744  lo1mul  15827  rlimno1  15853  cvgrat  16084  ruclem10  16439  bitsfzo  16637  1arith  17137  setsstruct2  17384  evth  25313  ioombl1lem1  25912  mbfi1flimlem  26076  itg2monolem3  26106  iblre  26147  itgreval  26150  iblss  26158  i1fibl  26161  itgitg1  26162  itgle  26163  itgeqa  26167  iblconst  26171  itgconst  26172  ibladdlem  26173  itgaddlem2  26177  iblabslem  26181  iblabsr  26183  iblmulc2  26184  itgmulc2lem2  26186  itgsplit  26189  plyaddlem1  26565  coeaddlem  26601  o1cxp  27335  cxp2lim  27337  cxploglim2  27339  ftalem1  27433  ftalem2  27434  chtppilim  27835  dchrisumlem3  27851  ostth2lem2  27994  ostth3  27998  knoppndvlem18  37586  ibladdnclem  38799  itgaddnclem2  38802  iblabsnclem  38806  iblmulc2nc  38808  itgmulc2nclem2  38810  ftc1anclem5  38820  irrapxlem4  44036  irrapxlem5  44037  rexabslelem  46643  uzublem  46655  max1d  46675  uzubioo  46792  climsuse  46835  limsupubuzlem  46937  limsupmnfuzlem  46951  limsupequzmptlem  46953  limsupre3uzlem  46960  liminflelimsuplem  47000  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159