Theorem ltnled 11052

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-xr 10944  df-le 10946

This theorem is referenced by:  ltsub1  11401  ltsub2  11402  0mnnnnn0  12195  mul2lt0bi  12765  fzp1nel  13269  fzodisj  13349  elfznelfzob  13421  ccatsymb  14215  swrdnd  14295  cshwcsh2id  14469  sqrlem7  14888  sqrtlt  14901  lo1bdd2  15161  isercoll  15307  fprodntriv  15580  fzm1ndvds  15959  fzo0dvdseq  15960  bitsfzolem  16069  bitsfzo  16070  sadcaddlem  16092  smuval2  16117  bezoutlem3  16177  2mulprm  16326  isprm5  16340  odzdvds  16424  prm23ge5  16444  pc2dvds  16508  pockthg  16535  prmreclem1  16545  prmreclem5  16549  1arith  16556  4sqlem11  16584  vdwlem6  16615  vdwlem11  16620  ramlb  16648  oddvds  19070  gexdvds  19104  sylow1lem3  19120  zringlpirlem3  20598  coe1tmmul2  21357  iccntr  23890  icccmplem2  23892  reconnlem2  23896  evth  24028  lebnumlem3  24032  nmoleub2lem3  24184  minveclem3b  24497  minveclem4  24501  pmltpclem2  24518  ovolgelb  24549  ovolicc2lem2  24587  ovolicc2lem4  24589  mbfposr  24721  itg2const2  24811  itg2cnlem2  24832  itg2cn  24833  plyco0  25258  coeeulem  25290  dgradd2  25334  cxplt2  25758  fsumharmonic  26066  dmlogdmgm  26078  lgamgulmlem1  26083  lgamucov  26092  ftalem3  26129  ftalem5  26131  ftalem7  26133  ppiprm  26205  chtprm  26207  chpub  26273  perfectlem2  26283  bposlem1  26337  lgsdilem2  26386  lgsqrlem2  26400  lgsquadlem2  26434  2sqblem  26484  2sqmod  26489  2sqnn0  26491  pntpbnd1  26639  pntlem3  26662  nbusgrvtxm1  27649  crctcshwlkn0lem3  28078  frgrreggt1  28658  minvecolem4  29143  minvecolem5  29144  nndiffz1  31009  psgnfzto1stlem  31269  lmdvg  31805  eulerpartlems  32227  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemrv2  32388  signsply0  32430  reprinfz1  32502  lpadmax  32562  lpadright  32564  0nn0m1nnn0  32971  erdszelem8  33060  bccolsum  33611  unbdqndv2lem1  34616  unbdqndv2lem2  34617  poimirlem2  35706  poimirlem3  35707  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem26  35730  poimirlem31  35735  poimir  35737  mblfinlem2  35742  itg2addnclem  35755  itg2addnclem2  35756  itg2addnclem3  35757  iblabsnclem  35767  ftc1anclem5  35781  areacirclem4  35795  areacirclem5  35796  areacirc  35797  cntotbnd  35881  aks4d1p5  40016  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  sticksstones1  40030  sticksstones22  40052  metakunt29  40081  metakunt30  40082  infdesc  40396  elpell1qr2  40610  pellfundglb  40623  pellfund14gap  40625  congabseq  40712  jm2.19  40731  jm2.26lem3  40739  dgraa0p  40890  dvgrat  41819  uzwo4  42490  divlt0gt0d  42714  supxrgere  42762  uzublem  42860  nleltd  42882  supminfxr  42894  xrpnf  42916  sqrlearg  42981  lptre2pt  43071  limsupubuzlem  43143  climxrrelem  43180  climxlim2lem  43276  icccncfext  43318  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  volioore  43421  voliooico  43423  voliccico  43430  stoweidlem26  43457  stoweidlem34  43465  stoweidlem59  43490  stirlinglem5  43509  dirkercncflem1  43534  fourierdlem10  43548  fourierdlem19  43557  fourierdlem25  43563  fourierdlem35  43573  fourierdlem40  43578  fourierdlem42  43580  fourierdlem64  43601  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem104  43641  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  etransclem32  43697  etransclem41  43706  hsphoidmvle2  44013  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem2  44024  hoidmvlelem4  44026  hoidmvlelem5  44027  hoiqssbllem3  44052  hspmbllem1  44054  hspmbllem2  44055  vonicc  44113  pimdecfgtioo  44141  pimincfltioo  44142  fmtno4prmfac  44912  requad01  44961  requad1  44962  perfectALTVlem2  45062  itsclc0yqsol  45998  aacllem  46391