Theorem ltleii 10766

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

Syntax hints:   ∈ wcel 2113   class class class wbr 5069  ℝcr 10539   < clt 10678   ≤ cle 10679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464  ax-resscn 10597  ax-pre-lttri 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-nel 3127  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8292  df-en 8513  df-dom 8514  df-sdom 8515  df-pnf 10680  df-mnf 10681  df-xr 10682  df-ltxr 10683  df-le 10684

This theorem is referenced by:  0le1  11166  ledivp1i  11568  ltdivp1i  11569  1le2  11849  1le3  11852  halfge0  11857  decleh  12136  eluz4eluz2  12288  uzuzle23  12292  fz0to4untppr  13013  fzo0to42pr  13127  faclbnd4lem1  13656  4bc2eq6  13692  sqrt9  14636  sqrt2gt1lt2  14637  absrdbnd  14704  sqrtpclii  14745  0.999...  15240  ef01bndlem  15540  sin01bnd  15541  cos01bnd  15542  cos2bnd  15544  rpnnen2lem3  15572  rpnnen2lem4  15573  rpnnen2lem9  15578  rpnnen2lem12  15581  flodddiv4  15767  strleun  16594  cnfldfun  20560  elii1  23542  htpycc  23587  pcoval1  23620  pcocn  23624  pcohtpylem  23626  pcopt  23629  pcopt2  23630  pcoass  23631  pcorevlem  23633  vitalilem4  24215  vitali  24217  dveflem  24579  sinhalfpilem  25052  sincosq1lem  25086  sincos4thpi  25102  sincos6thpi  25104  pige3  25107  tanregt0  25126  efif1olem4  25132  relogrn  25148  argregt0  25196  argrege0  25197  logneg2  25201  2logb9irr  25376  asin1  25475  reasinsin  25477  log2cnv  25525  log2tlbnd  25526  log2ub  25530  harmonicbnd3  25588  ppiublem1  25781  ppiub  25783  bposlem3  25865  bposlem4  25866  bposlem5  25867  bposlem7  25869  bposlem8  25870  bposlem9  25871  lgsdir2lem1  25904  chebbnd1lem3  26050  dchrvmasumlema  26079  logdivsum  26112  mulog2sumlem2  26114  pntpbnd1a  26164  pntpbnd2  26166  pntlemk  26185  istrkg3ld  26250  axlowdimlem16  26746  axlowdimlem17  26747  axlowdim  26750  usgrexmplef  27044  upgr4cycl4dv4e  27967  konigsbergiedgw  28030  konigsberglem1  28034  konigsberglem2  28035  konigsberglem3  28036  ex-fl  28229  ex-sqrt  28236  ex-gcd  28239  normlem6  28895  sqsscirc1  31155  prodfzo03  31878  hgt750lemd  31923  hgt750lem  31926  hgt750lem2  31927  hgt750leme  31933  tgoldbachgnn  31934  logi  32970  dnizeq0  33818  cnndvlem1  33880  bj-pinftyccb  34507  bj-pinftynminfty  34513  tan2h  34888  fdc  35024  jm2.20nn  39600  areaquad  39829  sineq0ALT  41277  halffl  41569  itgsin0pilem1  42241  itgsinexplem1  42245  wallispilem2  42358  wallispilem4  42360  stirlinglem15  42380  stirlingr  42382  fourierdlem62  42460  fourierdlem77  42475  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  fourierdlem114  42512  sqwvfoura  42520  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  etransclem23  42549  etransclem46  42572  smfmullem4  43076  fmtnoprmfac2lem1  43735  fmtno4prmfac  43741  31prm  43767  mod42tp1mod8  43774  2exp340mod341  43905  341fppr2  43906  9fppr8  43909  nfermltl8rev  43914  nfermltl2rev  43915  sbgoldbo  43959  nnsum3primes4  43960  nnsum3primesgbe  43964  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  wtgoldbnnsum4prm  43974  bgoldbnnsum3prm  43976  tgblthelfgott  43987  itsclc0yqsollem2  44757