Theorem ltnled 11263

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-xr 11153  df-le 11155

This theorem is referenced by:  ltsub1  11616  ltsub2  11617  0mnnnnn0  12416  mul2lt0bi  13001  fzp1nel  13514  fzodisj  13596  elfznelfzob  13676  ccatsymb  14489  swrdnd  14561  cshwcsh2id  14735  01sqrexlem7  15155  sqrtlt  15168  lo1bdd2  15431  isercoll  15575  fprodntriv  15849  fzm1ndvds  16233  fzo0dvdseq  16234  bitsfzolem  16345  bitsfzo  16346  sadcaddlem  16368  smuval2  16393  bezoutlem3  16452  2mulprm  16604  isprm5  16618  odzdvds  16707  prm23ge5  16727  pc2dvds  16791  pockthg  16818  prmreclem1  16828  prmreclem5  16832  1arith  16839  4sqlem11  16867  vdwlem6  16898  vdwlem11  16903  ramlb  16931  oddvds  19426  gexdvds  19463  sylow1lem3  19479  zringlpirlem3  21371  psdmul  22051  coe1tmmul2  22160  iccntr  24708  icccmplem2  24710  reconnlem2  24714  evth  24856  lebnumlem3  24860  nmoleub2lem3  25013  minveclem3b  25326  minveclem4  25330  pmltpclem2  25348  ovolgelb  25379  ovolicc2lem2  25417  ovolicc2lem4  25419  mbfposr  25551  itg2const2  25640  itg2cnlem2  25661  itg2cn  25662  plyco0  26095  coeeulem  26127  dgradd2  26172  cxplt2  26605  fsumharmonic  26920  dmlogdmgm  26932  lgamgulmlem1  26937  lgamucov  26946  ftalem3  26983  ftalem5  26985  ftalem7  26987  ppiprm  27059  chtprm  27061  chpub  27129  perfectlem2  27139  bposlem1  27193  lgsdilem2  27242  lgsqrlem2  27256  lgsquadlem2  27290  2sqblem  27340  2sqmod  27345  2sqnn0  27347  pntpbnd1  27495  pntlem3  27518  nbusgrvtxm1  29324  crctcshwlkn0lem3  29757  frgrreggt1  30337  minvecolem4  30824  minvecolem5  30825  nndiffz1  32729  psgnfzto1stlem  33042  exsslsb  33563  lmdvg  33920  eulerpartlems  34328  ballotlemfc0  34461  ballotlemfcc  34462  ballotlemrv2  34490  signsply0  34519  reprinfz1  34590  lpadmax  34650  lpadright  34652  0nn0m1nnn0  35090  erdszelem8  35175  bccolsum  35716  unbdqndv2lem1  36487  unbdqndv2lem2  36488  poimirlem2  37606  poimirlem3  37607  poimirlem6  37610  poimirlem7  37611  poimirlem8  37612  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem21  37625  poimirlem22  37626  poimirlem23  37627  poimirlem26  37630  poimirlem31  37635  poimir  37637  mblfinlem2  37642  itg2addnclem  37655  itg2addnclem2  37656  itg2addnclem3  37657  iblabsnclem  37667  ftc1anclem5  37681  areacirclem4  37695  areacirclem5  37696  areacirc  37697  cntotbnd  37780  aks4d1p5  42057  aks4d1p8d2  42062  aks4d1p8  42064  aks4d1p9  42065  posbezout  42077  primrootlekpowne0  42082  hashnexinj  42105  sticksstones1  42123  sticksstones22  42145  unitscyglem2  42173  unitscyglem4  42175  infdesc  42620  elpell1qr2  42849  pellfundglb  42862  pellfund14gap  42864  congabseq  42951  jm2.19  42970  jm2.26lem3  42978  dgraa0p  43126  dvgrat  44289  uzwo4  45035  divlt0gt0d  45272  supxrgere  45317  uzublem  45413  nleltd  45435  supminfxr  45447  xrpnf  45468  sqrlearg  45538  lptre2pt  45625  limsupubuzlem  45697  climxrrelem  45734  climxlim2lem  45830  icccncfext  45872  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  volioore  45975  voliooico  45977  voliccico  45984  stoweidlem26  46011  stoweidlem34  46019  stoweidlem59  46044  stirlinglem5  46063  dirkercncflem1  46088  fourierdlem10  46102  fourierdlem19  46111  fourierdlem25  46117  fourierdlem35  46127  fourierdlem40  46132  fourierdlem42  46134  fourierdlem64  46155  fourierdlem65  46156  fourierdlem74  46165  fourierdlem75  46166  fourierdlem78  46169  fourierdlem79  46170  fourierdlem104  46195  fourierswlem  46215  fouriersw  46216  elaa2lem  46218  etransclem32  46251  etransclem41  46260  hsphoidmvle2  46570  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmvlelem2  46581  hoidmvlelem4  46583  hoidmvlelem5  46584  hoiqssbllem3  46609  hspmbllem1  46611  hspmbllem2  46612  vonicc  46670  pimdecfgtioo  46702  pimincfltioo  46703  et-sqrtnegnre  46858  fmtno4prmfac  47560  requad01  47609  requad1  47610  perfectALTVlem2  47710  itsclc0yqsol  48753  aacllem  49790