Theorem ltnled 9753

Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1
ltd.2

Assertion

Ref	Expression
ltnled

Proof of Theorem ltnled

Step	Hyp	Ref	Expression
1		ltd.1	. 2
2		ltd.2	. 2
3		ltnle 9685	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  e.wcel 1818   class class class wbr 4452  cr 9512  clt 9649  cle 9650

This theorem is referenced by:  ltsub1  10073  ltsub2  10074  0mnnnnn0  10853  fzp1nel  11791  fzodisj  11859  elfznelfzob  11916  cshwcsh2id  12796  sqrlem7  13082  sqrtlt  13095  lo1bdd2  13347  isercoll  13490  fprodntriv  13749  fzm1ndvds  14038  fzo0dvdseq  14039  bitsfzolem  14084  bitsfzo  14085  sadcaddlem  14107  smuval2  14132  bezoutlem3  14178  isprm5  14253  odzdvds  14322  pc2dvds  14402  pockthg  14424  prmreclem1  14434  prmreclem5  14438  1arith  14445  4sqlem11  14473  vdwlem6  14504  vdwlem11  14509  ramlb  14537  oddvds  16571  gexdvds  16604  sylow1lem3  16620  coe1tmmul2  18317  zringlpirlem3  18511  zlpirlem3  18516  iccntr  21326  icccmplem2  21328  reconnlem2  21332  evth  21459  lebnumlem3  21463  nmoleub2lem3  21598  minveclem3b  21843  minveclem4  21847  pmltpclem2  21861  ovolgelb  21891  ovolicc2lem2  21929  ovolicc2lem4  21931  mbfposr  22059  itg2const2  22148  itg2cnlem2  22169  itg2cn  22170  plyco0  22589  coeeulem  22621  dgradd2  22665  pilem3  22848  cxplt2  23079  fsumharmonic  23341  ftalem3  23348  ftalem5  23350  ftalem7  23352  ppiprm  23425  chtprm  23427  chpub  23495  perfectlem2  23505  bposlem1  23559  lgsdilem2  23606  lgsqrlem2  23617  lgsquadlem2  23630  2sqblem  23652  pntpbnd1  23771  pntlem3  23794  clwwlkgt0  24771  eupath2lem3  24979  frgrareggt1  25116  minvecolem4  25796  minvecolem5  25797  mul2lt0bi  27569  nndiffz1  27596  2sqmod  27636  lmdvg  27935  eulerpartlems  28299  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemrv2  28460  signsply0  28508  dmlogdmgm  28566  lgamgulmlem1  28571  lgamucov  28580  erdszelem8  28642  mblfinlem2  30052  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  iblabsnclem  30078  ftc1anclem5  30094  areacirclem4  30110  areacirclem5  30111  areacirc  30112  cntotbnd  30292  elpell1qr2  30808  pellfundglb  30821  pellfund14gap  30823  congabseq  30912  jm2.19  30935  jm2.26lem3  30943  dgraa0p  31098  dvgrat  31193  divlt0gt0d  31469  lptre2pt  31646  icccncfext  31690  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem26  31808  stoweidlem34  31816  stoweidlem59  31841  stirlinglem5  31860  dirkercncflem1  31885  fourierdlem10  31899  fourierdlem19  31908  fourierdlem25  31914  fourierdlem35  31924  fourierdlem40  31929  fourierdlem42  31931  fourierdlem64  31953  fourierdlem65  31954  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem104  31993  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  etransclem32  32049  etransclem41  32058  aacllem  33216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-xr 9653  df-le 9655