Theorem ltle 10126

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

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  ltleletr  10130  letr  10131  letric  10137  ltlen  10138  ltlei  10159  ltled  10185  lt2add  10513  lep1  10862  lem1  10864  letrp1  10865  ltmul12a  10879  mulge0b  10893  lediv12a  10916  bndndx  11291  ltsubnn0  11344  uzind  11469  fnn0ind  11476  eluz2b2  11761  zmin  11784  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  rpge0  11845  rpneg  11863  iccsplit  12305  zltaddlt1le  12324  difelfznle  12453  fvffz0  12457  elfzouz2  12484  elfzo0le  12511  fzostep1  12584  fllep1  12602  fracle1  12604  expgt1  12898  expnbnd  12993  expnlbnd2  12995  faclbnd  13077  swrdsbslen  13448  swrdspsleq  13449  swrdccat3  13492  repswswrd  13531  resqrex  13991  sqrtgt0  13999  absmax  14069  eqsqrt2d  14108  rlim2lt  14228  mulcn2  14326  rlimo1  14347  o1rlimmul  14349  climbdd  14402  caucvgrlem  14403  supcvg  14588  efcllem  14808  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  cos01gt0  14921  absef  14927  efieq1re  14929  ruclem11  14969  nn0o  15099  pythagtriplem12  15531  pythagtriplem13  15532  pythagtriplem14  15533  pythagtriplem16  15535  pclem  15543  prmgaplem4  15758  cshwshashlem2  15803  isabvd  18820  met2ndci  22327  blcvx  22601  iocopnst  22739  nmoleub2a  22917  nmoleub2b  22918  nmhmcn  22920  iscmet3lem2  23090  caubl  23106  ivthlem2  23221  ovolicc2lem4  23288  ioombl1lem4  23329  ioovolcl  23338  volsup2  23373  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  dvne0  23774  ftc1lem4  23802  dgrlt  24022  aalioulem5  24091  ulmbdd  24152  iblulm  24161  radcnvlem1  24167  abelthlem5  24189  abelthlem7  24192  sincosq1lem  24249  tangtx  24257  tanabsge  24258  sinq12ge0  24260  sineq0  24273  tanord  24284  logcj  24352  argregt0  24356  argrege0  24357  argimgt0  24358  logdmnrp  24387  logcnlem3  24390  logf1o2  24396  cxpsqrtlem  24448  abscxpbnd  24494  logreclem  24500  asinneg  24613  atanlogsublem  24642  atanlogsub  24643  rlimcnp  24692  xrlimcnp  24695  basellem8  24814  chtub  24937  bposlem9  25017  chebbnd1  25161  chtppilimlem1  25162  dchrvmasumiflem1  25190  mulog2sumlem2  25224  pntrmax  25253  pntibndlem2  25280  pntibndlem3  25281  pntlemf  25294  axlowdimlem16  25837  pthdlem1  26662  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  nmblolbii  27654  ubthlem1  27726  bcsiALT  28036  nmbdoplbi  28883  nmcexi  28885  nmcoplbi  28887  lnconi  28892  nmbdfnlbi  28908  nmcfnlbi  28911  nmopcoi  28954  branmfn  28964  leopmul  28993  nmopleid  28998  esumcvg  30148  ballotlemfrceq  30590  sinccvglem  31566  opnrebl2  32316  ivthALT  32330  dnibndlem12  32479  poimirlem15  33424  poimirlem31  33440  ftc1cnnclem  33483  ftc1anclem5  33489  incsequz2  33545  nnubfi  33546  bfplem2  33622  pell14qrgap  37439  pellfundre  37445  pellfundlb  37448  stoweidlem17  40234  stoweidlem34  40251  wallispilem1  40282  leltletr  41308  2elfz2melfz  41328  elfzelfzlble  41331  subsubelfzo0  41336  pfxccat3  41426  bgoldbtbnd  41697  bgoldbachlt  41701  tgblthelfgott  41703  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  m1modmmod  42316  nnolog2flm1  42384