Theorem max1 13194

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

Assertion

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

Proof of Theorem max1

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ifcif 4498   class class class wbr 5117  ℝcr 11121  ℝ^*cxr 11261   ≤ cle 11263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-pre-lttri 11196  ax-pre-lttrn 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-po 5559  df-so 5560  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268

This theorem is referenced by:  z2ge  13207  ssfzunsnext  13576  uzsup  13870  expmulnbnd  14243  discr1  14247  rexuzre  15360  rexico  15361  caubnd  15366  limsupgre  15486  limsupbnd2  15488  rlim3  15503  lo1bdd2  15529  o1lo1  15542  rlimclim1  15550  lo1mul  15633  rlimno1  15659  cvgrat  15888  ruclem10  16244  bitsfzo  16441  1arith  16934  setsstruct2  17180  evth  24896  ioombl1lem1  25498  mbfi1flimlem  25662  itg2monolem3  25692  iblre  25734  itgreval  25737  iblss  25745  i1fibl  25748  itgitg1  25749  itgle  25750  itgeqa  25754  iblconst  25758  itgconst  25759  ibladdlem  25760  itgaddlem2  25764  iblabslem  25768  iblabsr  25770  iblmulc2  25771  itgmulc2lem2  25773  itgsplit  25776  plyaddlem1  26157  coeaddlem  26193  o1cxp  26923  cxp2lim  26925  cxploglim2  26927  ftalem1  27021  ftalem2  27022  chtppilim  27424  dchrisumlem3  27440  ostth2lem2  27583  ostth3  27587  knoppndvlem18  36476  ibladdnclem  37629  itgaddnclem2  37632  iblabsnclem  37636  iblmulc2nc  37638  itgmulc2nclem2  37640  ftc1anclem5  37650  irrapxlem4  42780  irrapxlem5  42781  rexabslelem  45379  uzublem  45391  max1d  45411  uzubioo  45530  climsuse  45573  limsupubuzlem  45677  limsupmnfuzlem  45691  limsupequzmptlem  45693  limsupre3uzlem  45700  liminflelimsuplem  45740  ioodvbdlimc1lem2  45897  ioodvbdlimc2lem  45899