Theorem ltleii 11256

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

Syntax hints:   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttri 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  0le1  11660  ledivp1i  12067  ltdivp1i  12068  1le2  12349  1le3  12352  halfge0  12357  decleh  12642  5eluz3  12796  uzuzle23  12797  uzuzle24  12798  uzuzle34  12799  fz0to4untppr  13546  fz0to5un2tp  13547  fzo0to42pr  13669  faclbnd4lem1  14216  4bc2eq6  14252  sqrt9  15196  sqrt2gt1lt2  15197  absrdbnd  15265  sqrtpclii  15306  0.999...  15804  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos2bnd  16113  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  rpnnen2lem12  16150  flodddiv4  16342  strleun  17084  chnub  18545  elii1  24887  htpycc  24935  pcoval1  24969  pcocn  24973  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  vitalilem4  25568  vitali  25570  dveflem  25939  sinhalfpilem  26428  sincosq1lem  26462  sincos4thpi  26478  sincos6thpi  26481  pige3  26484  cos0pilt1  26497  tanregt0  26504  efif1olem4  26510  relogrn  26526  logi  26552  argregt0  26575  argrege0  26576  logneg2  26580  2logb9irr  26761  asin1  26860  reasinsin  26862  log2cnv  26910  log2tlbnd  26911  log2ub  26915  harmonicbnd3  26974  ppiublem1  27169  ppiub  27171  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  chebbnd1lem3  27438  dchrvmasumlema  27467  logdivsum  27500  mulog2sumlem2  27502  pntpbnd1a  27552  pntpbnd2  27554  pntlemk  27573  istrkg3ld  28533  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  usgrexmplef  29332  upgr4cycl4dv4e  30260  konigsbergiedgw  30323  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  ex-fl  30522  ex-sqrt  30529  ex-gcd  30532  normlem6  31190  2sqr3minply  33937  cos9thpiminplylem1  33939  sqsscirc1  34065  prodfzo03  34760  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  tgoldbachgnn  34816  dnizeq0  36675  cnndvlem1  36737  bj-pinftyccb  37426  bj-pinftynminfty  37432  tan2h  37813  fdc  37946  asin1half  42612  jm2.20nn  43239  areaquad  43458  sineq0ALT  45177  halffl  45544  itgsin0pilem1  46194  itgsinexplem1  46198  wallispilem2  46310  wallispilem4  46312  stirlinglem15  46332  stirlingr  46334  fourierdlem62  46412  fourierdlem77  46427  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fourierdlem114  46464  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem23  46501  etransclem46  46524  smfmullem4  47038  ceilhalf1  47580  fmtnoprmfac2lem1  47812  fmtno4prmfac  47818  31prm  47843  mod42tp1mod8  47848  2exp340mod341  47979  341fppr2  47980  9fppr8  47983  nfermltl8rev  47988  nfermltl2rev  47989  sbgoldbo  48033  nnsum3primes4  48034  nnsum3primesgbe  48038  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  tgblthelfgott  48061  cycl3grtri  48193  usgrexmpl1lem  48267  usgrexmpl2lem  48272  gpgusgralem  48302  gpg5nbgrvtx13starlem2  48318  gpg5nbgr3star  48327  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  ackval42  48942  itsclc0yqsollem2  49009  sepfsepc  49173