MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltnled Structured version   Visualization version   GIF version

Theorem ltnled 11303
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
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 ltnle 11235 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wcel 2107   class class class wbr 5106  cr 11051   < clt 11190  cle 11191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-cnv 5642  df-xr 11194  df-le 11196
This theorem is referenced by:  ltsub1  11652  ltsub2  11653  0mnnnnn0  12446  mul2lt0bi  13022  fzp1nel  13526  fzodisj  13607  elfznelfzob  13679  ccatsymb  14471  swrdnd  14543  cshwcsh2id  14718  01sqrexlem7  15134  sqrtlt  15147  lo1bdd2  15407  isercoll  15553  fprodntriv  15826  fzm1ndvds  16205  fzo0dvdseq  16206  bitsfzolem  16315  bitsfzo  16316  sadcaddlem  16338  smuval2  16363  bezoutlem3  16423  2mulprm  16570  isprm5  16584  odzdvds  16668  prm23ge5  16688  pc2dvds  16752  pockthg  16779  prmreclem1  16789  prmreclem5  16793  1arith  16800  4sqlem11  16828  vdwlem6  16859  vdwlem11  16864  ramlb  16892  oddvds  19330  gexdvds  19367  sylow1lem3  19383  zringlpirlem3  20888  coe1tmmul2  21650  iccntr  24187  icccmplem2  24189  reconnlem2  24193  evth  24325  lebnumlem3  24329  nmoleub2lem3  24481  minveclem3b  24795  minveclem4  24799  pmltpclem2  24816  ovolgelb  24847  ovolicc2lem2  24885  ovolicc2lem4  24887  mbfposr  25019  itg2const2  25109  itg2cnlem2  25130  itg2cn  25131  plyco0  25556  coeeulem  25588  dgradd2  25632  cxplt2  26056  fsumharmonic  26364  dmlogdmgm  26376  lgamgulmlem1  26381  lgamucov  26390  ftalem3  26427  ftalem5  26429  ftalem7  26431  ppiprm  26503  chtprm  26505  chpub  26571  perfectlem2  26581  bposlem1  26635  lgsdilem2  26684  lgsqrlem2  26698  lgsquadlem2  26732  2sqblem  26782  2sqmod  26787  2sqnn0  26789  pntpbnd1  26937  pntlem3  26960  nbusgrvtxm1  28330  crctcshwlkn0lem3  28760  frgrreggt1  29340  minvecolem4  29825  minvecolem5  29826  nndiffz1  31692  psgnfzto1stlem  31952  lmdvg  32537  eulerpartlems  32963  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemrv2  33124  signsply0  33166  reprinfz1  33238  lpadmax  33298  lpadright  33300  0nn0m1nnn0  33706  erdszelem8  33795  bccolsum  34315  unbdqndv2lem1  34975  unbdqndv2lem2  34976  poimirlem2  36083  poimirlem3  36084  poimirlem6  36087  poimirlem7  36088  poimirlem8  36089  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem21  36102  poimirlem22  36103  poimirlem23  36104  poimirlem26  36107  poimirlem31  36112  poimir  36114  mblfinlem2  36119  itg2addnclem  36132  itg2addnclem2  36133  itg2addnclem3  36134  iblabsnclem  36144  ftc1anclem5  36158  areacirclem4  36172  areacirclem5  36173  areacirc  36174  cntotbnd  36258  aks4d1p5  40540  aks4d1p8d2  40545  aks4d1p8  40547  aks4d1p9  40548  sticksstones1  40557  sticksstones22  40579  metakunt29  40608  metakunt30  40609  infdesc  40984  elpell1qr2  41198  pellfundglb  41211  pellfund14gap  41213  congabseq  41301  jm2.19  41320  jm2.26lem3  41328  dgraa0p  41479  dvgrat  42599  uzwo4  43268  divlt0gt0d  43527  supxrgere  43574  uzublem  43672  nleltd  43694  supminfxr  43706  xrpnf  43728  sqrlearg  43798  lptre2pt  43888  limsupubuzlem  43960  climxrrelem  43997  climxlim2lem  44093  icccncfext  44135  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  volioore  44238  voliooico  44240  voliccico  44247  stoweidlem26  44274  stoweidlem34  44282  stoweidlem59  44307  stirlinglem5  44326  dirkercncflem1  44351  fourierdlem10  44365  fourierdlem19  44374  fourierdlem25  44380  fourierdlem35  44390  fourierdlem40  44395  fourierdlem42  44397  fourierdlem64  44418  fourierdlem65  44419  fourierdlem74  44428  fourierdlem75  44429  fourierdlem78  44432  fourierdlem79  44433  fourierdlem104  44458  fourierswlem  44478  fouriersw  44479  elaa2lem  44481  etransclem32  44514  etransclem41  44523  hsphoidmvle2  44833  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmvlelem2  44844  hoidmvlelem4  44846  hoidmvlelem5  44847  hoiqssbllem3  44872  hspmbllem1  44874  hspmbllem2  44875  vonicc  44933  pimdecfgtioo  44965  pimincfltioo  44966  et-sqrtnegnre  45121  fmtno4prmfac  45771  requad01  45820  requad1  45821  perfectALTVlem2  45921  itsclc0yqsol  46857  aacllem  47255
  Copyright terms: Public domain W3C validator