Theorem ltnled 11287

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031   < clt 11173   ≤ cle 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-xr 11177  df-le 11179

This theorem is referenced by:  ltsub1  11640  ltsub2  11641  0mnnnnn0  12463  mul2lt0bi  13044  fzp1nel  13559  fzodisj  13642  elfznelfzob  13723  ccatsymb  14539  swrdnd  14611  cshwcsh2id  14784  01sqrexlem7  15204  sqrtlt  15217  lo1bdd2  15480  isercoll  15624  fprodntriv  15901  fzm1ndvds  16285  fzo0dvdseq  16286  bitsfzolem  16397  bitsfzo  16398  sadcaddlem  16420  smuval2  16445  bezoutlem3  16504  2mulprm  16656  isprm5  16671  odzdvds  16760  prm23ge5  16780  pc2dvds  16844  pockthg  16871  prmreclem1  16881  prmreclem5  16885  1arith  16892  4sqlem11  16920  vdwlem6  16951  vdwlem11  16956  ramlb  16984  oddvds  19516  gexdvds  19553  sylow1lem3  19569  zringlpirlem3  21457  psdmul  22145  coe1tmmul2  22254  iccntr  24800  icccmplem2  24802  reconnlem2  24806  evth  24939  lebnumlem3  24943  nmoleub2lem3  25095  minveclem3b  25408  minveclem4  25412  pmltpclem2  25429  ovolgelb  25460  ovolicc2lem2  25498  ovolicc2lem4  25500  mbfposr  25632  itg2const2  25721  itg2cnlem2  25742  itg2cn  25743  plyco0  26170  coeeulem  26202  dgradd2  26246  cxplt2  26678  fsumharmonic  26992  dmlogdmgm  27004  lgamgulmlem1  27009  lgamucov  27018  ftalem3  27055  ftalem5  27057  ftalem7  27059  ppiprm  27131  chtprm  27133  chpub  27200  perfectlem2  27210  bposlem1  27264  lgsdilem2  27313  lgsqrlem2  27327  lgsquadlem2  27361  2sqblem  27411  2sqmod  27416  2sqnn0  27418  pntpbnd1  27566  pntlem3  27589  nbusgrvtxm1  29465  crctcshwlkn0lem3  29898  frgrreggt1  30481  minvecolem4  30969  minvecolem5  30970  nndiffz1  32877  psgnfzto1stlem  33179  exsslsb  33759  lmdvg  34116  eulerpartlems  34523  ballotlemfc0  34656  ballotlemfcc  34657  ballotlemrv2  34685  signsply0  34714  reprinfz1  34785  lpadmax  34845  lpadright  34847  0nn0m1nnn0  35314  erdszelem8  35399  bccolsum  35940  unbdqndv2lem1  36788  unbdqndv2lem2  36789  poimirlem2  37960  poimirlem3  37961  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem23  37981  poimirlem26  37984  poimirlem31  37989  poimir  37991  mblfinlem2  37996  itg2addnclem  38009  itg2addnclem2  38010  itg2addnclem3  38011  iblabsnclem  38021  ftc1anclem5  38035  areacirclem4  38049  areacirclem5  38050  areacirc  38051  cntotbnd  38134  aks4d1p5  42536  aks4d1p8d2  42541  aks4d1p8  42543  aks4d1p9  42544  posbezout  42556  primrootlekpowne0  42561  hashnexinj  42584  sticksstones1  42602  sticksstones22  42624  unitscyglem2  42652  unitscyglem4  42654  infdesc  43093  elpell1qr2  43321  pellfundglb  43334  pellfund14gap  43336  congabseq  43423  jm2.19  43442  jm2.26lem3  43450  dgraa0p  43598  dvgrat  44760  uzwo4  45505  divlt0gt0d  45740  supxrgere  45784  uzublem  45879  nleltd  45901  supminfxr  45913  xrpnf  45934  sqrlearg  46004  lptre2pt  46089  limsupubuzlem  46161  climxrrelem  46198  climxlim2lem  46294  icccncfext  46336  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  volioore  46439  voliooico  46441  voliccico  46448  stoweidlem26  46475  stoweidlem34  46483  stoweidlem59  46508  stirlinglem5  46527  dirkercncflem1  46552  fourierdlem10  46566  fourierdlem19  46575  fourierdlem25  46581  fourierdlem35  46591  fourierdlem40  46596  fourierdlem42  46598  fourierdlem64  46619  fourierdlem65  46620  fourierdlem74  46629  fourierdlem75  46630  fourierdlem78  46633  fourierdlem79  46634  fourierdlem104  46659  fourierswlem  46679  fouriersw  46680  elaa2lem  46682  etransclem32  46715  etransclem41  46724  hsphoidmvle2  47034  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmvlelem2  47045  hoidmvlelem4  47047  hoidmvlelem5  47048  hoiqssbllem3  47073  hspmbllem1  47075  hspmbllem2  47076  vonicc  47134  pimdecfgtioo  47166  pimincfltioo  47167  et-sqrtnegnre  47322  fmtno4prmfac  48050  requad01  48112  requad1  48113  perfectALTVlem2  48213  itsclc0yqsol  49255  aacllem  50291