Theorem ltleii 11329

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

Syntax hints:   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095   < clt 11239   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-pre-lttri 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  0le1  11733  ledivp1i  12136  ltdivp1i  12137  0le2  12339  2le3  12411  1le2  12448  1le3  12451  halfge0  12456  decleh  12747  8lt10  12845  7lt10  12846  6lt10  12847  5lt10  12848  4lt10  12849  3lt10  12850  2lt10  12851  1lt10  12852  5eluz3  12903  uzuzle23  12904  uzuzle24  12905  uzuzle34  12906  fz0to4untppr  13654  fz0to5un2tp  13655  fzo0to42pr  13778  faclbnd4lem1  14325  4bc2eq6  14361  sqrt9  15320  sqrt2gt1lt2  15321  absrdbnd  15389  sqrtpclii  15430  0.999...  15931  ef01bndlem  16236  sin01bnd  16237  cos01bnd  16238  cos2bnd  16240  rpnnen2lem3  16268  rpnnen2lem4  16269  rpnnen2lem9  16274  rpnnen2lem12  16277  flodddiv4  16469  strleun  17213  chnub  18674  elii1  25059  htpycc  25104  pcoval1  25137  pcocn  25141  pcohtpylem  25143  pcopt  25146  pcopt2  25147  pcoass  25148  pcorevlem  25150  vitalilem4  25735  vitali  25737  dveflem  26103  pige0  26586  sinhalfpilem  26590  sincosq1lem  26624  sincos4thpi  26640  sincos6thpi  26643  pige3  26646  cos0pilt1  26659  tanregt0  26666  efif1olem4  26672  relogrn  26688  logi  26714  argregt0  26737  argrege0  26738  logneg2  26742  2logb9irr  26922  asin1  27021  reasinsin  27023  log2cnv  27071  log2tlbnd  27072  log2ub  27076  harmonicbnd3  27134  ppiublem1  27328  ppiub  27330  bposlem3  27412  bposlem4  27413  bposlem5  27414  bposlem7  27416  bposlem8  27417  bposlem9  27418  lgsdir2lem1  27451  chebbnd1lem3  27597  dchrvmasumlema  27626  logdivsum  27659  mulog2sumlem2  27661  pntpbnd1a  27711  pntpbnd2  27713  pntlemk  27732  istrkg3ld  28692  axlowdimlem16  29244  axlowdimlem17  29245  axlowdim  29248  usgrexmplef  29546  upgr4cycl4dv4e  30473  konigsbergiedgw  30536  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  ex-fl  30735  ex-sqrt  30742  ex-gcd  30745  normlem6  31404  2sqr3minply  34111  cos9thpiminplylem1  34113  sqsscirc1  34239  prodfzo03  34931  hgt750lemd  34976  hgt750lem  34979  hgt750lem2  34980  hgt750leme  34986  tgoldbachgnn  34987  dnizeq0  36949  cnndvlem1  37011  bj-pinftyccb  37748  bj-pinftynminfty  37754  tan2h  38146  fdc  38279  asin1half  43001  areaquad  43828  sineq0ALT  45530  halffl  45900  itgsin0pilem1  46549  itgsinexplem1  46553  wallispilem2  46665  wallispilem4  46667  stirlingr  46689  fourierdlem62  46767  fourierdlem77  46782  fourierdlem102  46807  fourierdlem103  46808  fourierdlem104  46809  fourierdlem111  46816  fourierdlem112  46817  fourierdlem114  46819  sqwvfoura  46827  sqwvfourb  46828  fourierswlem  46829  fouriersw  46830  etransclem23  46856  etransclem46  46879  smfmullem4  47393  ceilhalf1  47957  fmtnoprmfac2lem1  48200  fmtno4prmfac  48206  31prm  48231  mod42tp1mod8  48236  nprmdvdsfacm1lem4  48257  nprmdvdsfacm1  48258  ppivalnnnprmge6  48260  2exp340mod341  48380  341fppr2  48381  9fppr8  48384  nfermltl8rev  48389  nfermltl2rev  48390  sbgoldbo  48434  nnsum3primes4  48435  nnsum3primesgbe  48439  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  wtgoldbnnsum4prm  48449  bgoldbnnsum3prm  48451  tgblthelfgott  48462  cycl3grtri  48594  usgrexmpl1lem  48668  usgrexmpl2lem  48673  gpgusgralem  48703  gpg5nbgrvtx13starlem2  48719  gpg5nbgr3star  48728  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  ackval42  49354  itsclc0yqsollem2  49421  sepfsepc  49584