Theorem ltle 9676

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

Syntax hints:   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1383   e. wcel 1804   class class class wbr 4437   RRcr 9494   < clt 9631   <_ cle 9632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-pre-lttri 9569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637

This theorem is referenced by:  ltleletr  9680  letr  9681  letric  9688  ltlen  9689  ltlei  9709  ltled  9736  lt2add  10044  lep1  10388  lem1  10390  letrp1  10391  ltmul12a  10405  mulge0b  10419  lediv12a  10445  bndndx  10801  uzind  10961  fnn0ind  10970  eluz2b2  11165  zmin  11189  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem5  11223  rpge0  11243  rpneg  11260  iccsplit  11664  difelfznle  11800  elfzouz2  11824  elfzo0le  11848  fzosplitprm1  11901  fzostep1  11904  fllep1  11920  fracle1  11922  expgt1  12186  expnbnd  12277  expnlbnd2  12279  faclbnd  12350  swrdccat3  12699  repswswrd  12738  resqrex  13066  sqrtgt0  13074  absmax  13144  eqsqrt2d  13183  rlim2lt  13302  mulcn2  13400  rlimo1  13421  o1rlimmul  13423  climbdd  13476  caucvgrlem  13477  supcvg  13649  efcllem  13795  sin01bnd  13902  cos01bnd  13903  sin01gt0  13907  cos01gt0  13908  absef  13914  efieq1re  13916  ruclem11  13955  pythagtriplem12  14332  pythagtriplem13  14333  pythagtriplem14  14334  pythagtriplem16  14336  pclem  14344  cshwshashlem2  14563  isabvd  17448  met2ndci  21003  blcvx  21281  iocopnst  21418  nmoleub2a  21578  nmoleub2b  21579  nmhmcn  21581  iscmet3lem2  21709  caubl  21724  ivthlem2  21842  ovolicc2lem4  21909  ioombl1lem4  21949  ioovolcl  21957  volsup2  21992  itg2monolem1  22135  itg2gt0  22145  itg2cnlem1  22146  dvne0  22390  ftc1lem4  22418  dgrlt  22641  aalioulem5  22710  ulmbdd  22771  iblulm  22780  radcnvlem1  22786  abelthlem5  22808  abelthlem7  22811  sincosq1lem  22868  tangtx  22876  tanabsge  22877  sinq12ge0  22879  sineq0  22892  tanord  22903  logcj  22969  argregt0  22973  argrege0  22974  argimgt0  22975  logdmnrp  23000  logcnlem3  23003  logf1o2  23009  cxpsqrtlem  23061  abscxpbnd  23105  logreclem  23128  asinneg  23195  atanlogsublem  23224  atanlogsub  23225  rlimcnp  23273  xrlimcnp  23276  basellem8  23339  chtub  23465  bposlem9  23545  chebbnd1  23635  chtppilimlem1  23636  dchrvmasumiflem1  23664  mulog2sumlem2  23698  pntrmax  23727  pntibndlem2  23754  pntibndlem3  23755  pntlemf  23768  axlowdimlem16  24238  nmblolbii  25692  ubthlem1  25764  bcsiALT  26074  nmbdoplbi  26921  nmcexi  26923  nmcoplbi  26925  lnconi  26930  nmbdfnlbi  26946  nmcfnlbi  26949  nmopcoi  26992  branmfn  27002  leopmul  27031  nmopleid  27036  esumcvg  28070  ballotlemfrceq  28445  sinccvglem  29016  ftc1cnnclem  30064  ftc1anclem5  30070  opnrebl2  30115  ivthALT  30129  incsequz2  30218  nnubfi  30219  bfplem2  30295  pell14qrgap  30787  pellfundre  30793  pellfundlb  30796  stoweidlem17  31753  stoweidlem34  31770  wallispilem1  31801  leltletr  32272  ltsubnn0  32281  2elfz2melfz  32288  elfzelfzlble  32291  subsubelfzo0  32292