Theorem ltnled 11328

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-xr 11219  df-le 11221

This theorem is referenced by:  ltsub1  11681  ltsub2  11682  0mnnnnn0  12481  mul2lt0bi  13066  fzp1nel  13579  fzodisj  13661  elfznelfzob  13741  ccatsymb  14554  swrdnd  14626  cshwcsh2id  14801  01sqrexlem7  15221  sqrtlt  15234  lo1bdd2  15497  isercoll  15641  fprodntriv  15915  fzm1ndvds  16299  fzo0dvdseq  16300  bitsfzolem  16411  bitsfzo  16412  sadcaddlem  16434  smuval2  16459  bezoutlem3  16518  2mulprm  16670  isprm5  16684  odzdvds  16773  prm23ge5  16793  pc2dvds  16857  pockthg  16884  prmreclem1  16894  prmreclem5  16898  1arith  16905  4sqlem11  16933  vdwlem6  16964  vdwlem11  16969  ramlb  16997  oddvds  19484  gexdvds  19521  sylow1lem3  19537  zringlpirlem3  21381  psdmul  22060  coe1tmmul2  22169  iccntr  24717  icccmplem2  24719  reconnlem2  24723  evth  24865  lebnumlem3  24869  nmoleub2lem3  25022  minveclem3b  25335  minveclem4  25339  pmltpclem2  25357  ovolgelb  25388  ovolicc2lem2  25426  ovolicc2lem4  25428  mbfposr  25560  itg2const2  25649  itg2cnlem2  25670  itg2cn  25671  plyco0  26104  coeeulem  26136  dgradd2  26181  cxplt2  26614  fsumharmonic  26929  dmlogdmgm  26941  lgamgulmlem1  26946  lgamucov  26955  ftalem3  26992  ftalem5  26994  ftalem7  26996  ppiprm  27068  chtprm  27070  chpub  27138  perfectlem2  27148  bposlem1  27202  lgsdilem2  27251  lgsqrlem2  27265  lgsquadlem2  27299  2sqblem  27349  2sqmod  27354  2sqnn0  27356  pntpbnd1  27504  pntlem3  27527  nbusgrvtxm1  29313  crctcshwlkn0lem3  29749  frgrreggt1  30329  minvecolem4  30816  minvecolem5  30817  nndiffz1  32716  psgnfzto1stlem  33064  exsslsb  33599  lmdvg  33950  eulerpartlems  34358  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemrv2  34520  signsply0  34549  reprinfz1  34620  lpadmax  34680  lpadright  34682  0nn0m1nnn0  35107  erdszelem8  35192  bccolsum  35733  unbdqndv2lem1  36504  unbdqndv2lem2  36505  poimirlem2  37623  poimirlem3  37624  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem26  37647  poimirlem31  37652  poimir  37654  mblfinlem2  37659  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  iblabsnclem  37684  ftc1anclem5  37698  areacirclem4  37712  areacirclem5  37713  areacirc  37714  cntotbnd  37797  aks4d1p5  42075  aks4d1p8d2  42080  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  primrootlekpowne0  42100  hashnexinj  42123  sticksstones1  42141  sticksstones22  42163  unitscyglem2  42191  unitscyglem4  42193  infdesc  42638  elpell1qr2  42867  pellfundglb  42880  pellfund14gap  42882  congabseq  42970  jm2.19  42989  jm2.26lem3  42997  dgraa0p  43145  dvgrat  44308  uzwo4  45054  divlt0gt0d  45291  supxrgere  45336  uzublem  45433  nleltd  45455  supminfxr  45467  xrpnf  45488  sqrlearg  45558  lptre2pt  45645  limsupubuzlem  45717  climxrrelem  45754  climxlim2lem  45850  icccncfext  45892  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  volioore  45995  voliooico  45997  voliccico  46004  stoweidlem26  46031  stoweidlem34  46039  stoweidlem59  46064  stirlinglem5  46083  dirkercncflem1  46108  fourierdlem10  46122  fourierdlem19  46131  fourierdlem25  46137  fourierdlem35  46147  fourierdlem40  46152  fourierdlem42  46154  fourierdlem64  46175  fourierdlem65  46176  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem79  46190  fourierdlem104  46215  fourierswlem  46235  fouriersw  46236  elaa2lem  46238  etransclem32  46271  etransclem41  46280  hsphoidmvle2  46590  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem2  46601  hoidmvlelem4  46603  hoidmvlelem5  46604  hoiqssbllem3  46629  hspmbllem1  46631  hspmbllem2  46632  vonicc  46690  pimdecfgtioo  46722  pimincfltioo  46723  et-sqrtnegnre  46878  fmtno4prmfac  47577  requad01  47626  requad1  47627  perfectALTVlem2  47727  itsclc0yqsol  48757  aacllem  49794