Theorem ltleii 11028

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 11027	. 2 ⊢ (𝐴 < 𝐵 → 𝐴 ≤ 𝐵)
5	1, 4	ax-mp 5	1 ⊢ 𝐴 ≤ 𝐵

Syntax hints:   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  0le1  11428  ledivp1i  11830  ltdivp1i  11831  1le2  12112  1le3  12115  halfge0  12120  decleh  12401  eluz4eluz2  12554  uzuzle23  12558  fz0to4untppr  13288  fzo0to42pr  13402  faclbnd4lem1  13935  4bc2eq6  13971  sqrt9  14913  sqrt2gt1lt2  14914  absrdbnd  14981  sqrtpclii  15022  0.999...  15521  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos2bnd  15825  rpnnen2lem3  15853  rpnnen2lem4  15854  rpnnen2lem9  15859  rpnnen2lem12  15862  flodddiv4  16050  strleun  16786  cnfldfun  20522  elii1  24004  htpycc  24049  pcoval1  24082  pcocn  24086  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  vitalilem4  24680  vitali  24682  dveflem  25048  sinhalfpilem  25525  sincosq1lem  25559  sincos4thpi  25575  sincos6thpi  25577  pige3  25580  cos0pilt1  25593  tanregt0  25600  efif1olem4  25606  relogrn  25622  argregt0  25670  argrege0  25671  logneg2  25675  2logb9irr  25850  asin1  25949  reasinsin  25951  log2cnv  25999  log2tlbnd  26000  log2ub  26004  harmonicbnd3  26062  ppiublem1  26255  ppiub  26257  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem7  26343  bposlem8  26344  bposlem9  26345  lgsdir2lem1  26378  chebbnd1lem3  26524  dchrvmasumlema  26553  logdivsum  26586  mulog2sumlem2  26588  pntpbnd1a  26638  pntpbnd2  26640  pntlemk  26659  istrkg3ld  26726  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  usgrexmplef  27529  upgr4cycl4dv4e  28450  konigsbergiedgw  28513  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  ex-fl  28712  ex-sqrt  28719  ex-gcd  28722  normlem6  29378  sqsscirc1  31760  prodfzo03  32483  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  tgoldbachgnn  32539  logi  33606  dnizeq0  34582  cnndvlem1  34644  bj-pinftyccb  35319  bj-pinftynminfty  35325  tan2h  35696  fdc  35830  jm2.20nn  40735  areaquad  40963  sineq0ALT  42446  halffl  42725  itgsin0pilem1  43381  itgsinexplem1  43385  wallispilem2  43497  wallispilem4  43499  stirlinglem15  43519  stirlingr  43521  fourierdlem62  43599  fourierdlem77  43614  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem114  43651  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  etransclem23  43688  etransclem46  43711  smfmullem4  44215  fmtnoprmfac2lem1  44906  fmtno4prmfac  44912  31prm  44937  mod42tp1mod8  44942  2exp340mod341  45073  341fppr2  45074  9fppr8  45077  nfermltl8rev  45082  nfermltl2rev  45083  sbgoldbo  45127  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  tgblthelfgott  45155  ackval42  45930  itsclc0yqsollem2  45997  sepfsepc  46109