Theorem ltle 9748

Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
ltle	|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		orc 391	. 2 |- ( A < B -> ( A < B \/ A = B ) )
2		leloe 9746	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
3	1, 2	syl5ibr 229	1 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Syntax hints:   -> wi 4   \/ wo 374   /\ wa 375   = wceq 1455   e. wcel 1898   class class class wbr 4416   RRcr 9564   < clt 9701   <_ cle 9702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-pre-lttri 9639

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707

This theorem is referenced by:  ltleletr  9752  letr  9753  letric  9760  ltlen  9761  ltlei  9782  ltled  9809  lt2add  10127  lep1  10472  lem1  10474  letrp1  10475  ltmul12a  10489  mulge0b  10503  lediv12a  10527  bndndx  10897  uzind  11056  fnn0ind  11063  eluz2b2  11260  zmin  11289  rpnnen1lem1  11319  rpnnen1lem2  11320  rpnnen1lem3  11321  rpnnen1lem5  11323  rpge0  11343  rpneg  11361  iccsplit  11794  difelfznle  11935  fvffz0  11938  elfzouz2  11965  elfzo0le  11990  fzosplitprm1  12049  fzostep1  12052  fllep1  12069  fracle1  12071  expgt1  12342  expnbnd  12433  expnlbnd2  12435  faclbnd  12507  swrdsbslen  12841  swrdspsleq  12842  swrdccat3  12885  repswswrd  12924  resqrex  13363  sqrtgt0  13371  absmax  13441  eqsqrt2d  13480  rlim2lt  13610  mulcn2  13708  rlimo1  13729  o1rlimmul  13731  climbdd  13784  caucvgrlem  13785  caucvgrlemOLD  13786  supcvg  13963  efcllem  14181  sin01bnd  14288  cos01bnd  14289  sin01gt0  14293  cos01gt0  14294  absef  14300  efieq1re  14302  ruclem11  14341  pythagtriplem12  14825  pythagtriplem13  14826  pythagtriplem14  14827  pythagtriplem16  14829  pclem  14837  prmgaplem4  15073  cshwshashlem2  15116  isabvd  18097  met2ndci  21586  blcvx  21865  iocopnst  22017  nmoleub2a  22180  nmoleub2b  22181  nmhmcn  22183  iscmet3lem2  22311  caubl  22326  ivthlem2  22452  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ioombl1lem4  22563  ioovolcl  22571  volsup2  22612  itg2monolem1  22757  itg2gt0  22767  itg2cnlem1  22768  dvne0  23012  ftc1lem4  23040  dgrlt  23269  aalioulem5  23341  ulmbdd  23402  iblulm  23411  radcnvlem1  23417  abelthlem5  23439  abelthlem7  23442  sincosq1lem  23501  tangtx  23509  tanabsge  23510  sinq12ge0  23512  sineq0  23525  tanord  23536  logcj  23604  argregt0  23608  argrege0  23609  argimgt0  23610  logdmnrp  23635  logcnlem3  23638  logf1o2  23644  cxpsqrtlem  23696  abscxpbnd  23742  logreclem  23748  asinneg  23861  atanlogsublem  23890  atanlogsub  23891  rlimcnp  23940  xrlimcnp  23943  basellem8  24063  chtub  24189  bposlem9  24269  chebbnd1  24359  chtppilimlem1  24360  dchrvmasumiflem1  24388  mulog2sumlem2  24422  pntrmax  24451  pntibndlem2  24478  pntibndlem3  24479  pntlemf  24492  axlowdimlem16  25036  nmblolbii  26489  ubthlem1  26561  bcsiALT  26881  nmbdoplbi  27726  nmcexi  27728  nmcoplbi  27730  lnconi  27735  nmbdfnlbi  27751  nmcfnlbi  27754  nmopcoi  27797  branmfn  27807  leopmul  27836  nmopleid  27841  esumcvg  28956  ballotlemfrceq  29410  ballotlemfrceqOLD  29448  sinccvglem  30365  opnrebl2  31026  ivthALT  31040  poimirlem15  32000  poimirlem31  32016  ftc1cnnclem  32060  ftc1anclem5  32066  incsequz2  32123  nnubfi  32124  bfplem2  32200  pell14qrgap  35766  pellfundre  35774  pellfundlb  35777  stoweidlem17  37915  stoweidlem34  37933  wallispilem1  37965  leltletr  38752  bgoldbtbnd  38942  bgoldbachlt  38944  tgblthelfgott  38946  pfxccat3  39007  ltsubnn0  39093  2elfz2melfz  39100  elfzelfzlble  39103  subsubelfzo0  39104  pthdlem1  39792  m1modmmod  40597  nn0o  40602  nnolog2flm1  40674