Theorem ltle 9662

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 383	. 2 |- ( A < B -> ( A < B \/ A = B ) )
2		leloe 9660	. 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 366   /\ wa 367   = wceq 1398   e. wcel 1823   class class class wbr 4439   RRcr 9480   < clt 9617   <_ cle 9618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-pre-lttri 9555

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623

This theorem is referenced by:  ltleletr  9666  letr  9667  letric  9674  ltlen  9675  ltlei  9695  ltled  9722  lt2add  10033  lep1  10377  lem1  10379  letrp1  10380  ltmul12a  10394  mulge0b  10408  lediv12a  10433  bndndx  10790  uzind  10950  fnn0ind  10959  eluz2b2  11155  zmin  11179  rpnnen1lem1  11209  rpnnen1lem2  11210  rpnnen1lem3  11211  rpnnen1lem5  11213  rpge0  11233  rpneg  11251  iccsplit  11656  difelfznle  11793  elfzouz2  11818  elfzo0le  11843  fzosplitprm1  11900  fzostep1  11903  fllep1  11919  fracle1  11921  expgt1  12189  expnbnd  12280  expnlbnd2  12282  faclbnd  12353  swrdsbslen  12667  swrdspsleq  12668  swrdccat3  12711  repswswrd  12750  resqrex  13169  sqrtgt0  13177  absmax  13247  eqsqrt2d  13286  rlim2lt  13405  mulcn2  13503  rlimo1  13524  o1rlimmul  13526  climbdd  13579  caucvgrlem  13580  supcvg  13752  efcllem  13898  sin01bnd  14005  cos01bnd  14006  sin01gt0  14010  cos01gt0  14011  absef  14017  efieq1re  14019  ruclem11  14060  pythagtriplem12  14437  pythagtriplem13  14438  pythagtriplem14  14439  pythagtriplem16  14441  pclem  14449  cshwshashlem2  14668  isabvd  17667  met2ndci  21194  blcvx  21472  iocopnst  21609  nmoleub2a  21769  nmoleub2b  21770  nmhmcn  21772  iscmet3lem2  21900  caubl  21915  ivthlem2  22033  ovolicc2lem4  22100  ioombl1lem4  22140  ioovolcl  22148  volsup2  22183  itg2monolem1  22326  itg2gt0  22336  itg2cnlem1  22337  dvne0  22581  ftc1lem4  22609  dgrlt  22832  aalioulem5  22901  ulmbdd  22962  iblulm  22971  radcnvlem1  22977  abelthlem5  22999  abelthlem7  23002  sincosq1lem  23059  tangtx  23067  tanabsge  23068  sinq12ge0  23070  sineq0  23083  tanord  23094  logcj  23162  argregt0  23166  argrege0  23167  argimgt0  23168  logdmnrp  23193  logcnlem3  23196  logf1o2  23202  cxpsqrtlem  23254  abscxpbnd  23298  logreclem  23304  asinneg  23417  atanlogsublem  23446  atanlogsub  23447  rlimcnp  23496  xrlimcnp  23499  basellem8  23562  chtub  23688  bposlem9  23768  chebbnd1  23858  chtppilimlem1  23859  dchrvmasumiflem1  23887  mulog2sumlem2  23921  pntrmax  23950  pntibndlem2  23977  pntibndlem3  23978  pntlemf  23991  axlowdimlem16  24465  nmblolbii  25915  ubthlem1  25987  bcsiALT  26297  nmbdoplbi  27144  nmcexi  27146  nmcoplbi  27148  lnconi  27153  nmbdfnlbi  27169  nmcfnlbi  27172  nmopcoi  27215  branmfn  27225  leopmul  27254  nmopleid  27259  esumcvg  28318  ballotlemfrceq  28734  sinccvglem  29305  ftc1cnnclem  30331  ftc1anclem5  30337  opnrebl2  30382  ivthALT  30396  incsequz2  30485  nnubfi  30486  bfplem2  30562  pell14qrgap  31053  pellfundre  31059  pellfundlb  31062  stoweidlem17  32041  stoweidlem34  32058  wallispilem1  32089  pfxccat3  32673  leltletr  32711  ltsubnn0  32720  2elfz2melfz  32727  elfzelfzlble  32730  subsubelfzo0  32731  m1modmmod  33407  nn0o  33412  nnolog2flm1  33484