Theorem ltnled 11380

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   < clt 11267   ≤ cle 11268

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-xr 11271  df-le 11273

This theorem is referenced by:  ltsub1  11731  ltsub2  11732  0mnnnnn0  12531  mul2lt0bi  13113  fzp1nel  13626  fzodisj  13708  elfznelfzob  13787  ccatsymb  14598  swrdnd  14670  cshwcsh2id  14845  01sqrexlem7  15265  sqrtlt  15278  lo1bdd2  15538  isercoll  15682  fprodntriv  15956  fzm1ndvds  16339  fzo0dvdseq  16340  bitsfzolem  16451  bitsfzo  16452  sadcaddlem  16474  smuval2  16499  bezoutlem3  16558  2mulprm  16710  isprm5  16724  odzdvds  16813  prm23ge5  16833  pc2dvds  16897  pockthg  16924  prmreclem1  16934  prmreclem5  16938  1arith  16945  4sqlem11  16973  vdwlem6  17004  vdwlem11  17009  ramlb  17037  oddvds  19526  gexdvds  19563  sylow1lem3  19579  zringlpirlem3  21423  psdmul  22102  coe1tmmul2  22211  iccntr  24759  icccmplem2  24761  reconnlem2  24765  evth  24907  lebnumlem3  24911  nmoleub2lem3  25064  minveclem3b  25378  minveclem4  25382  pmltpclem2  25400  ovolgelb  25431  ovolicc2lem2  25469  ovolicc2lem4  25471  mbfposr  25603  itg2const2  25692  itg2cnlem2  25713  itg2cn  25714  plyco0  26147  coeeulem  26179  dgradd2  26224  cxplt2  26657  fsumharmonic  26972  dmlogdmgm  26984  lgamgulmlem1  26989  lgamucov  26998  ftalem3  27035  ftalem5  27037  ftalem7  27039  ppiprm  27111  chtprm  27113  chpub  27181  perfectlem2  27191  bposlem1  27245  lgsdilem2  27294  lgsqrlem2  27308  lgsquadlem2  27342  2sqblem  27392  2sqmod  27397  2sqnn0  27399  pntpbnd1  27547  pntlem3  27570  nbusgrvtxm1  29304  crctcshwlkn0lem3  29740  frgrreggt1  30320  minvecolem4  30807  minvecolem5  30808  nndiffz1  32709  psgnfzto1stlem  33057  exsslsb  33582  lmdvg  33930  eulerpartlems  34338  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemrv2  34500  signsply0  34529  reprinfz1  34600  lpadmax  34660  lpadright  34662  0nn0m1nnn0  35081  erdszelem8  35166  bccolsum  35702  unbdqndv2lem1  36473  unbdqndv2lem2  36474  poimirlem2  37592  poimirlem3  37593  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem26  37616  poimirlem31  37621  poimir  37623  mblfinlem2  37628  itg2addnclem  37641  itg2addnclem2  37642  itg2addnclem3  37643  iblabsnclem  37653  ftc1anclem5  37667  areacirclem4  37681  areacirclem5  37682  areacirc  37683  cntotbnd  37766  aks4d1p5  42039  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1p9  42047  posbezout  42059  primrootlekpowne0  42064  hashnexinj  42087  sticksstones1  42105  sticksstones22  42127  unitscyglem2  42155  unitscyglem4  42157  metakunt29  42192  metakunt30  42193  infdesc  42613  elpell1qr2  42842  pellfundglb  42855  pellfund14gap  42857  congabseq  42945  jm2.19  42964  jm2.26lem3  42972  dgraa0p  43120  dvgrat  44284  uzwo4  45025  divlt0gt0d  45263  supxrgere  45308  uzublem  45405  nleltd  45427  supminfxr  45439  xrpnf  45460  sqrlearg  45530  lptre2pt  45617  limsupubuzlem  45689  climxrrelem  45726  climxlim2lem  45822  icccncfext  45864  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  volioore  45967  voliooico  45969  voliccico  45976  stoweidlem26  46003  stoweidlem34  46011  stoweidlem59  46036  stirlinglem5  46055  dirkercncflem1  46080  fourierdlem10  46094  fourierdlem19  46103  fourierdlem25  46109  fourierdlem35  46119  fourierdlem40  46124  fourierdlem42  46126  fourierdlem64  46147  fourierdlem65  46148  fourierdlem74  46157  fourierdlem75  46158  fourierdlem78  46161  fourierdlem79  46162  fourierdlem104  46187  fourierswlem  46207  fouriersw  46208  elaa2lem  46210  etransclem32  46243  etransclem41  46252  hsphoidmvle2  46562  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmvlelem2  46573  hoidmvlelem4  46575  hoidmvlelem5  46576  hoiqssbllem3  46601  hspmbllem1  46603  hspmbllem2  46604  vonicc  46662  pimdecfgtioo  46694  pimincfltioo  46695  et-sqrtnegnre  46850  fmtno4prmfac  47534  requad01  47583  requad1  47584  perfectALTVlem2  47684  itsclc0yqsol  48692  aacllem  49613