Theorem ltleii 11437

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

This proof depends on syntax axioms:   ∈ wcel 2144   class class class wbr 5102  ℝcr 11203   < clt 11347   ≤ cle 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-pre-lttri 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353

This theorem is used by:  0le1  11843  ledivp1i  12246  ltdivp1i  12247  0le2  12449  2le3  12521  1le2  12558  1le3  12561  halfge0  12566  decleh  12858  8lt10  12956  7lt10  12957  6lt10  12958  5lt10  12959  4lt10  12960  3lt10  12961  2lt10  12962  1lt10  12963  5eluz3  13014  uzuzle23  13015  uzuzle24  13016  uzuzle34  13017  fz0to4untppr  13768  fz0to5un2tp  13769  fzo0to42pr  13892  faclbnd4lem1  14441  4bc2eq6  14477  sqrt9  15446  sqrt2gt1lt2  15447  absrdbnd  15515  sqrtpclii  15556  0.999...  16056  ef01bndlem  16358  sin01bnd  16359  cos01bnd  16360  cos2bnd  16362  rpnnen2lem3  16390  rpnnen2lem4  16391  rpnnen2lem9  16396  rpnnen2lem12  16399  flodddiv4  16591  strleun  17341  chnub  18802  elii1  25262  htpycc  25307  pcoval1  25340  pcocn  25344  pcohtpylem  25346  pcopt  25349  pcopt2  25350  pcoass  25351  pcorevlem  25353  vitalilem4  25938  vitali  25940  dveflem  26305  pige0  26794  sinhalfpilem  26798  sincosq1lem  26832  sincos4thpi  26848  sincos6thpi  26850  pige3  26853  tanregt0  26873  efif1olem4  26879  relogrn  26895  logi  26921  argregt0  26944  argrege0  26945  logneg2  26949  2logb9irr  27129  asin1  27228  reasinsin  27230  log2cnv  27278  log2tlbnd  27279  log2ub  27283  harmonicbnd3  27341  ppiublem1  27535  ppiub  27537  bposlem3  27619  bposlem4  27620  bposlem5  27621  bposlem7  27623  bposlem8  27624  bposlem9  27625  lgsdir2lem1  27658  chebbnd1lem3  27804  dchrvmasumlema  27833  logdivsum  27866  mulog2sumlem2  27868  pntpbnd1a  27918  pntpbnd2  27920  pntlemk  27939  axlowdimlem16  29541  axlowdimlem17  29542  axlowdim  29545  usgrexmplef  29846  upgr4cycl4dv4e  30792  konigsbergiedgw  30855  konigsberglem3  30861  ex-fl  31054  ex-sqrt  31061  ex-gcd  31064  normlem6  31723  2sqr3minply  34459  cos9thpiminplylem1  34461  sqsscirc1  34587  prodfzo03  35279  hgt750lemd  35324  hgt750lem  35327  hgt750lem2  35328  hgt750leme  35334  tgoldbachgnn  35335  dnizeq0  37434  cnndvlem1  37496  bj-pinftyccb  38236  bj-pinftynminfty  38242  tan2h  38629  fdc  38773  asin1half  43502  areaquad  44312  sineq0ALT  46013  halffl  46406  itgsin0pilem1  47054  itgsinexplem1  47058  wallispilem2  47170  wallispilem4  47172  stirlingr  47194  fourierdlem62  47272  fourierdlem77  47287  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fourierdlem112  47322  fourierdlem114  47324  sqwvfoura  47332  sqwvfourb  47333  fourierswlem  47334  fouriersw  47335  etransclem23  47361  etransclem46  47384  smfmullem4  47898  ceilhalf1  48502  fmtnoprmfac2lem1  48745  fmtno4prmfac  48751  31prm  48776  mod42tp1mod8  48781  nprmdvdsfacm1lem4  48802  nprmdvdsfacm1  48803  ppivalnnnprmge6  48805  2exp340mod341  48925  341fppr2  48926  9fppr8  48929  nfermltl8rev  48934  nfermltl2rev  48935  sbgoldbo  48979  nnsum3primes4  48980  nnsum3primesgbe  48984  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  wtgoldbnnsum4prm  48994  bgoldbnnsum3prm  48996  tgblthelfgott  49007  cycl3grtri  49139  usgrexmpl1lem  49213  usgrexmpl2lem  49218  gpgusgralem  49248  gpg5nbgrvtx13starlem2  49264  gpg5nbgr3star  49273  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  ackval42  49902  itsclc0yqsollem2  49969  sepfsepc  50136  veronesev1lem  51142  veronesev2lem  51143  veronesev3lem  51144  veronesev4lem  51145  veronesev5lem  51146  veronesev6lem  51147  veronesevrowd  51148  veronesematrowd  51150  veroquadgsumlem  51152  veroquadmodzerod  51153  veroquadnolindfd  51154