Theorem ltnled 11260

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005   < clt 11146   ≤ cle 11147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-xr 11150  df-le 11152

This theorem is referenced by:  ltsub1  11613  ltsub2  11614  0mnnnnn0  12413  mul2lt0bi  12998  fzp1nel  13511  fzodisj  13593  elfznelfzob  13674  ccatsymb  14490  swrdnd  14562  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  19459  gexdvds  19496  sylow1lem3  19512  zringlpirlem3  21401  psdmul  22081  coe1tmmul2  22190  iccntr  24737  icccmplem2  24739  reconnlem2  24743  evth  24885  lebnumlem3  24889  nmoleub2lem3  25042  minveclem3b  25355  minveclem4  25359  pmltpclem2  25377  ovolgelb  25408  ovolicc2lem2  25446  ovolicc2lem4  25448  mbfposr  25580  itg2const2  25669  itg2cnlem2  25690  itg2cn  25691  plyco0  26124  coeeulem  26156  dgradd2  26201  cxplt2  26634  fsumharmonic  26949  dmlogdmgm  26961  lgamgulmlem1  26966  lgamucov  26975  ftalem3  27012  ftalem5  27014  ftalem7  27016  ppiprm  27088  chtprm  27090  chpub  27158  perfectlem2  27168  bposlem1  27222  lgsdilem2  27271  lgsqrlem2  27285  lgsquadlem2  27319  2sqblem  27369  2sqmod  27374  2sqnn0  27376  pntpbnd1  27524  pntlem3  27547  nbusgrvtxm1  29357  crctcshwlkn0lem3  29790  frgrreggt1  30373  minvecolem4  30860  minvecolem5  30861  nndiffz1  32769  psgnfzto1stlem  33069  exsslsb  33609  lmdvg  33966  eulerpartlems  34373  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemrv2  34535  signsply0  34564  reprinfz1  34635  lpadmax  34695  lpadright  34697  0nn0m1nnn0  35157  erdszelem8  35242  bccolsum  35783  unbdqndv2lem1  36553  unbdqndv2lem2  36554  poimirlem2  37672  poimirlem3  37673  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem23  37693  poimirlem26  37696  poimirlem31  37701  poimir  37703  mblfinlem2  37708  itg2addnclem  37721  itg2addnclem2  37722  itg2addnclem3  37723  iblabsnclem  37733  ftc1anclem5  37747  areacirclem4  37761  areacirclem5  37762  areacirc  37763  cntotbnd  37846  aks4d1p5  42183  aks4d1p8d2  42188  aks4d1p8  42190  aks4d1p9  42191  posbezout  42203  primrootlekpowne0  42208  hashnexinj  42231  sticksstones1  42249  sticksstones22  42271  unitscyglem2  42299  unitscyglem4  42301  infdesc  42746  elpell1qr2  42975  pellfundglb  42988  pellfund14gap  42990  congabseq  43077  jm2.19  43096  jm2.26lem3  43104  dgraa0p  43252  dvgrat  44415  uzwo4  45160  divlt0gt0d  45397  supxrgere  45442  uzublem  45538  nleltd  45560  supminfxr  45572  xrpnf  45593  sqrlearg  45663  lptre2pt  45748  limsupubuzlem  45820  climxrrelem  45857  climxlim2lem  45953  icccncfext  45995  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  volioore  46098  voliooico  46100  voliccico  46107  stoweidlem26  46134  stoweidlem34  46142  stoweidlem59  46167  stirlinglem5  46186  dirkercncflem1  46211  fourierdlem10  46225  fourierdlem19  46234  fourierdlem25  46240  fourierdlem35  46250  fourierdlem40  46255  fourierdlem42  46257  fourierdlem64  46278  fourierdlem65  46279  fourierdlem74  46288  fourierdlem75  46289  fourierdlem78  46292  fourierdlem79  46293  fourierdlem104  46318  fourierswlem  46338  fouriersw  46339  elaa2lem  46341  etransclem32  46374  etransclem41  46383  hsphoidmvle2  46693  hoidmv1lelem1  46699  hoidmv1lelem2  46700  hoidmv1lelem3  46701  hoidmvlelem2  46704  hoidmvlelem4  46706  hoidmvlelem5  46707  hoiqssbllem3  46732  hspmbllem1  46734  hspmbllem2  46735  vonicc  46793  pimdecfgtioo  46825  pimincfltioo  46826  et-sqrtnegnre  46981  fmtno4prmfac  47682  requad01  47731  requad1  47732  perfectALTVlem2  47832  itsclc0yqsol  48875  aacllem  49912