Theorem ltleii 11426

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

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 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342

This theorem is used by:  0le1  11832  ledivp1i  12235  ltdivp1i  12236  0le2  12438  2le3  12510  1le2  12547  1le3  12550  halfge0  12555  decleh  12847  8lt10  12945  7lt10  12946  6lt10  12947  5lt10  12948  4lt10  12949  3lt10  12950  2lt10  12951  1lt10  12952  5eluz3  13003  uzuzle23  13004  uzuzle24  13005  uzuzle34  13006  fz0to4untppr  13757  fz0to5un2tp  13758  fzo0to42pr  13881  faclbnd4lem1  14430  4bc2eq6  14466  sqrt9  15433  sqrt2gt1lt2  15434  absrdbnd  15502  sqrtpclii  15543  0.999...  16043  ef01bndlem  16345  sin01bnd  16346  cos01bnd  16347  cos2bnd  16349  rpnnen2lem3  16377  rpnnen2lem4  16378  rpnnen2lem9  16383  rpnnen2lem12  16386  flodddiv4  16578  strleun  17328  chnub  18789  elii1  25249  htpycc  25294  pcoval1  25327  pcocn  25331  pcohtpylem  25333  pcopt  25336  pcopt2  25337  pcoass  25338  pcorevlem  25340  vitalilem4  25925  vitali  25927  dveflem  26292  pige0  26781  sinhalfpilem  26785  sincosq1lem  26819  sincos4thpi  26835  sincos6thpi  26837  pige3  26840  cos0pilt1  26853  tanregt0  26860  efif1olem4  26866  relogrn  26882  logi  26908  argregt0  26931  argrege0  26932  logneg2  26936  2logb9irr  27116  asin1  27215  reasinsin  27217  log2cnv  27265  log2tlbnd  27266  log2ub  27270  harmonicbnd3  27328  ppiublem1  27522  ppiub  27524  bposlem3  27606  bposlem4  27607  bposlem5  27608  bposlem7  27610  bposlem8  27611  bposlem9  27612  lgsdir2lem1  27645  chebbnd1lem3  27791  dchrvmasumlema  27820  logdivsum  27853  mulog2sumlem2  27855  pntpbnd1a  27905  pntpbnd2  27907  pntlemk  27926  istrkg3ld  28916  axlowdimlem16  29528  axlowdimlem17  29529  axlowdim  29532  usgrexmplef  29833  upgr4cycl4dv4e  30779  konigsbergiedgw  30842  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  ex-fl  31041  ex-sqrt  31048  ex-gcd  31051  normlem6  31710  2sqr3minply  34405  cos9thpiminplylem1  34407  sqsscirc1  34533  prodfzo03  35225  hgt750lemd  35270  hgt750lem  35273  hgt750lem2  35274  hgt750leme  35280  tgoldbachgnn  35281  dnizeq0  37321  cnndvlem1  37383  bj-pinftyccb  38122  bj-pinftynminfty  38128  tan2h  38515  fdc  38659  asin1half  43388  areaquad  44202  sineq0ALT  45904  halffl  46281  itgsin0pilem1  46929  itgsinexplem1  46933  wallispilem2  47045  wallispilem4  47047  stirlingr  47069  fourierdlem62  47147  fourierdlem77  47162  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  etransclem23  47236  etransclem46  47259  smfmullem4  47773  ceilhalf1  48377  fmtnoprmfac2lem1  48620  fmtno4prmfac  48626  31prm  48651  mod42tp1mod8  48656  nprmdvdsfacm1lem4  48677  nprmdvdsfacm1  48678  ppivalnnnprmge6  48680  2exp340mod341  48800  341fppr2  48801  9fppr8  48804  nfermltl8rev  48809  nfermltl2rev  48810  sbgoldbo  48854  nnsum3primes4  48855  nnsum3primesgbe  48859  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  tgblthelfgott  48882  cycl3grtri  49014  usgrexmpl1lem  49088  usgrexmpl2lem  49093  gpgusgralem  49123  gpg5nbgrvtx13starlem2  49139  gpg5nbgr3star  49148  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  ackval42  49777  itsclc0yqsollem2  49844  sepfsepc  50005  veronesev1lem  50942  veronesev2lem  50943  veronesev3lem  50944  veronesev4lem  50945  veronesev5lem  50946  veronesev6lem  50947  veronesevrowd  50948  veronesematrowd  50950  veroquadgsumlem  50952  veroquadmodzerod  50953  veroquadnolindfd  50954