Theorem ltleii 11304

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

Syntax hints:   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  0le1  11708  ledivp1i  12115  ltdivp1i  12116  1le2  12397  1le3  12400  halfge0  12405  decleh  12691  5eluz3  12849  uzuzle23  12850  uzuzle24  12851  uzuzle34  12852  fz0to4untppr  13598  fz0to5un2tp  13599  fzo0to42pr  13721  faclbnd4lem1  14265  4bc2eq6  14301  sqrt9  15246  sqrt2gt1lt2  15247  absrdbnd  15315  sqrtpclii  15356  0.999...  15854  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  cos2bnd  16163  rpnnen2lem3  16191  rpnnen2lem4  16192  rpnnen2lem9  16197  rpnnen2lem12  16200  flodddiv4  16392  strleun  17134  elii1  24838  htpycc  24886  pcoval1  24920  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  vitalilem4  25519  vitali  25521  dveflem  25890  sinhalfpilem  26379  sincosq1lem  26413  sincos4thpi  26429  sincos6thpi  26432  pige3  26435  cos0pilt1  26448  tanregt0  26455  efif1olem4  26461  relogrn  26477  logi  26503  argregt0  26526  argrege0  26527  logneg2  26531  2logb9irr  26712  asin1  26811  reasinsin  26813  log2cnv  26861  log2tlbnd  26862  log2ub  26866  harmonicbnd3  26925  ppiublem1  27120  ppiub  27122  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  chebbnd1lem3  27389  dchrvmasumlema  27418  logdivsum  27451  mulog2sumlem2  27453  pntpbnd1a  27503  pntpbnd2  27505  pntlemk  27524  istrkg3ld  28395  axlowdimlem16  28891  axlowdimlem17  28892  axlowdim  28895  usgrexmplef  29193  upgr4cycl4dv4e  30121  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  ex-fl  30383  ex-sqrt  30390  ex-gcd  30393  normlem6  31051  chnub  32945  2sqr3minply  33777  cos9thpiminplylem1  33779  sqsscirc1  33905  prodfzo03  34601  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  tgoldbachgnn  34657  dnizeq0  36470  cnndvlem1  36532  bj-pinftyccb  37216  bj-pinftynminfty  37222  tan2h  37613  fdc  37746  asin1half  42352  jm2.20nn  42993  areaquad  43212  sineq0ALT  44933  halffl  45301  itgsin0pilem1  45955  itgsinexplem1  45959  wallispilem2  46071  wallispilem4  46073  stirlinglem15  46093  stirlingr  46095  fourierdlem62  46173  fourierdlem77  46188  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem23  46262  etransclem46  46285  smfmullem4  46799  ceilhalf1  47339  fmtnoprmfac2lem1  47571  fmtno4prmfac  47577  31prm  47602  mod42tp1mod8  47607  2exp340mod341  47738  341fppr2  47739  9fppr8  47742  nfermltl8rev  47747  nfermltl2rev  47748  sbgoldbo  47792  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  tgblthelfgott  47820  cycl3grtri  47950  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgusgralem  48051  gpg5nbgrvtx13starlem2  48067  gpg5nbgr3star  48076  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  ackval42  48689  itsclc0yqsollem2  48756  sepfsepc  48920