Theorem ltnled 10944

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2112   class class class wbr 5039  ℝcr 10693   < clt 10832   ≤ cle 10833

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 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-xr 10836  df-le 10838

This theorem is referenced by:  ltsub1  11293  ltsub2  11294  0mnnnnn0  12087  mul2lt0bi  12657  fzp1nel  13161  fzodisj  13241  elfznelfzob  13313  ccatsymb  14104  swrdnd  14184  cshwcsh2id  14358  sqrlem7  14777  sqrtlt  14790  lo1bdd2  15050  isercoll  15196  fprodntriv  15467  fzm1ndvds  15846  fzo0dvdseq  15847  bitsfzolem  15956  bitsfzo  15957  sadcaddlem  15979  smuval2  16004  bezoutlem3  16064  2mulprm  16213  isprm5  16227  odzdvds  16311  prm23ge5  16331  pc2dvds  16395  pockthg  16422  prmreclem1  16432  prmreclem5  16436  1arith  16443  4sqlem11  16471  vdwlem6  16502  vdwlem11  16507  ramlb  16535  oddvds  18893  gexdvds  18927  sylow1lem3  18943  zringlpirlem3  20405  coe1tmmul2  21151  iccntr  23672  icccmplem2  23674  reconnlem2  23678  evth  23810  lebnumlem3  23814  nmoleub2lem3  23966  minveclem3b  24279  minveclem4  24283  pmltpclem2  24300  ovolgelb  24331  ovolicc2lem2  24369  ovolicc2lem4  24371  mbfposr  24503  itg2const2  24593  itg2cnlem2  24614  itg2cn  24615  plyco0  25040  coeeulem  25072  dgradd2  25116  cxplt2  25540  fsumharmonic  25848  dmlogdmgm  25860  lgamgulmlem1  25865  lgamucov  25874  ftalem3  25911  ftalem5  25913  ftalem7  25915  ppiprm  25987  chtprm  25989  chpub  26055  perfectlem2  26065  bposlem1  26119  lgsdilem2  26168  lgsqrlem2  26182  lgsquadlem2  26216  2sqblem  26266  2sqmod  26271  2sqnn0  26273  pntpbnd1  26421  pntlem3  26444  nbusgrvtxm1  27421  crctcshwlkn0lem3  27850  frgrreggt1  28430  minvecolem4  28915  minvecolem5  28916  nndiffz1  30781  psgnfzto1stlem  31040  lmdvg  31571  eulerpartlems  31993  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemrv2  32154  signsply0  32196  reprinfz1  32268  lpadmax  32328  lpadright  32330  0nn0m1nnn0  32738  erdszelem8  32827  bccolsum  33374  unbdqndv2lem1  34375  unbdqndv2lem2  34376  poimirlem2  35465  poimirlem3  35466  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem26  35489  poimirlem31  35494  poimir  35496  mblfinlem2  35501  itg2addnclem  35514  itg2addnclem2  35515  itg2addnclem3  35516  iblabsnclem  35526  ftc1anclem5  35540  areacirclem4  35554  areacirclem5  35555  areacirc  35556  cntotbnd  35640  sticksstones1  39771  metakunt29  39816  metakunt30  39817  infdesc  40124  elpell1qr2  40338  pellfundglb  40351  pellfund14gap  40353  congabseq  40440  jm2.19  40459  jm2.26lem3  40467  dgraa0p  40618  dvgrat  41544  uzwo4  42215  divlt0gt0d  42438  supxrgere  42486  uzublem  42584  nleltd  42608  supminfxr  42620  xrpnf  42642  sqrlearg  42707  lptre2pt  42799  limsupubuzlem  42871  climxrrelem  42908  climxlim2lem  43004  icccncfext  43046  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  volioore  43149  voliooico  43151  voliccico  43158  stoweidlem26  43185  stoweidlem34  43193  stoweidlem59  43218  stirlinglem5  43237  dirkercncflem1  43262  fourierdlem10  43276  fourierdlem19  43285  fourierdlem25  43291  fourierdlem35  43301  fourierdlem40  43306  fourierdlem42  43308  fourierdlem64  43329  fourierdlem65  43330  fourierdlem74  43339  fourierdlem75  43340  fourierdlem78  43343  fourierdlem79  43344  fourierdlem104  43369  fourierswlem  43389  fouriersw  43390  elaa2lem  43392  etransclem32  43425  etransclem41  43434  hsphoidmvle2  43741  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmv1lelem3  43749  hoidmvlelem2  43752  hoidmvlelem4  43754  hoidmvlelem5  43755  hoiqssbllem3  43780  hspmbllem1  43782  hspmbllem2  43783  vonicc  43841  pimdecfgtioo  43869  pimincfltioo  43870  fmtno4prmfac  44640  requad01  44689  requad1  44690  perfectALTVlem2  44790  itsclc0yqsol  45726  aacllem  46119