Theorem ltnled 11131

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 11063	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879   < clt 11018   ≤ cle 11019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-cnv 5598  df-xr 11022  df-le 11024

This theorem is referenced by:  ltsub1  11480  ltsub2  11481  0mnnnnn0  12274  mul2lt0bi  12845  fzp1nel  13349  fzodisj  13430  elfznelfzob  13502  ccatsymb  14296  swrdnd  14376  cshwcsh2id  14550  sqrlem7  14969  sqrtlt  14982  lo1bdd2  15242  isercoll  15388  fprodntriv  15661  fzm1ndvds  16040  fzo0dvdseq  16041  bitsfzolem  16150  bitsfzo  16151  sadcaddlem  16173  smuval2  16198  bezoutlem3  16258  2mulprm  16407  isprm5  16421  odzdvds  16505  prm23ge5  16525  pc2dvds  16589  pockthg  16616  prmreclem1  16626  prmreclem5  16630  1arith  16637  4sqlem11  16665  vdwlem6  16696  vdwlem11  16701  ramlb  16729  oddvds  19164  gexdvds  19198  sylow1lem3  19214  zringlpirlem3  20695  coe1tmmul2  21456  iccntr  23993  icccmplem2  23995  reconnlem2  23999  evth  24131  lebnumlem3  24135  nmoleub2lem3  24287  minveclem3b  24601  minveclem4  24605  pmltpclem2  24622  ovolgelb  24653  ovolicc2lem2  24691  ovolicc2lem4  24693  mbfposr  24825  itg2const2  24915  itg2cnlem2  24936  itg2cn  24937  plyco0  25362  coeeulem  25394  dgradd2  25438  cxplt2  25862  fsumharmonic  26170  dmlogdmgm  26182  lgamgulmlem1  26187  lgamucov  26196  ftalem3  26233  ftalem5  26235  ftalem7  26237  ppiprm  26309  chtprm  26311  chpub  26377  perfectlem2  26387  bposlem1  26441  lgsdilem2  26490  lgsqrlem2  26504  lgsquadlem2  26538  2sqblem  26588  2sqmod  26593  2sqnn0  26595  pntpbnd1  26743  pntlem3  26766  nbusgrvtxm1  27755  crctcshwlkn0lem3  28186  frgrreggt1  28766  minvecolem4  29251  minvecolem5  29252  nndiffz1  31116  psgnfzto1stlem  31376  lmdvg  31912  eulerpartlems  32336  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemrv2  32497  signsply0  32539  reprinfz1  32611  lpadmax  32671  lpadright  32673  0nn0m1nnn0  33080  erdszelem8  33169  bccolsum  33714  unbdqndv2lem1  34698  unbdqndv2lem2  34699  poimirlem2  35788  poimirlem3  35789  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem26  35812  poimirlem31  35817  poimir  35819  mblfinlem2  35824  itg2addnclem  35837  itg2addnclem2  35838  itg2addnclem3  35839  iblabsnclem  35849  ftc1anclem5  35863  areacirclem4  35877  areacirclem5  35878  areacirc  35879  cntotbnd  35963  aks4d1p5  40095  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  sticksstones1  40109  sticksstones22  40131  metakunt29  40160  metakunt30  40161  infdesc  40487  elpell1qr2  40701  pellfundglb  40714  pellfund14gap  40716  congabseq  40803  jm2.19  40822  jm2.26lem3  40830  dgraa0p  40981  dvgrat  41937  uzwo4  42608  divlt0gt0d  42832  supxrgere  42879  uzublem  42977  nleltd  42999  supminfxr  43011  xrpnf  43033  sqrlearg  43098  lptre2pt  43188  limsupubuzlem  43260  climxrrelem  43297  climxlim2lem  43393  icccncfext  43435  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  volioore  43538  voliooico  43540  voliccico  43547  stoweidlem26  43574  stoweidlem34  43582  stoweidlem59  43607  stirlinglem5  43626  dirkercncflem1  43651  fourierdlem10  43665  fourierdlem19  43674  fourierdlem25  43680  fourierdlem35  43690  fourierdlem40  43695  fourierdlem42  43697  fourierdlem64  43718  fourierdlem65  43719  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem79  43733  fourierdlem104  43758  fourierswlem  43778  fouriersw  43779  elaa2lem  43781  etransclem32  43814  etransclem41  43823  hsphoidmvle2  44130  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem2  44141  hoidmvlelem4  44143  hoidmvlelem5  44144  hoiqssbllem3  44169  hspmbllem1  44171  hspmbllem2  44172  vonicc  44230  pimdecfgtioo  44262  pimincfltioo  44263  fmtno4prmfac  45035  requad01  45084  requad1  45085  perfectALTVlem2  45185  itsclc0yqsol  46121  aacllem  46516