Theorem ltleii 11269

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

Syntax hints:   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-pre-lttri 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185

This theorem is referenced by:  0le1  11673  ledivp1i  12081  ltdivp1i  12082  1le2  12385  1le3  12388  halfge0  12393  decleh  12679  5eluz3  12833  uzuzle23  12834  uzuzle24  12835  uzuzle34  12836  fz0to4untppr  13584  fz0to5un2tp  13585  fzo0to42pr  13708  faclbnd4lem1  14255  4bc2eq6  14291  sqrt9  15235  sqrt2gt1lt2  15236  absrdbnd  15304  sqrtpclii  15345  0.999...  15846  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos2bnd  16155  rpnnen2lem3  16183  rpnnen2lem4  16184  rpnnen2lem9  16189  rpnnen2lem12  16192  flodddiv4  16384  strleun  17127  chnub  18588  elii1  24902  htpycc  24947  pcoval1  24980  pcocn  24984  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  vitalilem4  25578  vitali  25580  dveflem  25946  sinhalfpilem  26427  sincosq1lem  26461  sincos4thpi  26477  sincos6thpi  26480  pige3  26483  cos0pilt1  26496  tanregt0  26503  efif1olem4  26509  relogrn  26525  logi  26551  argregt0  26574  argrege0  26575  logneg2  26579  2logb9irr  26759  asin1  26858  reasinsin  26860  log2cnv  26908  log2tlbnd  26909  log2ub  26913  harmonicbnd3  26971  ppiublem1  27165  ppiub  27167  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  chebbnd1lem3  27434  dchrvmasumlema  27463  logdivsum  27496  mulog2sumlem2  27498  pntpbnd1a  27548  pntpbnd2  27550  pntlemk  27569  istrkg3ld  28529  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  usgrexmplef  29328  upgr4cycl4dv4e  30255  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  ex-fl  30517  ex-sqrt  30524  ex-gcd  30527  normlem6  31186  2sqr3minply  33924  cos9thpiminplylem1  33926  sqsscirc1  34052  prodfzo03  34747  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  tgoldbachgnn  34803  dnizeq0  36735  cnndvlem1  36797  bj-pinftyccb  37535  bj-pinftynminfty  37541  tan2h  37933  fdc  38066  asin1half  42789  jm2.20nn  43425  areaquad  43644  sineq0ALT  45363  halffl  45729  itgsin0pilem1  46378  itgsinexplem1  46382  wallispilem2  46494  wallispilem4  46496  stirlinglem15  46516  stirlingr  46518  fourierdlem62  46596  fourierdlem77  46611  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem23  46685  etransclem46  46708  smfmullem4  47222  ceilhalf1  47786  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  31prm  48060  mod42tp1mod8  48065  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  ppivalnnnprmge6  48089  2exp340mod341  48209  341fppr2  48210  9fppr8  48213  nfermltl8rev  48218  nfermltl2rev  48219  sbgoldbo  48263  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  tgblthelfgott  48291  cycl3grtri  48423  usgrexmpl1lem  48497  usgrexmpl2lem  48502  gpgusgralem  48532  gpg5nbgrvtx13starlem2  48548  gpg5nbgr3star  48557  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  ackval42  49172  itsclc0yqsollem2  49239  sepfsepc  49403