Theorem ltleii 10499

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

Syntax hints:   ∈ wcel 2107   class class class wbr 4886  ℝcr 10271   < clt 10411   ≤ cle 10412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-pre-lttri 10346

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417

This theorem is referenced by:  0le1  10898  ledivp1i  11303  ltdivp1i  11304  1le2  11591  1le3  11594  halfge0  11599  decleh  11881  uzuzle23  12035  fz0to4untppr  12761  fzo0to42pr  12874  faclbnd4lem1  13398  4bc2eq6  13434  sqrt9  14421  sqrt2gt1lt2  14422  absrdbnd  14488  sqrtpclii  14529  0.999...  15016  ef01bndlem  15316  sin01bnd  15317  cos01bnd  15318  cos2bnd  15320  rpnnen2lem3  15349  rpnnen2lem4  15350  rpnnen2lem9  15355  rpnnen2lem12  15358  flodddiv4  15543  strleun  16364  cnfldfun  20154  elii1  23142  htpycc  23187  pcoval1  23220  pco0  23221  pcoval2  23223  pcocn  23224  pcohtpylem  23226  pcopt  23229  pcopt2  23230  pcoass  23231  pcorevlem  23233  vitalilem4  23815  vitali  23817  mbfi1fseqlem6  23924  dveflem  24179  sinhalfpilem  24653  sincosq1lem  24687  sincos4thpi  24703  sincos6thpi  24705  tanregt0  24723  efif1olem4  24729  relogrn  24745  argregt0  24793  argrege0  24794  logneg2  24798  2logb9irr  24973  heron  25016  asin1  25072  reasinsin  25074  log2cnv  25123  log2tlbnd  25124  log2ub  25128  harmonicbnd3  25186  ppiublem1  25379  ppiub  25381  bposlem3  25463  bposlem4  25464  bposlem5  25465  bposlem7  25467  bposlem8  25468  bposlem9  25469  lgsdir2lem1  25502  chebbnd1lem3  25612  dchrvmasumlema  25641  logdivsum  25674  mulog2sumlem2  25676  pntpbnd1a  25726  pntpbnd2  25728  pntlemk  25747  istrkg3ld  25812  axlowdimlem16  26306  axlowdimlem17  26307  axlowdim  26310  usgrexmplef  26606  upgr4cycl4dv4e  27588  konigsbergiedgw  27654  konigsberglem1  27658  konigsberglem2  27659  konigsberglem3  27660  ex-fl  27879  ex-sqrt  27886  ex-gcd  27889  normlem6  28544  sqsscirc1  30552  prodfzo03  31283  hgt750lemd  31328  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  tgoldbachgnn  31339  logi  32214  dnizeq0  33048  cnndvlem1  33110  bj-pinftyccb  33698  bj-pinftynminfty  33704  tan2h  34026  fdc  34165  jm2.20nn  38523  areaquad  38760  sineq0ALT  40106  halffl  40419  itgsin0pilem1  41093  itgsinexplem1  41097  wallispilem2  41210  wallispilem4  41212  stirlinglem15  41232  stirlingr  41234  fourierdlem62  41312  fourierdlem77  41327  fourierdlem102  41352  fourierdlem103  41353  fourierdlem104  41354  fourierdlem111  41361  fourierdlem112  41362  fourierdlem114  41364  sqwvfoura  41372  sqwvfourb  41373  fourierswlem  41374  fouriersw  41375  etransclem23  41401  etransclem46  41424  smfmullem4  41928  fmtnoprmfac2lem1  42499  fmtno4prmfac  42505  31prm  42533  mod42tp1mod8  42540  sbgoldbo  42700  nnsum3primes4  42701  nnsum3primesgbe  42705  nnsum4primeseven  42713  nnsum4primesevenALTV  42714  wtgoldbnnsum4prm  42715  bgoldbnnsum3prm  42717  tgblthelfgott  42728  itsclc0yqsollem2  43499