Theorem ltleii 11333

Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)

Hypotheses

Ref	Expression
lt.1	⊢ 𝐴 ∈ ℝ
lt.2	⊢ 𝐵 ∈ ℝ
ltlei.1	⊢ 𝐴 < 𝐵

Assertion

Ref	Expression
ltleii	⊢ 𝐴 ≤ 𝐵

Proof of Theorem ltleii

Step	Hyp	Ref	Expression
1		ltlei.1	. 2 ⊢ 𝐴 < 𝐵
2		lt.1	. . 3 ⊢ 𝐴 ∈ ℝ
3		lt.2	. . 3 ⊢ 𝐵 ∈ ℝ
4	2, 3	ltlei 11332	. 2 ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)
5	1, 4	ax-mp 5	1 ⊢ 𝐴 ≤ 𝐵

Syntax hints:   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-pre-lttri 11180

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  0le1  11733  ledivp1i  12135  ltdivp1i  12136  1le2  12417  1le3  12420  halfge0  12425  decleh  12708  eluz4eluz2  12865  uzuzle23  12869  fz0to4untppr  13600  fzo0to42pr  13715  faclbnd4lem1  14249  4bc2eq6  14285  sqrt9  15216  sqrt2gt1lt2  15217  absrdbnd  15284  sqrtpclii  15325  0.999...  15823  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  cos2bnd  16127  rpnnen2lem3  16155  rpnnen2lem4  16156  rpnnen2lem9  16161  rpnnen2lem12  16164  flodddiv4  16352  strleun  17086  cnfldfunALTOLD  20950  elii1  24442  htpycc  24487  pcoval1  24520  pcocn  24524  pcohtpylem  24526  pcopt  24529  pcopt2  24530  pcoass  24531  pcorevlem  24533  vitalilem4  25119  vitali  25121  dveflem  25487  sinhalfpilem  25964  sincosq1lem  25998  sincos4thpi  26014  sincos6thpi  26016  pige3  26019  cos0pilt1  26032  tanregt0  26039  efif1olem4  26045  relogrn  26061  argregt0  26109  argrege0  26110  logneg2  26114  2logb9irr  26289  asin1  26388  reasinsin  26390  log2cnv  26438  log2tlbnd  26439  log2ub  26443  harmonicbnd3  26501  ppiublem1  26694  ppiub  26696  bposlem3  26778  bposlem4  26779  bposlem5  26780  bposlem7  26782  bposlem8  26783  bposlem9  26784  lgsdir2lem1  26817  chebbnd1lem3  26963  dchrvmasumlema  26992  logdivsum  27025  mulog2sumlem2  27027  pntpbnd1a  27077  pntpbnd2  27079  pntlemk  27098  istrkg3ld  27701  axlowdimlem16  28204  axlowdimlem17  28205  axlowdim  28208  usgrexmplef  28505  upgr4cycl4dv4e  29427  konigsbergiedgw  29490  konigsberglem1  29494  konigsberglem2  29495  konigsberglem3  29496  ex-fl  29689  ex-sqrt  29696  ex-gcd  29699  normlem6  30355  sqsscirc1  32876  prodfzo03  33603  hgt750lemd  33648  hgt750lem  33651  hgt750lem2  33652  hgt750leme  33658  tgoldbachgnn  33659  logi  34692  dnizeq0  35339  cnndvlem1  35401  bj-pinftyccb  36090  bj-pinftynminfty  36096  tan2h  36468  fdc  36601  jm2.20nn  41721  areaquad  41950  sineq0ALT  43683  halffl  43992  itgsin0pilem1  44652  itgsinexplem1  44656  wallispilem2  44768  wallispilem4  44770  stirlinglem15  44790  stirlingr  44792  fourierdlem62  44870  fourierdlem77  44885  fourierdlem102  44910  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fourierdlem112  44920  fourierdlem114  44922  sqwvfoura  44930  sqwvfourb  44931  fourierswlem  44932  fouriersw  44933  etransclem23  44959  etransclem46  44982  smfmullem4  45496  fmtnoprmfac2lem1  46220  fmtno4prmfac  46226  31prm  46251  mod42tp1mod8  46256  2exp340mod341  46387  341fppr2  46388  9fppr8  46391  nfermltl8rev  46396  nfermltl2rev  46397  sbgoldbo  46441  nnsum3primes4  46442  nnsum3primesgbe  46446  nnsum4primeseven  46454  nnsum4primesevenALTV  46455  wtgoldbnnsum4prm  46456  bgoldbnnsum3prm  46458  tgblthelfgott  46469  ackval42  47335  itsclc0yqsollem2  47402  sepfsepc  47513