Theorem ltleii 10844

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5031  ℝcr 10617   < clt 10756   ≤ cle 10757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-resscn 10675  ax-pre-lttri 10692

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-er 8323  df-en 8559  df-dom 8560  df-sdom 8561  df-pnf 10758  df-mnf 10759  df-xr 10760  df-ltxr 10761  df-le 10762

This theorem is referenced by:  0le1  11244  ledivp1i  11646  ltdivp1i  11647  1le2  11928  1le3  11931  halfge0  11936  decleh  12217  eluz4eluz2  12370  uzuzle23  12374  fz0to4untppr  13104  fzo0to42pr  13218  faclbnd4lem1  13748  4bc2eq6  13784  sqrt9  14726  sqrt2gt1lt2  14727  absrdbnd  14794  sqrtpclii  14835  0.999...  15332  ef01bndlem  15632  sin01bnd  15633  cos01bnd  15634  cos2bnd  15636  rpnnen2lem3  15664  rpnnen2lem4  15665  rpnnen2lem9  15670  rpnnen2lem12  15673  flodddiv4  15861  strleun  16697  cnfldfun  20232  elii1  23690  htpycc  23735  pcoval1  23768  pcocn  23772  pcohtpylem  23774  pcopt  23777  pcopt2  23778  pcoass  23779  pcorevlem  23781  vitalilem4  24366  vitali  24368  dveflem  24734  sinhalfpilem  25211  sincosq1lem  25245  sincos4thpi  25261  sincos6thpi  25263  pige3  25266  cos0pilt1  25279  tanregt0  25286  efif1olem4  25292  relogrn  25308  argregt0  25356  argrege0  25357  logneg2  25361  2logb9irr  25536  asin1  25635  reasinsin  25637  log2cnv  25685  log2tlbnd  25686  log2ub  25690  harmonicbnd3  25748  ppiublem1  25941  ppiub  25943  bposlem3  26025  bposlem4  26026  bposlem5  26027  bposlem7  26029  bposlem8  26030  bposlem9  26031  lgsdir2lem1  26064  chebbnd1lem3  26210  dchrvmasumlema  26239  logdivsum  26272  mulog2sumlem2  26274  pntpbnd1a  26324  pntpbnd2  26326  pntlemk  26345  istrkg3ld  26410  axlowdimlem16  26906  axlowdimlem17  26907  axlowdim  26910  usgrexmplef  27204  upgr4cycl4dv4e  28125  konigsbergiedgw  28188  konigsberglem1  28192  konigsberglem2  28193  konigsberglem3  28194  ex-fl  28387  ex-sqrt  28394  ex-gcd  28397  normlem6  29053  sqsscirc1  31433  prodfzo03  32156  hgt750lemd  32201  hgt750lem  32204  hgt750lem2  32205  hgt750leme  32211  tgoldbachgnn  32212  logi  33276  dnizeq0  34301  cnndvlem1  34363  bj-pinftyccb  35036  bj-pinftynminfty  35042  tan2h  35415  fdc  35549  jm2.20nn  40414  areaquad  40642  sineq0ALT  42118  halffl  42396  itgsin0pilem1  43056  itgsinexplem1  43060  wallispilem2  43172  wallispilem4  43174  stirlinglem15  43194  stirlingr  43196  fourierdlem62  43274  fourierdlem77  43289  fourierdlem102  43314  fourierdlem103  43315  fourierdlem104  43316  fourierdlem111  43323  fourierdlem112  43324  fourierdlem114  43326  sqwvfoura  43334  sqwvfourb  43335  fourierswlem  43336  fouriersw  43337  etransclem23  43363  etransclem46  43386  smfmullem4  43890  fmtnoprmfac2lem1  44582  fmtno4prmfac  44588  31prm  44613  mod42tp1mod8  44618  2exp340mod341  44749  341fppr2  44750  9fppr8  44753  nfermltl8rev  44758  nfermltl2rev  44759  sbgoldbo  44803  nnsum3primes4  44804  nnsum3primesgbe  44808  nnsum4primeseven  44816  nnsum4primesevenALTV  44817  wtgoldbnnsum4prm  44818  bgoldbnnsum3prm  44820  tgblthelfgott  44831  ackval42  45606  itsclc0yqsollem2  45673  sepfsepc  45773