Theorem ltnled 11496

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   < clt 11382   ≤ cle 11383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-xr 11386  df-le 11388

This theorem is used by:  ltsub1  11852  ltsub2  11853  0mnnnnn0  12678  0nn0m1nnn0  12793  mul2lt0bi  13268  fzp1nel  13785  fzodisj  13868  elfznelfzob  13949  ccatsymb  14769  swrdnd  14846  cshwcsh2id  15021  01sqrexlem7  15458  sqrtlt  15471  lo1bdd2  15735  isercoll  15879  fprodntriv  16153  fzm1ndvds  16536  fzo0dvdseq  16537  bitsfzolem  16648  bitsfzo  16649  sadcaddlem  16671  smuval2  16696  bezoutlem3  16758  2mulprm  16912  isprm5  16927  odzdvds  17017  prm23ge5  17037  pc2dvds  17101  pockthg  17128  prmreclem1  17138  prmreclem5  17142  1arith  17149  4sqlem11  17177  vdwlem6  17208  vdwlem11  17213  ramlb  17241  oddvds  19812  gexdvds  19849  sylow1lem3  19865  zringlpirlem3  21825  psdmul  22542  coe1tmmul2  22650  iccntr  25196  icccmplem2  25198  reconnlem2  25202  evth  25335  lebnumlem3  25339  nmoleub2lem3  25491  minveclem3b  25804  minveclem4  25808  pmltpclem2  25825  ovolgelb  25856  ovolicc2lem2  25894  ovolicc2lem4  25896  mbfposr  26028  itg2const2  26117  itg2cnlem2  26138  itg2cn  26139  plyco0  26565  coeeulem  26598  dgradd2  26642  cxplt2  27083  fsumharmonic  27396  dmlogdmgm  27408  lgamgulmlem1  27413  lgamucov  27422  ftalem3  27459  ftalem5  27461  ftalem7  27463  ppiprm  27535  chtprm  27537  chpub  27604  perfectlem2  27614  bposlem1  27668  lgsdilem2  27717  lgsqrlem2  27731  lgsquadlem2  27765  2sqblem  27815  2sqmod  27820  2sqnn0  27822  pntpbnd1  27970  pntlem3  27993  infdesc  28024  nbusgrvtxm1  30017  crctcshwlkn0lem3  30458  frgrreggt1  31051  minvecolem4  31539  minvecolem5  31540  nndiffz1  33474  psgnfzto1stlem  33760  exsslsb  34340  lmdvg  34696  eulerpartlems  35103  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemrv2  35265  signsply0  35291  reprinfz1  35362  lpadmax  35425  lpadright  35427  erdszelem8  36171  bccolsum  36719  unbdqndv2lem1  37590  unbdqndv2lem2  37591  poimirlem2  38808  poimirlem3  38809  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem23  38829  poimirlem26  38832  poimirlem31  38837  poimir  38839  mblfinlem2  38844  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  iblabsnclem  38869  ftc1anclem5  38883  areacirclem4  38897  areacirclem5  38898  areacirc  38899  cntotbnd  38996  aks4d1p5  43396  aks4d1p8d2  43401  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  primrootlekpowne0  43421  hashnexinj  43444  sticksstones1  43462  sticksstones22  43484  unitscyglem2  43512  unitscyglem4  43514  elpell1qr2  44145  pellfundglb  44158  pellfund14gap  44160  congabseq  44247  jm2.19  44266  jm2.26lem3  44274  dgraa0p  44416  dvgrat  45557  uzwo4  46344  divlt0gt0d  46575  supxrgere  46618  uzublem  46713  nleltd  46735  supminfxr  46747  xrpnf  46768  sqrlearg  46838  lptre2pt  46923  limsupubuzlem  46995  climxrrelem  47032  climxlim2lem  47128  icccncfext  47170  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  volioore  47273  voliooico  47275  voliccico  47282  stoweidlem26  47309  stoweidlem34  47317  stoweidlem59  47342  stirlinglem5  47361  dirkercncflem1  47386  fourierdlem10  47400  fourierdlem19  47409  fourierdlem25  47415  fourierdlem35  47425  fourierdlem40  47430  fourierdlem42  47432  fourierdlem64  47453  fourierdlem65  47454  fourierdlem74  47463  fourierdlem75  47464  fourierdlem78  47467  fourierdlem79  47468  fourierdlem104  47493  fourierswlem  47513  fouriersw  47514  elaa2lem  47516  etransclem32  47549  etransclem41  47558  hsphoidmvle2  47868  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmvlelem2  47879  hoidmvlelem4  47881  hoidmvlelem5  47882  hoiqssbllem3  47907  hspmbllem1  47909  hspmbllem2  47910  vonicc  47968  pimdecfgtioo  48000  pimincfltioo  48001  et-sqrtnegnre  48156  fmtno4prmfac  48930  requad01  48992  requad1  48993  perfectALTVlem2  49093  itsclc0yqsol  50207  aacllem  51367