Theorem ltleii 11357

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123   < clt 11267   ≤ cle 11268

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  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 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  0le1  11761  ledivp1i  12164  ltdivp1i  12165  0le2  12367  2le3  12439  1le2  12476  1le3  12479  halfge0  12484  decleh  12776  8lt10  12874  7lt10  12875  6lt10  12876  5lt10  12877  4lt10  12878  3lt10  12879  2lt10  12880  1lt10  12881  5eluz3  12932  uzuzle23  12933  uzuzle24  12934  uzuzle34  12935  fz0to4untppr  13685  fz0to5un2tp  13686  fzo0to42pr  13809  faclbnd4lem1  14357  4bc2eq6  14393  sqrt9  15360  sqrt2gt1lt2  15361  absrdbnd  15429  sqrtpclii  15470  0.999...  15970  ef01bndlem  16272  sin01bnd  16273  cos01bnd  16274  cos2bnd  16276  rpnnen2lem3  16304  rpnnen2lem4  16305  rpnnen2lem9  16310  rpnnen2lem12  16313  flodddiv4  16505  strleun  17249  chnub  18710  elii1  25163  htpycc  25208  pcoval1  25241  pcocn  25245  pcohtpylem  25247  pcopt  25250  pcopt2  25251  pcoass  25252  pcorevlem  25254  vitalilem4  25839  vitali  25841  dveflem  26206  pige0  26697  sinhalfpilem  26701  sincosq1lem  26735  sincos4thpi  26751  sincos6thpi  26753  pige3  26756  cos0pilt1  26769  tanregt0  26776  efif1olem4  26782  relogrn  26798  logi  26824  argregt0  26847  argrege0  26848  logneg2  26852  2logb9irr  27032  asin1  27131  reasinsin  27133  log2cnv  27181  log2tlbnd  27182  log2ub  27186  harmonicbnd3  27244  ppiublem1  27438  ppiub  27440  bposlem3  27522  bposlem4  27523  bposlem5  27524  bposlem7  27526  bposlem8  27527  bposlem9  27528  lgsdir2lem1  27561  chebbnd1lem3  27707  dchrvmasumlema  27736  logdivsum  27769  mulog2sumlem2  27771  pntpbnd1a  27821  pntpbnd2  27823  pntlemk  27842  istrkg3ld  28802  axlowdimlem16  29414  axlowdimlem17  29415  axlowdim  29418  usgrexmplef  29719  upgr4cycl4dv4e  30665  konigsbergiedgw  30728  konigsberglem1  30732  konigsberglem2  30733  konigsberglem3  30734  ex-fl  30927  ex-sqrt  30934  ex-gcd  30937  normlem6  31596  2sqr3minply  34290  cos9thpiminplylem1  34292  sqsscirc1  34418  prodfzo03  35111  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  hgt750leme  35166  tgoldbachgnn  35167  dnizeq0  37172  cnndvlem1  37234  bj-pinftyccb  37973  bj-pinftynminfty  37979  tan2h  38366  fdc  38495  asin1half  43232  areaquad  44057  sineq0ALT  45759  halffl  46129  itgsin0pilem1  46778  itgsinexplem1  46782  wallispilem2  46894  wallispilem4  46896  stirlingr  46918  fourierdlem62  46996  fourierdlem77  47011  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fourierdlem114  47048  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  etransclem23  47085  etransclem46  47108  smfmullem4  47622  ceilhalf1  48226  fmtnoprmfac2lem1  48469  fmtno4prmfac  48475  31prm  48500  mod42tp1mod8  48505  nprmdvdsfacm1lem4  48526  nprmdvdsfacm1  48527  ppivalnnnprmge6  48529  2exp340mod341  48649  341fppr2  48650  9fppr8  48653  nfermltl8rev  48658  nfermltl2rev  48659  sbgoldbo  48703  nnsum3primes4  48704  nnsum3primesgbe  48708  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  wtgoldbnnsum4prm  48718  bgoldbnnsum3prm  48720  tgblthelfgott  48731  cycl3grtri  48863  usgrexmpl1lem  48937  usgrexmpl2lem  48942  gpgusgralem  48972  gpg5nbgrvtx13starlem2  48988  gpg5nbgr3star  48997  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  ackval42  49626  itsclc0yqsollem2  49693  sepfsepc  49854  veronesev1lem  50806  veronesev2lem  50807  veronesev3lem  50808  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811  veronesevrowd  50812  veronesematrowd  50814  veroquadgsumlem  50816  veroquadmodzerod  50817  veroquadnolindfd  50818