Theorem ltleii 11260

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  0le1  11664  ledivp1i  12072  ltdivp1i  12073  1le2  12376  1le3  12379  halfge0  12384  decleh  12670  5eluz3  12824  uzuzle23  12825  uzuzle24  12826  uzuzle34  12827  fz0to4untppr  13575  fz0to5un2tp  13576  fzo0to42pr  13699  faclbnd4lem1  14246  4bc2eq6  14282  sqrt9  15226  sqrt2gt1lt2  15227  absrdbnd  15295  sqrtpclii  15336  0.999...  15837  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos2bnd  16146  rpnnen2lem3  16174  rpnnen2lem4  16175  rpnnen2lem9  16180  rpnnen2lem12  16183  flodddiv4  16375  strleun  17118  chnub  18579  elii1  24912  htpycc  24957  pcoval1  24990  pcocn  24994  pcohtpylem  24996  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  vitalilem4  25588  vitali  25590  dveflem  25956  sinhalfpilem  26440  sincosq1lem  26474  sincos4thpi  26490  sincos6thpi  26493  pige3  26496  cos0pilt1  26509  tanregt0  26516  efif1olem4  26522  relogrn  26538  logi  26564  argregt0  26587  argrege0  26588  logneg2  26592  2logb9irr  26772  asin1  26871  reasinsin  26873  log2cnv  26921  log2tlbnd  26922  log2ub  26926  harmonicbnd3  26985  ppiublem1  27179  ppiub  27181  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem7  27267  bposlem8  27268  bposlem9  27269  lgsdir2lem1  27302  chebbnd1lem3  27448  dchrvmasumlema  27477  logdivsum  27510  mulog2sumlem2  27512  pntpbnd1a  27562  pntpbnd2  27564  pntlemk  27583  istrkg3ld  28543  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  usgrexmplef  29342  upgr4cycl4dv4e  30270  konigsbergiedgw  30333  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  ex-fl  30532  ex-sqrt  30539  ex-gcd  30542  normlem6  31201  2sqr3minply  33940  cos9thpiminplylem1  33942  sqsscirc1  34068  prodfzo03  34763  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  hgt750leme  34818  tgoldbachgnn  34819  dnizeq0  36751  cnndvlem1  36813  bj-pinftyccb  37551  bj-pinftynminfty  37557  tan2h  37947  fdc  38080  asin1half  42803  jm2.20nn  43443  areaquad  43662  sineq0ALT  45381  halffl  45747  itgsin0pilem1  46396  itgsinexplem1  46400  wallispilem2  46512  wallispilem4  46514  stirlinglem15  46534  stirlingr  46536  fourierdlem62  46614  fourierdlem77  46629  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  etransclem23  46703  etransclem46  46726  smfmullem4  47240  ceilhalf1  47798  fmtnoprmfac2lem1  48041  fmtno4prmfac  48047  31prm  48072  mod42tp1mod8  48077  nprmdvdsfacm1lem4  48098  nprmdvdsfacm1  48099  ppivalnnnprmge6  48101  2exp340mod341  48221  341fppr2  48222  9fppr8  48225  nfermltl8rev  48230  nfermltl2rev  48231  sbgoldbo  48275  nnsum3primes4  48276  nnsum3primesgbe  48280  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  tgblthelfgott  48303  cycl3grtri  48435  usgrexmpl1lem  48509  usgrexmpl2lem  48514  gpgusgralem  48544  gpg5nbgrvtx13starlem2  48560  gpg5nbgr3star  48569  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  ackval42  49184  itsclc0yqsollem2  49251  sepfsepc  49415