Theorem ltleii 11335

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

Syntax hints:   ∈ wcel 2098   class class class wbr 5139  ℝcr 11106   < clt 11246   ≤ cle 11247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-pre-lttri 11181

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252

This theorem is referenced by:  0le1  11735  ledivp1i  12137  ltdivp1i  12138  1le2  12419  1le3  12422  halfge0  12427  decleh  12710  eluz4eluz2  12867  uzuzle23  12871  fz0to4untppr  13602  fzo0to42pr  13717  faclbnd4lem1  14251  4bc2eq6  14287  sqrt9  15218  sqrt2gt1lt2  15219  absrdbnd  15286  sqrtpclii  15327  0.999...  15825  ef01bndlem  16126  sin01bnd  16127  cos01bnd  16128  cos2bnd  16130  rpnnen2lem3  16158  rpnnen2lem4  16159  rpnnen2lem9  16164  rpnnen2lem12  16167  flodddiv4  16355  strleun  17091  cnfldfunALTOLD  21244  elii1  24782  htpycc  24830  pcoval1  24864  pcocn  24868  pcohtpylem  24870  pcopt  24873  pcopt2  24874  pcoass  24875  pcorevlem  24877  vitalilem4  25464  vitali  25466  dveflem  25835  sinhalfpilem  26317  sincosq1lem  26351  sincos4thpi  26367  sincos6thpi  26369  pige3  26372  cos0pilt1  26385  tanregt0  26392  efif1olem4  26398  relogrn  26414  logi  26440  argregt0  26463  argrege0  26464  logneg2  26468  2logb9irr  26646  asin1  26745  reasinsin  26747  log2cnv  26795  log2tlbnd  26796  log2ub  26800  harmonicbnd3  26859  ppiublem1  27054  ppiub  27056  bposlem3  27138  bposlem4  27139  bposlem5  27140  bposlem7  27142  bposlem8  27143  bposlem9  27144  lgsdir2lem1  27177  chebbnd1lem3  27323  dchrvmasumlema  27352  logdivsum  27385  mulog2sumlem2  27387  pntpbnd1a  27437  pntpbnd2  27439  pntlemk  27458  istrkg3ld  28184  axlowdimlem16  28687  axlowdimlem17  28688  axlowdim  28691  usgrexmplef  28988  upgr4cycl4dv4e  29910  konigsbergiedgw  29973  konigsberglem1  29977  konigsberglem2  29978  konigsberglem3  29979  ex-fl  30172  ex-sqrt  30179  ex-gcd  30182  normlem6  30840  sqsscirc1  33380  prodfzo03  34106  hgt750lemd  34151  hgt750lem  34154  hgt750lem2  34155  hgt750leme  34161  tgoldbachgnn  34162  dnizeq0  35842  cnndvlem1  35904  bj-pinftyccb  36593  bj-pinftynminfty  36599  tan2h  36974  fdc  37107  jm2.20nn  42250  areaquad  42479  sineq0ALT  44212  halffl  44516  itgsin0pilem1  45176  itgsinexplem1  45180  wallispilem2  45292  wallispilem4  45294  stirlinglem15  45314  stirlingr  45316  fourierdlem62  45394  fourierdlem77  45409  fourierdlem102  45434  fourierdlem103  45435  fourierdlem104  45436  fourierdlem111  45443  fourierdlem112  45444  fourierdlem114  45446  sqwvfoura  45454  sqwvfourb  45455  fourierswlem  45456  fouriersw  45457  etransclem23  45483  etransclem46  45506  smfmullem4  46020  fmtnoprmfac2lem1  46744  fmtno4prmfac  46750  31prm  46775  mod42tp1mod8  46780  2exp340mod341  46911  341fppr2  46912  9fppr8  46915  nfermltl8rev  46920  nfermltl2rev  46921  sbgoldbo  46965  nnsum3primes4  46966  nnsum3primesgbe  46970  nnsum4primeseven  46978  nnsum4primesevenALTV  46979  wtgoldbnnsum4prm  46980  bgoldbnnsum3prm  46982  tgblthelfgott  46993  ackval42  47595  itsclc0yqsollem2  47662  sepfsepc  47772