Theorem ltleii 11382

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

Syntax hints:   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152   < clt 11293   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-pre-lttri 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299

This theorem is referenced by:  0le1  11784  ledivp1i  12191  ltdivp1i  12192  1le2  12473  1le3  12476  halfge0  12481  decleh  12766  eluz4eluz2  12923  eluz4eluz3  12924  5eluz3  12925  uzuzle23  12929  fz0to4untppr  13667  fz0to5un2tp  13668  fzo0to42pr  13789  faclbnd4lem1  14329  4bc2eq6  14365  sqrt9  15309  sqrt2gt1lt2  15310  absrdbnd  15377  sqrtpclii  15418  0.999...  15914  ef01bndlem  16217  sin01bnd  16218  cos01bnd  16219  cos2bnd  16221  rpnnen2lem3  16249  rpnnen2lem4  16250  rpnnen2lem9  16255  rpnnen2lem12  16258  flodddiv4  16449  strleun  17191  cnfldfunALTOLDOLD  21411  elii1  24978  htpycc  25026  pcoval1  25060  pcocn  25064  pcohtpylem  25066  pcopt  25069  pcopt2  25070  pcoass  25071  pcorevlem  25073  vitalilem4  25660  vitali  25662  dveflem  26032  sinhalfpilem  26520  sincosq1lem  26554  sincos4thpi  26570  sincos6thpi  26573  pige3  26576  cos0pilt1  26589  tanregt0  26596  efif1olem4  26602  relogrn  26618  logi  26644  argregt0  26667  argrege0  26668  logneg2  26672  2logb9irr  26853  asin1  26952  reasinsin  26954  log2cnv  27002  log2tlbnd  27003  log2ub  27007  harmonicbnd3  27066  ppiublem1  27261  ppiub  27263  bposlem3  27345  bposlem4  27346  bposlem5  27347  bposlem7  27349  bposlem8  27350  bposlem9  27351  lgsdir2lem1  27384  chebbnd1lem3  27530  dchrvmasumlema  27559  logdivsum  27592  mulog2sumlem2  27594  pntpbnd1a  27644  pntpbnd2  27646  pntlemk  27665  istrkg3ld  28484  axlowdimlem16  28987  axlowdimlem17  28988  axlowdim  28991  usgrexmplef  29291  upgr4cycl4dv4e  30214  konigsbergiedgw  30277  konigsberglem1  30281  konigsberglem2  30282  konigsberglem3  30283  ex-fl  30476  ex-sqrt  30483  ex-gcd  30486  normlem6  31144  chnub  32986  2sqr3minply  33753  sqsscirc1  33869  prodfzo03  34597  hgt750lemd  34642  hgt750lem  34645  hgt750lem2  34646  hgt750leme  34652  tgoldbachgnn  34653  dnizeq0  36458  cnndvlem1  36520  bj-pinftyccb  37204  bj-pinftynminfty  37210  tan2h  37599  fdc  37732  asin1half  42366  jm2.20nn  42986  areaquad  43205  sineq0ALT  44935  halffl  45247  itgsin0pilem1  45906  itgsinexplem1  45910  wallispilem2  46022  wallispilem4  46024  stirlinglem15  46044  stirlingr  46046  fourierdlem62  46124  fourierdlem77  46139  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem111  46173  fourierdlem112  46174  fourierdlem114  46176  sqwvfoura  46184  sqwvfourb  46185  fourierswlem  46186  fouriersw  46187  etransclem23  46213  etransclem46  46236  smfmullem4  46750  fmtnoprmfac2lem1  47491  fmtno4prmfac  47497  31prm  47522  mod42tp1mod8  47527  2exp340mod341  47658  341fppr2  47659  9fppr8  47662  nfermltl8rev  47667  nfermltl2rev  47668  sbgoldbo  47712  nnsum3primes4  47713  nnsum3primesgbe  47717  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  wtgoldbnnsum4prm  47727  bgoldbnnsum3prm  47729  tgblthelfgott  47740  usgrexmpl1lem  47916  usgrexmpl2lem  47921  gpgusgralem  47946  gpg5nbgrvtx13starlem2  47963  gpg5nbgr3star  47972  ackval42  48546  itsclc0yqsollem2  48613  sepfsepc  48724