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

Theorem ltnle 11192
Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
Assertion
Ref Expression
ltnle ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ltnle
StepHypRef Expression
1 lenlt 11191 . . 3 ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
21ancoms 459 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
32con2bid 354 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wcel 2106   class class class wbr 5103  cr 11008   < clt 11147  cle 11148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-xp 5637  df-cnv 5639  df-xr 11151  df-le 11153
This theorem is referenced by:  letric  11213  ltnled  11260  leaddsub  11589  mulge0b  11983  nnnle0  12144  nn0n0n1ge2b  12439  znnnlt1  12488  uzwo  12790  qsqueeze  13074  difreicc  13355  fzp1disj  13454  fzneuz  13476  fznuz  13477  uznfz  13478  difelfznle  13509  nelfzo  13531  ssfzoulel  13620  elfzonelfzo  13628  modfzo0difsn  13802  ssnn0fi  13844  discr1  14096  bcval5  14172  swrdnd  14500  swrdnnn0nd  14502  swrdnd0  14503  swrdsbslen  14510  swrdspsleq  14511  pfxnd0  14534  pfxccat3  14580  swrdccat  14581  pfxccat3a  14584  repswswrd  14630  cnpart  15085  absmax  15174  rlimrege0  15421  rpnnen2lem12  16067  alzdvds  16162  algcvgblem  16413  prmndvdsfaclt  16561  pcprendvds  16672  pcdvdsb  16701  pcmpt  16724  prmunb  16746  prmreclem2  16749  prmgaplem5  16887  prmgaplem6  16888  prmlem1  16940  prmlem2  16952  lt6abl  19631  metdseq0  24169  xrhmeo  24261  ovolicc2lem3  24835  itg2seq  25059  dvne0  25327  coeeulem  25537  radcnvlt1  25729  argimgt0  25919  cxple2  26004  ressatans  26236  eldmgm  26323  basellem2  26383  issqf  26437  bpos1  26583  bposlem3  26586  bposlem6  26589  2sqreulem1  26746  2sqreunnlem1  26749  pntpbnd2  26887  ostth2lem4  26936  crctcshwlkn0  28595  crctcsh  28598  eucrctshift  29016  ltflcei  36004  poimirlem4  36020  poimirlem13  36029  poimirlem14  36030  poimirlem15  36031  poimirlem31  36047  mblfinlem1  36053  mbfposadd  36063  itgaddnclem2  36075  ftc1anclem1  36089  ftc1anclem5  36093  dvasin  36100  reabsifnpos  41816  reabsifnneg  41818  icccncfext  44029  stoweidlem14  44156  stoweidlem34  44176  ltnltne  45432  nnsum4primeseven  45893  nnsum4primesevenALTV  45894  ply1mulgsumlem2  46369
  Copyright terms: Public domain W3C validator