Theorem ltnled 11288

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2121   class class class wbr 5075  ℝcr 11032   < clt 11174   ≤ cle 11175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-cnv 5629  df-xr 11178  df-le 11180

This theorem is referenced by:  ltsub1  11641  ltsub2  11642  0mnnnnn0  12464  mul2lt0bi  13045  fzp1nel  13560  fzodisj  13643  elfznelfzob  13724  ccatsymb  14540  swrdnd  14612  cshwcsh2id  14785  01sqrexlem7  15205  sqrtlt  15218  lo1bdd2  15481  isercoll  15625  fprodntriv  15902  fzm1ndvds  16286  fzo0dvdseq  16287  bitsfzolem  16398  bitsfzo  16399  sadcaddlem  16421  smuval2  16446  bezoutlem3  16505  2mulprm  16657  isprm5  16672  odzdvds  16761  prm23ge5  16781  pc2dvds  16845  pockthg  16872  prmreclem1  16882  prmreclem5  16886  1arith  16893  4sqlem11  16921  vdwlem6  16952  vdwlem11  16957  ramlb  16985  oddvds  19517  gexdvds  19554  sylow1lem3  19570  zringlpirlem3  21443  psdmul  22158  coe1tmmul2  22266  iccntr  24809  icccmplem2  24811  reconnlem2  24815  evth  24948  lebnumlem3  24952  nmoleub2lem3  25104  minveclem3b  25417  minveclem4  25421  pmltpclem2  25438  ovolgelb  25469  ovolicc2lem2  25507  ovolicc2lem4  25509  mbfposr  25641  itg2const2  25730  itg2cnlem2  25751  itg2cn  25752  plyco0  26179  coeeulem  26211  dgradd2  26255  cxplt2  26684  fsumharmonic  26997  dmlogdmgm  27009  lgamgulmlem1  27014  lgamucov  27023  ftalem3  27060  ftalem5  27062  ftalem7  27064  ppiprm  27136  chtprm  27138  chpub  27205  perfectlem2  27215  bposlem1  27269  lgsdilem2  27318  lgsqrlem2  27332  lgsquadlem2  27366  2sqblem  27416  2sqmod  27421  2sqnn0  27423  pntpbnd1  27571  pntlem3  27594  nbusgrvtxm1  29470  crctcshwlkn0lem3  29902  frgrreggt1  30485  minvecolem4  30973  minvecolem5  30974  nndiffz1  32882  psgnfzto1stlem  33185  exsslsb  33793  lmdvg  34149  eulerpartlems  34556  ballotlemfc0  34689  ballotlemfcc  34690  ballotlemrv2  34718  signsply0  34747  reprinfz1  34818  lpadmax  34881  lpadright  34883  0nn0m1nnn0  35356  erdszelem8  35441  bccolsum  35982  unbdqndv2lem1  36830  unbdqndv2lem2  36831  poimirlem2  38004  poimirlem3  38005  poimirlem6  38008  poimirlem7  38009  poimirlem8  38010  poimirlem16  38018  poimirlem17  38019  poimirlem19  38021  poimirlem20  38022  poimirlem21  38023  poimirlem22  38024  poimirlem23  38025  poimirlem26  38028  poimirlem31  38033  poimir  38035  mblfinlem2  38040  itg2addnclem  38053  itg2addnclem2  38054  itg2addnclem3  38055  iblabsnclem  38065  ftc1anclem5  38079  areacirclem4  38093  areacirclem5  38094  areacirc  38095  cntotbnd  38178  aks4d1p5  42580  aks4d1p8d2  42585  aks4d1p8  42587  aks4d1p9  42588  posbezout  42600  primrootlekpowne0  42605  hashnexinj  42628  sticksstones1  42646  sticksstones22  42668  unitscyglem2  42696  unitscyglem4  42698  infdesc  43108  elpell1qr2  43332  pellfundglb  43345  pellfund14gap  43347  congabseq  43434  jm2.19  43453  jm2.26lem3  43461  dgraa0p  43609  dvgrat  44771  uzwo4  45516  divlt0gt0d  45748  supxrgere  45792  uzublem  45887  nleltd  45909  supminfxr  45921  xrpnf  45942  sqrlearg  46012  lptre2pt  46097  limsupubuzlem  46169  climxrrelem  46206  climxlim2lem  46302  icccncfext  46344  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  volioore  46447  voliooico  46449  voliccico  46456  stoweidlem26  46483  stoweidlem34  46491  stoweidlem59  46516  stirlinglem5  46535  dirkercncflem1  46560  fourierdlem10  46574  fourierdlem19  46583  fourierdlem25  46589  fourierdlem35  46599  fourierdlem40  46604  fourierdlem42  46606  fourierdlem64  46627  fourierdlem65  46628  fourierdlem74  46637  fourierdlem75  46638  fourierdlem78  46641  fourierdlem79  46642  fourierdlem104  46667  fourierswlem  46687  fouriersw  46688  elaa2lem  46690  etransclem32  46723  etransclem41  46732  hsphoidmvle2  47042  hoidmv1lelem1  47048  hoidmv1lelem2  47049  hoidmv1lelem3  47050  hoidmvlelem2  47053  hoidmvlelem4  47055  hoidmvlelem5  47056  hoiqssbllem3  47081  hspmbllem1  47083  hspmbllem2  47084  vonicc  47142  pimdecfgtioo  47174  pimincfltioo  47175  et-sqrtnegnre  47330  fmtno4prmfac  48064  requad01  48126  requad1  48127  perfectALTVlem2  48227  itsclc0yqsol  49269  aacllem  50305