Theorem ltnled 11405

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-xr 11296  df-le 11298

This theorem is referenced by:  ltsub1  11756  ltsub2  11757  0mnnnnn0  12555  mul2lt0bi  13138  fzp1nel  13647  fzodisj  13729  elfznelfzob  13808  ccatsymb  14616  swrdnd  14688  cshwcsh2id  14863  01sqrexlem7  15283  sqrtlt  15296  lo1bdd2  15556  isercoll  15700  fprodntriv  15974  fzm1ndvds  16355  fzo0dvdseq  16356  bitsfzolem  16467  bitsfzo  16468  sadcaddlem  16490  smuval2  16515  bezoutlem3  16574  2mulprm  16726  isprm5  16740  odzdvds  16828  prm23ge5  16848  pc2dvds  16912  pockthg  16939  prmreclem1  16949  prmreclem5  16953  1arith  16960  4sqlem11  16988  vdwlem6  17019  vdwlem11  17024  ramlb  17052  oddvds  19579  gexdvds  19616  sylow1lem3  19632  zringlpirlem3  21492  psdmul  22187  coe1tmmul2  22294  iccntr  24856  icccmplem2  24858  reconnlem2  24862  evth  25004  lebnumlem3  25008  nmoleub2lem3  25161  minveclem3b  25475  minveclem4  25479  pmltpclem2  25497  ovolgelb  25528  ovolicc2lem2  25566  ovolicc2lem4  25568  mbfposr  25700  itg2const2  25790  itg2cnlem2  25811  itg2cn  25812  plyco0  26245  coeeulem  26277  dgradd2  26322  cxplt2  26754  fsumharmonic  27069  dmlogdmgm  27081  lgamgulmlem1  27086  lgamucov  27095  ftalem3  27132  ftalem5  27134  ftalem7  27136  ppiprm  27208  chtprm  27210  chpub  27278  perfectlem2  27288  bposlem1  27342  lgsdilem2  27391  lgsqrlem2  27405  lgsquadlem2  27439  2sqblem  27489  2sqmod  27494  2sqnn0  27496  pntpbnd1  27644  pntlem3  27667  nbusgrvtxm1  29410  crctcshwlkn0lem3  29841  frgrreggt1  30421  minvecolem4  30908  minvecolem5  30909  nndiffz1  32794  psgnfzto1stlem  33102  lmdvg  33913  eulerpartlems  34341  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemrv2  34502  signsply0  34544  reprinfz1  34615  lpadmax  34675  lpadright  34677  0nn0m1nnn0  35096  erdszelem8  35182  bccolsum  35718  unbdqndv2lem1  36491  unbdqndv2lem2  36492  poimirlem2  37608  poimirlem3  37609  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem26  37632  poimirlem31  37637  poimir  37639  mblfinlem2  37644  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  iblabsnclem  37669  ftc1anclem5  37683  areacirclem4  37697  areacirclem5  37698  areacirc  37699  cntotbnd  37782  aks4d1p5  42061  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootlekpowne0  42086  hashnexinj  42109  sticksstones1  42127  sticksstones22  42149  unitscyglem2  42177  unitscyglem4  42179  metakunt29  42214  metakunt30  42215  infdesc  42629  elpell1qr2  42859  pellfundglb  42872  pellfund14gap  42874  congabseq  42962  jm2.19  42981  jm2.26lem3  42989  dgraa0p  43137  dvgrat  44307  uzwo4  44992  divlt0gt0d  45236  supxrgere  45282  uzublem  45379  nleltd  45401  supminfxr  45413  xrpnf  45435  sqrlearg  45505  lptre2pt  45595  limsupubuzlem  45667  climxrrelem  45704  climxlim2lem  45800  icccncfext  45842  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  volioore  45945  voliooico  45947  voliccico  45954  stoweidlem26  45981  stoweidlem34  45989  stoweidlem59  46014  stirlinglem5  46033  dirkercncflem1  46058  fourierdlem10  46072  fourierdlem19  46081  fourierdlem25  46087  fourierdlem35  46097  fourierdlem40  46102  fourierdlem42  46104  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem104  46165  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem32  46221  etransclem41  46230  hsphoidmvle2  46540  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem2  46551  hoidmvlelem4  46553  hoidmvlelem5  46554  hoiqssbllem3  46579  hspmbllem1  46581  hspmbllem2  46582  vonicc  46640  pimdecfgtioo  46672  pimincfltioo  46673  et-sqrtnegnre  46828  fmtno4prmfac  47496  requad01  47545  requad1  47546  perfectALTVlem2  47646  itsclc0yqsol  48613  aacllem  49031