Theorem ltnled 11352

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-xr 11242  df-le 11244

This theorem is referenced by:  ltsub1  11705  ltsub2  11706  0mnnnnn0  12531  mul2lt0bi  13119  fzp1nel  13635  fzodisj  13718  elfznelfzob  13799  ccatsymb  14616  swrdnd  14688  cshwcsh2id  14861  01sqrexlem7  15295  sqrtlt  15308  lo1bdd2  15571  isercoll  15715  fprodntriv  15992  fzm1ndvds  16375  fzo0dvdseq  16376  bitsfzolem  16487  bitsfzo  16488  sadcaddlem  16510  smuval2  16535  bezoutlem3  16594  2mulprm  16746  isprm5  16761  odzdvds  16850  prm23ge5  16870  pc2dvds  16934  pockthg  16961  prmreclem1  16971  prmreclem5  16975  1arith  16982  4sqlem11  17010  vdwlem6  17041  vdwlem11  17046  ramlb  17074  oddvds  19612  gexdvds  19649  sylow1lem3  19665  zringlpirlem3  21614  psdmul  22329  coe1tmmul2  22437  iccntr  24979  icccmplem2  24981  reconnlem2  24985  evth  25118  lebnumlem3  25122  nmoleub2lem3  25274  minveclem3b  25587  minveclem4  25591  pmltpclem2  25608  ovolgelb  25639  ovolicc2lem2  25677  ovolicc2lem4  25679  mbfposr  25811  itg2const2  25900  itg2cnlem2  25921  itg2cn  25922  plyco0  26349  coeeulem  26381  dgradd2  26425  cxplt2  26863  fsumharmonic  27176  dmlogdmgm  27188  lgamgulmlem1  27193  lgamucov  27202  ftalem3  27239  ftalem5  27241  ftalem7  27243  ppiprm  27315  chtprm  27317  chpub  27384  perfectlem2  27394  bposlem1  27448  lgsdilem2  27497  lgsqrlem2  27511  lgsquadlem2  27545  2sqblem  27595  2sqmod  27600  2sqnn0  27602  pntpbnd1  27750  pntlem3  27773  nbusgrvtxm1  29729  crctcshwlkn0lem3  30161  frgrreggt1  30744  minvecolem4  31232  minvecolem5  31233  nndiffz1  33131  psgnfzto1stlem  33420  exsslsb  33987  lmdvg  34343  eulerpartlems  34750  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemrv2  34912  signsply0  34938  reprinfz1  35009  lpadmax  35072  lpadright  35074  0nn0m1nnn0  35604  erdszelem8  35690  bccolsum  36231  unbdqndv2lem1  37098  unbdqndv2lem2  37099  poimirlem2  38273  poimirlem3  38274  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem23  38294  poimirlem26  38297  poimirlem31  38302  poimir  38304  mblfinlem2  38309  itg2addnclem  38322  itg2addnclem2  38323  itg2addnclem3  38324  iblabsnclem  38334  ftc1anclem5  38348  areacirclem4  38362  areacirclem5  38363  areacirc  38364  cntotbnd  38447  aks4d1p5  42847  aks4d1p8d2  42852  aks4d1p8  42854  aks4d1p9  42855  posbezout  42867  primrootlekpowne0  42872  hashnexinj  42895  sticksstones1  42913  sticksstones22  42935  unitscyglem2  42963  unitscyglem4  42965  infdesc  43375  elpell1qr2  43599  pellfundglb  43612  pellfund14gap  43614  congabseq  43701  jm2.19  43720  jm2.26lem3  43728  dgraa0p  43876  dvgrat  45022  uzwo4  45773  divlt0gt0d  46005  supxrgere  46049  uzublem  46144  nleltd  46166  supminfxr  46178  xrpnf  46199  sqrlearg  46269  lptre2pt  46354  limsupubuzlem  46426  climxrrelem  46463  climxlim2lem  46559  icccncfext  46601  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  volioore  46704  voliooico  46706  voliccico  46713  stoweidlem26  46740  stoweidlem34  46748  stoweidlem59  46773  stirlinglem5  46792  dirkercncflem1  46817  fourierdlem10  46831  fourierdlem19  46840  fourierdlem25  46846  fourierdlem35  46856  fourierdlem40  46861  fourierdlem42  46863  fourierdlem64  46884  fourierdlem65  46885  fourierdlem74  46894  fourierdlem75  46895  fourierdlem78  46898  fourierdlem79  46899  fourierdlem104  46924  fourierswlem  46944  fouriersw  46945  elaa2lem  46947  etransclem32  46980  etransclem41  46989  hsphoidmvle2  47299  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmvlelem2  47310  hoidmvlelem4  47312  hoidmvlelem5  47313  hoiqssbllem3  47338  hspmbllem1  47340  hspmbllem2  47341  vonicc  47399  pimdecfgtioo  47431  pimincfltioo  47432  et-sqrtnegnre  47587  fmtno4prmfac  48324  requad01  48386  requad1  48387  perfectALTVlem2  48487  itsclc0yqsol  49544  aacllem  50621