Theorem ltleii 11300

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

Syntax hints:   ∈ wcel 2141   class class class wbr 5097  ℝcr 11066   < clt 11210   ≤ cle 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-pre-lttri 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216

This theorem is referenced by:  0le1  11704  ledivp1i  12111  ltdivp1i  12112  0le2  12314  2le3  12386  1le2  12423  1le3  12426  halfge0  12431  decleh  12722  8lt10  12820  7lt10  12821  6lt10  12822  5lt10  12823  4lt10  12824  3lt10  12825  2lt10  12826  1lt10  12827  5eluz3  12878  uzuzle23  12879  uzuzle24  12880  uzuzle34  12881  fz0to4untppr  13629  fz0to5un2tp  13630  fzo0to42pr  13753  faclbnd4lem1  14300  4bc2eq6  14336  sqrt9  15291  sqrt2gt1lt2  15292  absrdbnd  15360  sqrtpclii  15401  0.999...  15902  ef01bndlem  16207  sin01bnd  16208  cos01bnd  16209  cos2bnd  16211  rpnnen2lem3  16239  rpnnen2lem4  16240  rpnnen2lem9  16245  rpnnen2lem12  16248  flodddiv4  16440  strleun  17184  chnub  18645  elii1  24985  htpycc  25030  pcoval1  25063  pcocn  25067  pcohtpylem  25069  pcopt  25072  pcopt2  25073  pcoass  25074  pcorevlem  25076  vitalilem4  25661  vitali  25663  dveflem  26029  pige0  26512  sinhalfpilem  26516  sincosq1lem  26550  sincos4thpi  26566  sincos6thpi  26569  pige3  26572  cos0pilt1  26585  tanregt0  26592  efif1olem4  26598  relogrn  26614  logi  26640  argregt0  26663  argrege0  26664  logneg2  26668  2logb9irr  26848  asin1  26947  reasinsin  26949  log2cnv  26997  log2tlbnd  26998  log2ub  27002  harmonicbnd3  27060  ppiublem1  27254  ppiub  27256  bposlem3  27338  bposlem4  27339  bposlem5  27340  bposlem7  27342  bposlem8  27343  bposlem9  27344  lgsdir2lem1  27377  chebbnd1lem3  27523  dchrvmasumlema  27552  logdivsum  27585  mulog2sumlem2  27587  pntpbnd1a  27637  pntpbnd2  27639  pntlemk  27658  istrkg3ld  28618  axlowdimlem16  29115  axlowdimlem17  29116  axlowdim  29119  usgrexmplef  29417  upgr4cycl4dv4e  30344  konigsbergiedgw  30407  konigsberglem1  30411  konigsberglem2  30412  konigsberglem3  30413  ex-fl  30606  ex-sqrt  30613  ex-gcd  30616  normlem6  31275  2sqr3minply  34038  cos9thpiminplylem1  34040  sqsscirc1  34166  prodfzo03  34858  hgt750lemd  34903  hgt750lem  34906  hgt750lem2  34907  hgt750leme  34913  tgoldbachgnn  34914  dnizeq0  36874  cnndvlem1  36936  bj-pinftyccb  37674  bj-pinftynminfty  37680  tan2h  38072  fdc  38205  asin1half  42927  areaquad  43754  sineq0ALT  45473  halffl  45836  itgsin0pilem1  46485  itgsinexplem1  46489  wallispilem2  46601  wallispilem4  46603  stirlingr  46625  fourierdlem62  46703  fourierdlem77  46718  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem111  46752  fourierdlem112  46753  fourierdlem114  46755  sqwvfoura  46763  sqwvfourb  46764  fourierswlem  46765  fouriersw  46766  etransclem23  46792  etransclem46  46815  smfmullem4  47329  ceilhalf1  47893  fmtnoprmfac2lem1  48136  fmtno4prmfac  48142  31prm  48167  mod42tp1mod8  48172  nprmdvdsfacm1lem4  48193  nprmdvdsfacm1  48194  ppivalnnnprmge6  48196  2exp340mod341  48316  341fppr2  48317  9fppr8  48320  nfermltl8rev  48325  nfermltl2rev  48326  sbgoldbo  48370  nnsum3primes4  48371  nnsum3primesgbe  48375  nnsum4primeseven  48383  nnsum4primesevenALTV  48384  wtgoldbnnsum4prm  48385  bgoldbnnsum3prm  48387  tgblthelfgott  48398  cycl3grtri  48530  usgrexmpl1lem  48604  usgrexmpl2lem  48609  gpgusgralem  48639  gpg5nbgrvtx13starlem2  48655  gpg5nbgr3star  48664  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  ackval42  49279  itsclc0yqsollem2  49346  sepfsepc  49510