Theorem ltnled 11297

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  ltsub1  11650  ltsub2  11651  0mnnnnn0  12450  mul2lt0bi  13035  fzp1nel  13548  fzodisj  13630  elfznelfzob  13710  ccatsymb  14523  swrdnd  14595  cshwcsh2id  14770  01sqrexlem7  15190  sqrtlt  15203  lo1bdd2  15466  isercoll  15610  fprodntriv  15884  fzm1ndvds  16268  fzo0dvdseq  16269  bitsfzolem  16380  bitsfzo  16381  sadcaddlem  16403  smuval2  16428  bezoutlem3  16487  2mulprm  16639  isprm5  16653  odzdvds  16742  prm23ge5  16762  pc2dvds  16826  pockthg  16853  prmreclem1  16863  prmreclem5  16867  1arith  16874  4sqlem11  16902  vdwlem6  16933  vdwlem11  16938  ramlb  16966  oddvds  19461  gexdvds  19498  sylow1lem3  19514  zringlpirlem3  21406  psdmul  22086  coe1tmmul2  22195  iccntr  24743  icccmplem2  24745  reconnlem2  24749  evth  24891  lebnumlem3  24895  nmoleub2lem3  25048  minveclem3b  25361  minveclem4  25365  pmltpclem2  25383  ovolgelb  25414  ovolicc2lem2  25452  ovolicc2lem4  25454  mbfposr  25586  itg2const2  25675  itg2cnlem2  25696  itg2cn  25697  plyco0  26130  coeeulem  26162  dgradd2  26207  cxplt2  26640  fsumharmonic  26955  dmlogdmgm  26967  lgamgulmlem1  26972  lgamucov  26981  ftalem3  27018  ftalem5  27020  ftalem7  27022  ppiprm  27094  chtprm  27096  chpub  27164  perfectlem2  27174  bposlem1  27228  lgsdilem2  27277  lgsqrlem2  27291  lgsquadlem2  27325  2sqblem  27375  2sqmod  27380  2sqnn0  27382  pntpbnd1  27530  pntlem3  27553  nbusgrvtxm1  29359  crctcshwlkn0lem3  29792  frgrreggt1  30372  minvecolem4  30859  minvecolem5  30860  nndiffz1  32759  psgnfzto1stlem  33072  exsslsb  33585  lmdvg  33936  eulerpartlems  34344  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemrv2  34506  signsply0  34535  reprinfz1  34606  lpadmax  34666  lpadright  34668  0nn0m1nnn0  35093  erdszelem8  35178  bccolsum  35719  unbdqndv2lem1  36490  unbdqndv2lem2  36491  poimirlem2  37609  poimirlem3  37610  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem23  37630  poimirlem26  37633  poimirlem31  37638  poimir  37640  mblfinlem2  37645  itg2addnclem  37658  itg2addnclem2  37659  itg2addnclem3  37660  iblabsnclem  37670  ftc1anclem5  37684  areacirclem4  37698  areacirclem5  37699  areacirc  37700  cntotbnd  37783  aks4d1p5  42061  aks4d1p8d2  42066  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootlekpowne0  42086  hashnexinj  42109  sticksstones1  42127  sticksstones22  42149  unitscyglem2  42177  unitscyglem4  42179  infdesc  42624  elpell1qr2  42853  pellfundglb  42866  pellfund14gap  42868  congabseq  42956  jm2.19  42975  jm2.26lem3  42983  dgraa0p  43131  dvgrat  44294  uzwo4  45040  divlt0gt0d  45277  supxrgere  45322  uzublem  45419  nleltd  45441  supminfxr  45453  xrpnf  45474  sqrlearg  45544  lptre2pt  45631  limsupubuzlem  45703  climxrrelem  45740  climxlim2lem  45836  icccncfext  45878  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  volioore  45981  voliooico  45983  voliccico  45990  stoweidlem26  46017  stoweidlem34  46025  stoweidlem59  46050  stirlinglem5  46069  dirkercncflem1  46094  fourierdlem10  46108  fourierdlem19  46117  fourierdlem25  46123  fourierdlem35  46133  fourierdlem40  46138  fourierdlem42  46140  fourierdlem64  46161  fourierdlem65  46162  fourierdlem74  46171  fourierdlem75  46172  fourierdlem78  46175  fourierdlem79  46176  fourierdlem104  46201  fourierswlem  46221  fouriersw  46222  elaa2lem  46224  etransclem32  46257  etransclem41  46266  hsphoidmvle2  46576  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem2  46587  hoidmvlelem4  46589  hoidmvlelem5  46590  hoiqssbllem3  46615  hspmbllem1  46617  hspmbllem2  46618  vonicc  46676  pimdecfgtioo  46708  pimincfltioo  46709  et-sqrtnegnre  46864  fmtno4prmfac  47566  requad01  47615  requad1  47616  perfectALTVlem2  47716  itsclc0yqsol  48746  aacllem  49783