Theorem max1 13229

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

Assertion

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

Proof of Theorem max1

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ifcif 4492   class class class wbr 5114  ℝcr 11117  ℝ^*cxr 11260   ≤ cle 11262

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-pre-lttri 11192  ax-pre-lttrn 11193

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267

This theorem is used by:  z2ge  13242  ssfzunsnext  13616  uzsup  13916  expmulnbnd  14291  discr1  14295  rexuzre  15430  rexico  15431  caubnd  15436  limsupgre  15558  limsupbnd2  15560  rlim3  15575  lo1bdd2  15601  o1lo1  15614  rlimclim1  15622  lo1mul  15705  rlimno1  15731  cvgrat  15963  ruclem10  16320  bitsfzo  16518  1arith  17012  setsstruct2  17259  evth  25155  ioombl1lem1  25754  mbfi1flimlem  25918  itg2monolem3  25948  iblre  25990  itgreval  25993  iblss  26001  i1fibl  26004  itgitg1  26005  itgle  26006  itgeqa  26010  iblconst  26014  itgconst  26015  ibladdlem  26016  itgaddlem2  26020  iblabslem  26024  iblabsr  26026  iblmulc2  26027  itgmulc2lem2  26029  itgsplit  26032  plyaddlem1  26407  coeaddlem  26443  o1cxp  27176  cxp2lim  27178  cxploglim2  27180  ftalem1  27274  ftalem2  27275  chtppilim  27676  dchrisumlem3  27692  ostth2lem2  27835  ostth3  27839  knoppndvlem18  37159  ibladdnclem  38368  itgaddnclem2  38371  iblabsnclem  38375  iblmulc2nc  38377  itgmulc2nclem2  38379  ftc1anclem5  38389  irrapxlem4  43593  irrapxlem5  43594  rexabslelem  46173  uzublem  46185  max1d  46205  uzubioo  46322  climsuse  46365  limsupubuzlem  46467  limsupmnfuzlem  46481  limsupequzmptlem  46483  limsupre3uzlem  46490  liminflelimsuplem  46530  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689