Theorem ltleii 11258

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027   < clt 11168   ≤ cle 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-pre-lttri 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  0le1  11662  ledivp1i  12069  ltdivp1i  12070  1le2  12351  1le3  12354  halfge0  12359  decleh  12645  5eluz3  12803  uzuzle23  12804  uzuzle24  12805  uzuzle34  12806  fz0to4untppr  13552  fz0to5un2tp  13553  fzo0to42pr  13675  faclbnd4lem1  14219  4bc2eq6  14255  sqrt9  15199  sqrt2gt1lt2  15200  absrdbnd  15268  sqrtpclii  15309  0.999...  15807  ef01bndlem  16112  sin01bnd  16113  cos01bnd  16114  cos2bnd  16116  rpnnen2lem3  16144  rpnnen2lem4  16145  rpnnen2lem9  16150  rpnnen2lem12  16153  flodddiv4  16345  strleun  17087  elii1  24848  htpycc  24896  pcoval1  24930  pcocn  24934  pcohtpylem  24936  pcopt  24939  pcopt2  24940  pcoass  24941  pcorevlem  24943  vitalilem4  25529  vitali  25531  dveflem  25900  sinhalfpilem  26389  sincosq1lem  26423  sincos4thpi  26439  sincos6thpi  26442  pige3  26445  cos0pilt1  26458  tanregt0  26465  efif1olem4  26471  relogrn  26487  logi  26513  argregt0  26536  argrege0  26537  logneg2  26541  2logb9irr  26722  asin1  26821  reasinsin  26823  log2cnv  26871  log2tlbnd  26872  log2ub  26876  harmonicbnd3  26935  ppiublem1  27130  ppiub  27132  bposlem3  27214  bposlem4  27215  bposlem5  27216  bposlem7  27218  bposlem8  27219  bposlem9  27220  lgsdir2lem1  27253  chebbnd1lem3  27399  dchrvmasumlema  27428  logdivsum  27461  mulog2sumlem2  27463  pntpbnd1a  27513  pntpbnd2  27515  pntlemk  27534  istrkg3ld  28425  axlowdimlem16  28921  axlowdimlem17  28922  axlowdim  28925  usgrexmplef  29223  upgr4cycl4dv4e  30148  konigsbergiedgw  30211  konigsberglem1  30215  konigsberglem2  30216  konigsberglem3  30217  ex-fl  30410  ex-sqrt  30417  ex-gcd  30420  normlem6  31078  chnub  32973  2sqr3minply  33766  cos9thpiminplylem1  33768  sqsscirc1  33894  prodfzo03  34590  hgt750lemd  34635  hgt750lem  34638  hgt750lem2  34639  hgt750leme  34645  tgoldbachgnn  34646  dnizeq0  36468  cnndvlem1  36530  bj-pinftyccb  37214  bj-pinftynminfty  37220  tan2h  37611  fdc  37744  asin1half  42350  jm2.20nn  42990  areaquad  43209  sineq0ALT  44930  halffl  45298  itgsin0pilem1  45951  itgsinexplem1  45955  wallispilem2  46067  wallispilem4  46069  stirlinglem15  46089  stirlingr  46091  fourierdlem62  46169  fourierdlem77  46184  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fourierdlem112  46219  fourierdlem114  46221  sqwvfoura  46229  sqwvfourb  46230  fourierswlem  46231  fouriersw  46232  etransclem23  46258  etransclem46  46281  smfmullem4  46795  ceilhalf1  47338  fmtnoprmfac2lem1  47570  fmtno4prmfac  47576  31prm  47601  mod42tp1mod8  47606  2exp340mod341  47737  341fppr2  47738  9fppr8  47741  nfermltl8rev  47746  nfermltl2rev  47747  sbgoldbo  47791  nnsum3primes4  47792  nnsum3primesgbe  47796  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  tgblthelfgott  47819  cycl3grtri  47951  usgrexmpl1lem  48025  usgrexmpl2lem  48030  gpgusgralem  48060  gpg5nbgrvtx13starlem2  48076  gpg5nbgr3star  48085  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  ackval42  48701  itsclc0yqsollem2  48768  sepfsepc  48932