Theorem ltle 9721

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 386	. 2 |- ( A < B -> ( A < B \/ A = B ) )
2		leloe 9719	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
3	1, 2	syl5ibr 224	1 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )

Syntax hints:   -> wi 4   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1870   class class class wbr 4426   RRcr 9537   < clt 9674   <_ cle 9675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-pre-lttri 9612

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680

This theorem is referenced by:  ltleletr  9725  letr  9726  letric  9733  ltlen  9734  ltlei  9755  ltled  9782  lt2add  10098  lep1  10443  lem1  10445  letrp1  10446  ltmul12a  10460  mulge0b  10474  lediv12a  10499  bndndx  10868  uzind  11027  fnn0ind  11034  eluz2b2  11231  zmin  11260  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  rpge0  11314  rpneg  11332  iccsplit  11763  difelfznle  11903  elfzouz2  11932  elfzo0le  11957  fzosplitprm1  12015  fzostep1  12018  fllep1  12034  fracle1  12036  expgt1  12307  expnbnd  12398  expnlbnd2  12400  faclbnd  12472  swrdsbslen  12789  swrdspsleq  12790  swrdccat3  12833  repswswrd  12872  resqrex  13293  sqrtgt0  13301  absmax  13371  eqsqrt2d  13410  rlim2lt  13539  mulcn2  13637  rlimo1  13658  o1rlimmul  13660  climbdd  13713  caucvgrlem  13714  caucvgrlemOLD  13715  supcvg  13892  efcllem  14110  sin01bnd  14217  cos01bnd  14218  sin01gt0  14222  cos01gt0  14223  absef  14229  efieq1re  14231  ruclem11  14270  pythagtriplem12  14739  pythagtriplem13  14740  pythagtriplem14  14741  pythagtriplem16  14743  pclem  14751  prmgaplem4  14987  cshwshashlem2  15030  isabvd  17983  met2ndci  21468  blcvx  21727  iocopnst  21864  nmoleub2a  22024  nmoleub2b  22025  nmhmcn  22027  iscmet3lem2  22155  caubl  22170  ivthlem2  22284  ovolicc2lem4  22351  ioombl1lem4  22391  ioovolcl  22399  volsup2  22440  itg2monolem1  22585  itg2gt0  22595  itg2cnlem1  22596  dvne0  22840  ftc1lem4  22868  dgrlt  23088  aalioulem5  23157  ulmbdd  23218  iblulm  23227  radcnvlem1  23233  abelthlem5  23255  abelthlem7  23258  sincosq1lem  23317  tangtx  23325  tanabsge  23326  sinq12ge0  23328  sineq0  23341  tanord  23352  logcj  23420  argregt0  23424  argrege0  23425  argimgt0  23426  logdmnrp  23451  logcnlem3  23454  logf1o2  23460  cxpsqrtlem  23512  abscxpbnd  23558  logreclem  23564  asinneg  23677  atanlogsublem  23706  atanlogsub  23707  rlimcnp  23756  xrlimcnp  23759  basellem8  23877  chtub  24003  bposlem9  24083  chebbnd1  24173  chtppilimlem1  24174  dchrvmasumiflem1  24202  mulog2sumlem2  24236  pntrmax  24265  pntibndlem2  24292  pntibndlem3  24293  pntlemf  24306  axlowdimlem16  24833  nmblolbii  26285  ubthlem1  26357  bcsiALT  26667  nmbdoplbi  27512  nmcexi  27514  nmcoplbi  27516  lnconi  27521  nmbdfnlbi  27537  nmcfnlbi  27540  nmopcoi  27583  branmfn  27593  leopmul  27622  nmopleid  27627  esumcvg  28746  ballotlemfrceq  29187  sinccvglem  30104  opnrebl2  30762  ivthALT  30776  poimirlem15  31658  poimirlem31  31674  ftc1cnnclem  31718  ftc1anclem5  31724  incsequz2  31781  nnubfi  31782  bfplem2  31858  pell14qrgap  35428  pellfundre  35434  pellfundlb  35437  stoweidlem17  37445  stoweidlem34  37463  wallispilem1  37495  leltletr  38103  bgoldbtbnd  38293  bgoldbachlt  38295  tgblthelfgott  38297  pfxccat3  38356  ltsubnn0  38399  2elfz2melfz  38406  elfzelfzlble  38409  subsubelfzo0  38410  m1modmmod  39084  nn0o  39089  nnolog2flm1  39161