Theorem ltnled 11292

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  ltsub1  11645  ltsub2  11646  0mnnnnn0  12445  mul2lt0bi  13025  fzp1nel  13539  fzodisj  13621  elfznelfzob  13702  ccatsymb  14518  swrdnd  14590  cshwcsh2id  14763  01sqrexlem7  15183  sqrtlt  15196  lo1bdd2  15459  isercoll  15603  fprodntriv  15877  fzm1ndvds  16261  fzo0dvdseq  16262  bitsfzolem  16373  bitsfzo  16374  sadcaddlem  16396  smuval2  16421  bezoutlem3  16480  2mulprm  16632  isprm5  16646  odzdvds  16735  prm23ge5  16755  pc2dvds  16819  pockthg  16846  prmreclem1  16856  prmreclem5  16860  1arith  16867  4sqlem11  16895  vdwlem6  16926  vdwlem11  16931  ramlb  16959  oddvds  19488  gexdvds  19525  sylow1lem3  19541  zringlpirlem3  21431  psdmul  22121  coe1tmmul2  22230  iccntr  24778  icccmplem2  24780  reconnlem2  24784  evth  24926  lebnumlem3  24930  nmoleub2lem3  25083  minveclem3b  25396  minveclem4  25400  pmltpclem2  25418  ovolgelb  25449  ovolicc2lem2  25487  ovolicc2lem4  25489  mbfposr  25621  itg2const2  25710  itg2cnlem2  25731  itg2cn  25732  plyco0  26165  coeeulem  26197  dgradd2  26242  cxplt2  26675  fsumharmonic  26990  dmlogdmgm  27002  lgamgulmlem1  27007  lgamucov  27016  ftalem3  27053  ftalem5  27055  ftalem7  27057  ppiprm  27129  chtprm  27131  chpub  27199  perfectlem2  27209  bposlem1  27263  lgsdilem2  27312  lgsqrlem2  27326  lgsquadlem2  27360  2sqblem  27410  2sqmod  27415  2sqnn0  27417  pntpbnd1  27565  pntlem3  27588  nbusgrvtxm1  29464  crctcshwlkn0lem3  29897  frgrreggt1  30480  minvecolem4  30968  minvecolem5  30969  nndiffz1  32877  psgnfzto1stlem  33194  exsslsb  33774  lmdvg  34131  eulerpartlems  34538  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemrv2  34700  signsply0  34729  reprinfz1  34800  lpadmax  34860  lpadright  34862  0nn0m1nnn0  35329  erdszelem8  35414  bccolsum  35955  unbdqndv2lem1  36731  unbdqndv2lem2  36732  poimirlem2  37873  poimirlem3  37874  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem23  37894  poimirlem26  37897  poimirlem31  37902  poimir  37904  mblfinlem2  37909  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  iblabsnclem  37934  ftc1anclem5  37948  areacirclem4  37962  areacirclem5  37963  areacirc  37964  cntotbnd  38047  aks4d1p5  42450  aks4d1p8d2  42455  aks4d1p8  42457  aks4d1p9  42458  posbezout  42470  primrootlekpowne0  42475  hashnexinj  42498  sticksstones1  42516  sticksstones22  42538  unitscyglem2  42566  unitscyglem4  42568  infdesc  43001  elpell1qr2  43229  pellfundglb  43242  pellfund14gap  43244  congabseq  43331  jm2.19  43350  jm2.26lem3  43358  dgraa0p  43506  dvgrat  44668  uzwo4  45413  divlt0gt0d  45648  supxrgere  45692  uzublem  45788  nleltd  45810  supminfxr  45822  xrpnf  45843  sqrlearg  45913  lptre2pt  45998  limsupubuzlem  46070  climxrrelem  46107  climxlim2lem  46203  icccncfext  46245  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  volioore  46348  voliooico  46350  voliccico  46357  stoweidlem26  46384  stoweidlem34  46392  stoweidlem59  46417  stirlinglem5  46436  dirkercncflem1  46461  fourierdlem10  46475  fourierdlem19  46484  fourierdlem25  46490  fourierdlem35  46500  fourierdlem40  46505  fourierdlem42  46507  fourierdlem64  46528  fourierdlem65  46529  fourierdlem74  46538  fourierdlem75  46539  fourierdlem78  46542  fourierdlem79  46543  fourierdlem104  46568  fourierswlem  46588  fouriersw  46589  elaa2lem  46591  etransclem32  46624  etransclem41  46633  hsphoidmvle2  46943  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmvlelem2  46954  hoidmvlelem4  46956  hoidmvlelem5  46957  hoiqssbllem3  46982  hspmbllem1  46984  hspmbllem2  46985  vonicc  47043  pimdecfgtioo  47075  pimincfltioo  47076  et-sqrtnegnre  47231  fmtno4prmfac  47932  requad01  47981  requad1  47982  perfectALTVlem2  48082  itsclc0yqsol  49124  aacllem  50160