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

Theorem ltnle 11235
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 11234 . . 3 ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
21ancoms 460 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵𝐴 ↔ ¬ 𝐴 < 𝐵))
32con2bid 355 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  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:  letric  11256  ltnled  11303  leaddsub  11632  mulge0b  12026  nnnle0  12187  nn0n0n1ge2b  12482  znnnlt1  12531  uzwo  12837  qsqueeze  13121  difreicc  13402  fzp1disj  13501  fzneuz  13523  fznuz  13524  uznfz  13525  difelfznle  13556  nelfzo  13578  ssfzoulel  13667  elfzonelfzo  13675  modfzo0difsn  13849  ssnn0fi  13891  discr1  14143  bcval5  14219  swrdnd  14543  swrdnnn0nd  14545  swrdnd0  14546  swrdsbslen  14553  swrdspsleq  14554  pfxnd0  14577  pfxccat3  14623  swrdccat  14624  pfxccat3a  14627  repswswrd  14673  cnpart  15126  absmax  15215  rlimrege0  15462  rpnnen2lem12  16108  alzdvds  16203  algcvgblem  16454  prmndvdsfaclt  16602  pcprendvds  16713  pcdvdsb  16742  pcmpt  16765  prmunb  16787  prmreclem2  16790  prmgaplem5  16928  prmgaplem6  16929  prmlem1  16981  prmlem2  16993  lt6abl  19673  metdseq0  24220  xrhmeo  24312  ovolicc2lem3  24886  itg2seq  25110  dvne0  25378  coeeulem  25588  radcnvlt1  25780  argimgt0  25970  cxple2  26055  ressatans  26287  eldmgm  26374  basellem2  26434  issqf  26488  bpos1  26634  bposlem3  26637  bposlem6  26640  2sqreulem1  26797  2sqreunnlem1  26800  pntpbnd2  26938  ostth2lem4  26987  crctcshwlkn0  28769  crctcsh  28772  eucrctshift  29190  ltflcei  36069  poimirlem4  36085  poimirlem13  36094  poimirlem14  36095  poimirlem15  36096  poimirlem31  36112  mblfinlem1  36118  mbfposadd  36128  itgaddnclem2  36140  ftc1anclem1  36154  ftc1anclem5  36158  dvasin  36165  reabsifnpos  41912  reabsifnneg  41914  icccncfext  44135  stoweidlem14  44262  stoweidlem34  44282  ltnltne  45538  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  ply1mulgsumlem2  46475
  Copyright terms: Public domain W3C validator