Theorem ltnled 11278

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-xr 11168  df-le 11170

This theorem is referenced by:  ltsub1  11631  ltsub2  11632  0mnnnnn0  12431  mul2lt0bi  13011  fzp1nel  13525  fzodisj  13607  elfznelfzob  13688  ccatsymb  14504  swrdnd  14576  cshwcsh2id  14749  01sqrexlem7  15169  sqrtlt  15182  lo1bdd2  15445  isercoll  15589  fprodntriv  15863  fzm1ndvds  16247  fzo0dvdseq  16248  bitsfzolem  16359  bitsfzo  16360  sadcaddlem  16382  smuval2  16407  bezoutlem3  16466  2mulprm  16618  isprm5  16632  odzdvds  16721  prm23ge5  16741  pc2dvds  16805  pockthg  16832  prmreclem1  16842  prmreclem5  16846  1arith  16853  4sqlem11  16881  vdwlem6  16912  vdwlem11  16917  ramlb  16945  oddvds  19474  gexdvds  19511  sylow1lem3  19527  zringlpirlem3  21417  psdmul  22107  coe1tmmul2  22216  iccntr  24764  icccmplem2  24766  reconnlem2  24770  evth  24912  lebnumlem3  24916  nmoleub2lem3  25069  minveclem3b  25382  minveclem4  25386  pmltpclem2  25404  ovolgelb  25435  ovolicc2lem2  25473  ovolicc2lem4  25475  mbfposr  25607  itg2const2  25696  itg2cnlem2  25717  itg2cn  25718  plyco0  26151  coeeulem  26183  dgradd2  26228  cxplt2  26661  fsumharmonic  26976  dmlogdmgm  26988  lgamgulmlem1  26993  lgamucov  27002  ftalem3  27039  ftalem5  27041  ftalem7  27043  ppiprm  27115  chtprm  27117  chpub  27185  perfectlem2  27195  bposlem1  27249  lgsdilem2  27298  lgsqrlem2  27312  lgsquadlem2  27346  2sqblem  27396  2sqmod  27401  2sqnn0  27403  pntpbnd1  27551  pntlem3  27574  nbusgrvtxm1  29401  crctcshwlkn0lem3  29834  frgrreggt1  30417  minvecolem4  30904  minvecolem5  30905  nndiffz1  32815  psgnfzto1stlem  33131  exsslsb  33702  lmdvg  34059  eulerpartlems  34466  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemrv2  34628  signsply0  34657  reprinfz1  34728  lpadmax  34788  lpadright  34790  0nn0m1nnn0  35256  erdszelem8  35341  bccolsum  35882  unbdqndv2lem1  36652  unbdqndv2lem2  36653  poimirlem2  37762  poimirlem3  37763  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem23  37783  poimirlem26  37786  poimirlem31  37791  poimir  37793  mblfinlem2  37798  itg2addnclem  37811  itg2addnclem2  37812  itg2addnclem3  37813  iblabsnclem  37823  ftc1anclem5  37837  areacirclem4  37851  areacirclem5  37852  areacirc  37853  cntotbnd  37936  aks4d1p5  42273  aks4d1p8d2  42278  aks4d1p8  42280  aks4d1p9  42281  posbezout  42293  primrootlekpowne0  42298  hashnexinj  42321  sticksstones1  42339  sticksstones22  42361  unitscyglem2  42389  unitscyglem4  42391  infdesc  42828  elpell1qr2  43056  pellfundglb  43069  pellfund14gap  43071  congabseq  43158  jm2.19  43177  jm2.26lem3  43185  dgraa0p  43333  dvgrat  44495  uzwo4  45240  divlt0gt0d  45476  supxrgere  45520  uzublem  45616  nleltd  45638  supminfxr  45650  xrpnf  45671  sqrlearg  45741  lptre2pt  45826  limsupubuzlem  45898  climxrrelem  45935  climxlim2lem  46031  icccncfext  46073  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  volioore  46176  voliooico  46178  voliccico  46185  stoweidlem26  46212  stoweidlem34  46220  stoweidlem59  46245  stirlinglem5  46264  dirkercncflem1  46289  fourierdlem10  46303  fourierdlem19  46312  fourierdlem25  46318  fourierdlem35  46328  fourierdlem40  46333  fourierdlem42  46335  fourierdlem64  46356  fourierdlem65  46357  fourierdlem74  46366  fourierdlem75  46367  fourierdlem78  46370  fourierdlem79  46371  fourierdlem104  46396  fourierswlem  46416  fouriersw  46417  elaa2lem  46419  etransclem32  46452  etransclem41  46461  hsphoidmvle2  46771  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmvlelem2  46782  hoidmvlelem4  46784  hoidmvlelem5  46785  hoiqssbllem3  46810  hspmbllem1  46812  hspmbllem2  46813  vonicc  46871  pimdecfgtioo  46903  pimincfltioo  46904  et-sqrtnegnre  47059  fmtno4prmfac  47760  requad01  47809  requad1  47810  perfectALTVlem2  47910  itsclc0yqsol  48952  aacllem  49988