Theorem ltleii 11433

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

This proof depends on syntax axioms:   ∈ wcel 2145   class class class wbr 5103  ℝcr 11199   < clt 11343   ≤ cle 11344

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 7751  ax-resscn 11257  ax-pre-lttri 11274

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 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349

This theorem is used by:  0le1  11839  ledivp1i  12242  ltdivp1i  12243  0le2  12445  2le3  12517  1le2  12554  1le3  12557  halfge0  12562  decleh  12854  8lt10  12952  7lt10  12953  6lt10  12954  5lt10  12955  4lt10  12956  3lt10  12957  2lt10  12958  1lt10  12959  5eluz3  13010  uzuzle23  13011  uzuzle24  13012  uzuzle34  13013  fz0to4untppr  13764  fz0to5un2tp  13765  fzo0to42pr  13888  faclbnd4lem1  14437  4bc2eq6  14473  sqrt9  15440  sqrt2gt1lt2  15441  absrdbnd  15509  sqrtpclii  15550  0.999...  16050  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos2bnd  16356  rpnnen2lem3  16384  rpnnen2lem4  16385  rpnnen2lem9  16390  rpnnen2lem12  16393  flodddiv4  16585  strleun  17335  chnub  18796  elii1  25256  htpycc  25301  pcoval1  25334  pcocn  25338  pcohtpylem  25340  pcopt  25343  pcopt2  25344  pcoass  25345  pcorevlem  25347  vitalilem4  25932  vitali  25934  dveflem  26299  pige0  26788  sinhalfpilem  26792  sincosq1lem  26826  sincos4thpi  26842  sincos6thpi  26844  pige3  26847  cos0pilt1  26860  tanregt0  26867  efif1olem4  26873  relogrn  26889  logi  26915  argregt0  26938  argrege0  26939  logneg2  26943  2logb9irr  27123  asin1  27222  reasinsin  27224  log2cnv  27272  log2tlbnd  27273  log2ub  27277  harmonicbnd3  27335  ppiublem1  27529  ppiub  27531  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem7  27617  bposlem8  27618  bposlem9  27619  lgsdir2lem1  27652  chebbnd1lem3  27798  dchrvmasumlema  27827  logdivsum  27860  mulog2sumlem2  27862  pntpbnd1a  27912  pntpbnd2  27914  pntlemk  27933  istrkg3ld  28923  axlowdimlem16  29535  axlowdimlem17  29536  axlowdim  29539  usgrexmplef  29840  upgr4cycl4dv4e  30786  konigsbergiedgw  30849  konigsberglem1  30853  konigsberglem2  30854  konigsberglem3  30855  ex-fl  31048  ex-sqrt  31055  ex-gcd  31058  normlem6  31717  2sqr3minply  34412  cos9thpiminplylem1  34414  sqsscirc1  34540  prodfzo03  35232  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  tgoldbachgnn  35288  dnizeq0  37341  cnndvlem1  37403  bj-pinftyccb  38142  bj-pinftynminfty  38148  tan2h  38535  fdc  38679  asin1half  43408  areaquad  44217  sineq0ALT  45918  halffl  46311  itgsin0pilem1  46959  itgsinexplem1  46963  wallispilem2  47075  wallispilem4  47077  stirlingr  47099  fourierdlem62  47177  fourierdlem77  47192  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fourierdlem112  47227  fourierdlem114  47229  sqwvfoura  47237  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  etransclem23  47266  etransclem46  47289  smfmullem4  47803  ceilhalf1  48407  fmtnoprmfac2lem1  48650  fmtno4prmfac  48656  31prm  48681  mod42tp1mod8  48686  nprmdvdsfacm1lem4  48707  nprmdvdsfacm1  48708  ppivalnnnprmge6  48710  2exp340mod341  48830  341fppr2  48831  9fppr8  48834  nfermltl8rev  48839  nfermltl2rev  48840  sbgoldbo  48884  nnsum3primes4  48885  nnsum3primesgbe  48889  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  tgblthelfgott  48912  cycl3grtri  49044  usgrexmpl1lem  49118  usgrexmpl2lem  49123  gpgusgralem  49153  gpg5nbgrvtx13starlem2  49169  gpg5nbgr3star  49178  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  ackval42  49807  itsclc0yqsollem2  49874  sepfsepc  50035  veronesev1lem  50972  veronesev2lem  50973  veronesev3lem  50974  veronesev4lem  50975  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veronesematrowd  50980  veroquadgsumlem  50982  veroquadmodzerod  50983  veroquadnolindfd  50984