Theorem ltnled 11284

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-xr 11174  df-le 11176

This theorem is referenced by:  ltsub1  11637  ltsub2  11638  0mnnnnn0  12460  mul2lt0bi  13041  fzp1nel  13556  fzodisj  13639  elfznelfzob  13720  ccatsymb  14536  swrdnd  14608  cshwcsh2id  14781  01sqrexlem7  15201  sqrtlt  15214  lo1bdd2  15477  isercoll  15621  fprodntriv  15898  fzm1ndvds  16282  fzo0dvdseq  16283  bitsfzolem  16394  bitsfzo  16395  sadcaddlem  16417  smuval2  16442  bezoutlem3  16501  2mulprm  16653  isprm5  16668  odzdvds  16757  prm23ge5  16777  pc2dvds  16841  pockthg  16868  prmreclem1  16878  prmreclem5  16882  1arith  16889  4sqlem11  16917  vdwlem6  16948  vdwlem11  16953  ramlb  16981  oddvds  19513  gexdvds  19550  sylow1lem3  19566  zringlpirlem3  21439  psdmul  22154  coe1tmmul2  22262  iccntr  24805  icccmplem2  24807  reconnlem2  24811  evth  24944  lebnumlem3  24948  nmoleub2lem3  25100  minveclem3b  25413  minveclem4  25417  pmltpclem2  25434  ovolgelb  25465  ovolicc2lem2  25503  ovolicc2lem4  25505  mbfposr  25637  itg2const2  25726  itg2cnlem2  25747  itg2cn  25748  plyco0  26175  coeeulem  26207  dgradd2  26251  cxplt2  26680  fsumharmonic  26993  dmlogdmgm  27005  lgamgulmlem1  27010  lgamucov  27019  ftalem3  27056  ftalem5  27058  ftalem7  27060  ppiprm  27132  chtprm  27134  chpub  27201  perfectlem2  27211  bposlem1  27265  lgsdilem2  27314  lgsqrlem2  27328  lgsquadlem2  27362  2sqblem  27412  2sqmod  27417  2sqnn0  27419  pntpbnd1  27567  pntlem3  27590  nbusgrvtxm1  29466  crctcshwlkn0lem3  29898  frgrreggt1  30481  minvecolem4  30969  minvecolem5  30970  nndiffz1  32878  psgnfzto1stlem  33181  exsslsb  33781  lmdvg  34137  eulerpartlems  34544  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemrv2  34706  signsply0  34735  reprinfz1  34806  lpadmax  34866  lpadright  34868  0nn0m1nnn0  35341  erdszelem8  35426  bccolsum  35967  unbdqndv2lem1  36815  unbdqndv2lem2  36816  poimirlem2  37989  poimirlem3  37990  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem23  38010  poimirlem26  38013  poimirlem31  38018  poimir  38020  mblfinlem2  38025  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  iblabsnclem  38050  ftc1anclem5  38064  areacirclem4  38078  areacirclem5  38079  areacirc  38080  cntotbnd  38163  aks4d1p5  42565  aks4d1p8d2  42570  aks4d1p8  42572  aks4d1p9  42573  posbezout  42585  primrootlekpowne0  42590  hashnexinj  42613  sticksstones1  42631  sticksstones22  42653  unitscyglem2  42681  unitscyglem4  42683  infdesc  43093  elpell1qr2  43317  pellfundglb  43330  pellfund14gap  43332  congabseq  43419  jm2.19  43438  jm2.26lem3  43446  dgraa0p  43594  dvgrat  44756  uzwo4  45501  divlt0gt0d  45734  supxrgere  45778  uzublem  45873  nleltd  45895  supminfxr  45907  xrpnf  45928  sqrlearg  45998  lptre2pt  46083  limsupubuzlem  46155  climxrrelem  46192  climxlim2lem  46288  icccncfext  46330  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  volioore  46433  voliooico  46435  voliccico  46442  stoweidlem26  46469  stoweidlem34  46477  stoweidlem59  46502  stirlinglem5  46521  dirkercncflem1  46546  fourierdlem10  46560  fourierdlem19  46569  fourierdlem25  46575  fourierdlem35  46585  fourierdlem40  46590  fourierdlem42  46592  fourierdlem64  46613  fourierdlem65  46614  fourierdlem74  46623  fourierdlem75  46624  fourierdlem78  46627  fourierdlem79  46628  fourierdlem104  46653  fourierswlem  46673  fouriersw  46674  elaa2lem  46676  etransclem32  46709  etransclem41  46718  hsphoidmvle2  47028  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmvlelem2  47039  hoidmvlelem4  47041  hoidmvlelem5  47042  hoiqssbllem3  47067  hspmbllem1  47069  hspmbllem2  47070  vonicc  47128  pimdecfgtioo  47160  pimincfltioo  47161  et-sqrtnegnre  47316  fmtno4prmfac  48050  requad01  48112  requad1  48113  perfectALTVlem2  48213  itsclc0yqsol  49255  aacllem  50291