Theorem ltleii 10752

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

Syntax hints:   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525   < clt 10664   ≤ cle 10665

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-pre-lttri 10600

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670

This theorem is referenced by:  0le1  11152  ledivp1i  11554  ltdivp1i  11555  1le2  11834  1le3  11837  halfge0  11842  decleh  12121  eluz4eluz2  12273  uzuzle23  12277  fz0to4untppr  13005  fzo0to42pr  13119  faclbnd4lem1  13649  4bc2eq6  13685  sqrt9  14625  sqrt2gt1lt2  14626  absrdbnd  14693  sqrtpclii  14734  0.999...  15229  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos2bnd  15533  rpnnen2lem3  15561  rpnnen2lem4  15562  rpnnen2lem9  15567  rpnnen2lem12  15570  flodddiv4  15754  strleun  16583  cnfldfun  20103  elii1  23540  htpycc  23585  pcoval1  23618  pcocn  23622  pcohtpylem  23624  pcopt  23627  pcopt2  23628  pcoass  23629  pcorevlem  23631  vitalilem4  24215  vitali  24217  dveflem  24582  sinhalfpilem  25056  sincosq1lem  25090  sincos4thpi  25106  sincos6thpi  25108  pige3  25111  cos0pilt1  25124  tanregt0  25131  efif1olem4  25137  relogrn  25153  argregt0  25201  argrege0  25202  logneg2  25206  2logb9irr  25381  asin1  25480  reasinsin  25482  log2cnv  25530  log2tlbnd  25531  log2ub  25535  harmonicbnd3  25593  ppiublem1  25786  ppiub  25788  bposlem3  25870  bposlem4  25871  bposlem5  25872  bposlem7  25874  bposlem8  25875  bposlem9  25876  lgsdir2lem1  25909  chebbnd1lem3  26055  dchrvmasumlema  26084  logdivsum  26117  mulog2sumlem2  26119  pntpbnd1a  26169  pntpbnd2  26171  pntlemk  26190  istrkg3ld  26255  axlowdimlem16  26751  axlowdimlem17  26752  axlowdim  26755  usgrexmplef  27049  upgr4cycl4dv4e  27970  konigsbergiedgw  28033  konigsberglem1  28037  konigsberglem2  28038  konigsberglem3  28039  ex-fl  28232  ex-sqrt  28239  ex-gcd  28242  normlem6  28898  sqsscirc1  31261  prodfzo03  31984  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  hgt750leme  32039  tgoldbachgnn  32040  logi  33079  dnizeq0  33927  cnndvlem1  33989  bj-pinftyccb  34636  bj-pinftynminfty  34642  tan2h  35049  fdc  35183  jm2.20nn  39938  areaquad  40166  sineq0ALT  41643  halffl  41928  itgsin0pilem1  42592  itgsinexplem1  42596  wallispilem2  42708  wallispilem4  42710  stirlinglem15  42730  stirlingr  42732  fourierdlem62  42810  fourierdlem77  42825  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem114  42862  sqwvfoura  42870  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  etransclem23  42899  etransclem46  42922  smfmullem4  43426  fmtnoprmfac2lem1  44083  fmtno4prmfac  44089  31prm  44114  mod42tp1mod8  44120  2exp340mod341  44251  341fppr2  44252  9fppr8  44255  nfermltl8rev  44260  nfermltl2rev  44261  sbgoldbo  44305  nnsum3primes4  44306  nnsum3primesgbe  44310  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  tgblthelfgott  44333  ackval42  45110  itsclc0yqsollem2  45177