Theorem ltleii 11260

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

Syntax hints:   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  0le1  11664  ledivp1i  12072  ltdivp1i  12073  1le2  12376  1le3  12379  halfge0  12384  decleh  12670  5eluz3  12824  uzuzle23  12825  uzuzle24  12826  uzuzle34  12827  fz0to4untppr  13575  fz0to5un2tp  13576  fzo0to42pr  13699  faclbnd4lem1  14246  4bc2eq6  14282  sqrt9  15226  sqrt2gt1lt2  15227  absrdbnd  15295  sqrtpclii  15336  0.999...  15837  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos2bnd  16146  rpnnen2lem3  16174  rpnnen2lem4  16175  rpnnen2lem9  16180  rpnnen2lem12  16183  flodddiv4  16375  strleun  17118  chnub  18579  elii1  24920  htpycc  24965  pcoval1  24998  pcocn  25002  pcohtpylem  25004  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevlem  25011  vitalilem4  25596  vitali  25598  dveflem  25964  sinhalfpilem  26445  sincosq1lem  26479  sincos4thpi  26495  sincos6thpi  26498  pige3  26501  cos0pilt1  26514  tanregt0  26521  efif1olem4  26527  relogrn  26543  logi  26569  argregt0  26592  argrege0  26593  logneg2  26597  2logb9irr  26777  asin1  26876  reasinsin  26878  log2cnv  26926  log2tlbnd  26927  log2ub  26931  harmonicbnd3  26989  ppiublem1  27183  ppiub  27185  bposlem3  27267  bposlem4  27268  bposlem5  27269  bposlem7  27271  bposlem8  27272  bposlem9  27273  lgsdir2lem1  27306  chebbnd1lem3  27452  dchrvmasumlema  27481  logdivsum  27514  mulog2sumlem2  27516  pntpbnd1a  27566  pntpbnd2  27568  pntlemk  27587  istrkg3ld  28547  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  usgrexmplef  29346  upgr4cycl4dv4e  30273  konigsbergiedgw  30336  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  ex-fl  30535  ex-sqrt  30542  ex-gcd  30545  normlem6  31204  2sqr3minply  33964  cos9thpiminplylem1  33966  sqsscirc1  34092  prodfzo03  34787  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  tgoldbachgnn  34843  dnizeq0  36781  cnndvlem1  36843  bj-pinftyccb  37581  bj-pinftynminfty  37587  tan2h  37979  fdc  38112  asin1half  42834  jm2.20nn  43442  areaquad  43661  sineq0ALT  45380  halffl  45744  itgsin0pilem1  46393  itgsinexplem1  46397  wallispilem2  46509  wallispilem4  46511  stirlinglem15  46531  stirlingr  46533  fourierdlem62  46611  fourierdlem77  46626  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem114  46663  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  etransclem23  46700  etransclem46  46723  smfmullem4  47237  ceilhalf1  47801  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  31prm  48075  mod42tp1mod8  48080  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  2exp340mod341  48224  341fppr2  48225  9fppr8  48228  nfermltl8rev  48233  nfermltl2rev  48234  sbgoldbo  48278  nnsum3primes4  48279  nnsum3primesgbe  48283  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  tgblthelfgott  48306  cycl3grtri  48438  usgrexmpl1lem  48512  usgrexmpl2lem  48517  gpgusgralem  48547  gpg5nbgrvtx13starlem2  48563  gpg5nbgr3star  48572  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  ackval42  49187  itsclc0yqsollem2  49254  sepfsepc  49418