Theorem ltleii 11341

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

Syntax hints:   ∈ wcel 2106   class class class wbr 5148  ℝcr 11111   < clt 11252   ≤ cle 11253

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-pre-lttri 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258

This theorem is referenced by:  0le1  11741  ledivp1i  12143  ltdivp1i  12144  1le2  12425  1le3  12428  halfge0  12433  decleh  12716  eluz4eluz2  12873  uzuzle23  12877  fz0to4untppr  13608  fzo0to42pr  13723  faclbnd4lem1  14257  4bc2eq6  14293  sqrt9  15224  sqrt2gt1lt2  15225  absrdbnd  15292  sqrtpclii  15333  0.999...  15831  ef01bndlem  16131  sin01bnd  16132  cos01bnd  16133  cos2bnd  16135  rpnnen2lem3  16163  rpnnen2lem4  16164  rpnnen2lem9  16169  rpnnen2lem12  16172  flodddiv4  16360  strleun  17094  cnfldfunALTOLD  21158  elii1  24675  htpycc  24720  pcoval1  24753  pcocn  24757  pcohtpylem  24759  pcopt  24762  pcopt2  24763  pcoass  24764  pcorevlem  24766  vitalilem4  25352  vitali  25354  dveflem  25720  sinhalfpilem  26197  sincosq1lem  26231  sincos4thpi  26247  sincos6thpi  26249  pige3  26252  cos0pilt1  26265  tanregt0  26272  efif1olem4  26278  relogrn  26294  argregt0  26342  argrege0  26343  logneg2  26347  2logb9irr  26524  asin1  26623  reasinsin  26625  log2cnv  26673  log2tlbnd  26674  log2ub  26678  harmonicbnd3  26736  ppiublem1  26929  ppiub  26931  bposlem3  27013  bposlem4  27014  bposlem5  27015  bposlem7  27017  bposlem8  27018  bposlem9  27019  lgsdir2lem1  27052  chebbnd1lem3  27198  dchrvmasumlema  27227  logdivsum  27260  mulog2sumlem2  27262  pntpbnd1a  27312  pntpbnd2  27314  pntlemk  27333  istrkg3ld  27967  axlowdimlem16  28470  axlowdimlem17  28471  axlowdim  28474  usgrexmplef  28771  upgr4cycl4dv4e  29693  konigsbergiedgw  29756  konigsberglem1  29760  konigsberglem2  29761  konigsberglem3  29762  ex-fl  29955  ex-sqrt  29962  ex-gcd  29965  normlem6  30623  sqsscirc1  33174  prodfzo03  33901  hgt750lemd  33946  hgt750lem  33949  hgt750lem2  33950  hgt750leme  33956  tgoldbachgnn  33957  logi  34996  dnizeq0  35654  cnndvlem1  35716  bj-pinftyccb  36405  bj-pinftynminfty  36411  tan2h  36783  fdc  36916  jm2.20nn  42038  areaquad  42267  sineq0ALT  44000  halffl  44305  itgsin0pilem1  44965  itgsinexplem1  44969  wallispilem2  45081  wallispilem4  45083  stirlinglem15  45103  stirlingr  45105  fourierdlem62  45183  fourierdlem77  45198  fourierdlem102  45223  fourierdlem103  45224  fourierdlem104  45225  fourierdlem111  45232  fourierdlem112  45233  fourierdlem114  45235  sqwvfoura  45243  sqwvfourb  45244  fourierswlem  45245  fouriersw  45246  etransclem23  45272  etransclem46  45295  smfmullem4  45809  fmtnoprmfac2lem1  46533  fmtno4prmfac  46539  31prm  46564  mod42tp1mod8  46569  2exp340mod341  46700  341fppr2  46701  9fppr8  46704  nfermltl8rev  46709  nfermltl2rev  46710  sbgoldbo  46754  nnsum3primes4  46755  nnsum3primesgbe  46759  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  wtgoldbnnsum4prm  46769  bgoldbnnsum3prm  46771  tgblthelfgott  46782  ackval42  47470  itsclc0yqsollem2  47537  sepfsepc  47648