MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  max1 Structured version   Visualization version   GIF version

Theorem max1 12570
Description: A number is less than or equal to the maximum of it and another. See also max1ALT 12571. (Contributed by NM, 3-Apr-2005.)
Assertion
Ref Expression
max1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴𝐵, 𝐵, 𝐴))

Proof of Theorem max1
StepHypRef Expression
1 rexr 10679 . 2 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
2 rexr 10679 . 2 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
3 xrmax1 12560 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → 𝐴 ≤ if(𝐴𝐵, 𝐵, 𝐴))
41, 2, 3syl2an 597 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ≤ if(𝐴𝐵, 𝐵, 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2108  ifcif 4465   class class class wbr 5057  cr 10528  *cxr 10666  cle 10668
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-pre-lttri 10603  ax-pre-lttrn 10604
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673
This theorem is referenced by:  z2ge  12583  ssfzunsnext  12944  uzsup  13223  expmulnbnd  13588  discr1  13592  rexuzre  14704  rexico  14705  caubnd  14710  limsupgre  14830  limsupbnd2  14832  rlim3  14847  lo1bdd2  14873  o1lo1  14886  rlimclim1  14894  lo1mul  14976  rlimno1  15002  cvgrat  15231  ruclem10  15584  bitsfzo  15776  1arith  16255  setsstruct2  16513  evth  23555  ioombl1lem1  24151  mbfi1flimlem  24315  itg2monolem3  24345  iblre  24386  itgreval  24389  iblss  24397  i1fibl  24400  itgitg1  24401  itgle  24402  itgeqa  24406  iblconst  24410  itgconst  24411  ibladdlem  24412  itgaddlem2  24416  iblabslem  24420  iblabsr  24422  iblmulc2  24423  itgmulc2lem2  24425  itgsplit  24428  plyaddlem1  24795  coeaddlem  24831  o1cxp  25544  cxp2lim  25546  cxploglim2  25548  ftalem1  25642  ftalem2  25643  chtppilim  26043  dchrisumlem3  26059  ostth2lem2  26202  ostth3  26206  knoppndvlem18  33861  ibladdnclem  34940  itgaddnclem2  34943  iblabsnclem  34947  iblmulc2nc  34949  itgmulc2nclem2  34951  ftc1anclem5  34963  irrapxlem4  39413  irrapxlem5  39414  rexabslelem  41682  uzublem  41694  max1d  41715  uzubioo  41833  climsuse  41879  limsupubuzlem  41983  limsupmnfuzlem  41997  limsupequzmptlem  41999  limsupre3uzlem  42006  liminflelimsuplem  42046  ioodvbdlimc1lem2  42207  ioodvbdlimc2lem  42209
  Copyright terms: Public domain W3C validator