Theorem ltnle 11054

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

Step	Hyp	Ref	Expression
1		lenlt 11053	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 459	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 355	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870   < clt 11009   ≤ cle 11010

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-xr 11013  df-le 11015

This theorem is referenced by:  letric  11075  ltnled  11122  leaddsub  11451  mulge0b  11845  nnnle0  12006  nn0n0n1ge2b  12301  znnnlt1  12347  uzwo  12651  qsqueeze  12935  difreicc  13216  fzp1disj  13315  fzneuz  13337  fznuz  13338  uznfz  13339  difelfznle  13370  nelfzo  13392  ssfzoulel  13481  elfzonelfzo  13489  modfzo0difsn  13663  ssnn0fi  13705  discr1  13954  bcval5  14032  swrdnd  14367  swrdnnn0nd  14369  swrdnd0  14370  swrdsbslen  14377  swrdspsleq  14378  pfxnd0  14401  pfxccat3  14447  swrdccat  14448  pfxccat3a  14451  repswswrd  14497  cnpart  14951  absmax  15041  rlimrege0  15288  rpnnen2lem12  15934  alzdvds  16029  algcvgblem  16282  prmndvdsfaclt  16430  pcprendvds  16541  pcdvdsb  16570  pcmpt  16593  prmunb  16615  prmreclem2  16618  prmgaplem5  16756  prmgaplem6  16757  prmlem1  16809  prmlem2  16821  lt6abl  19496  metdseq0  24017  xrhmeo  24109  ovolicc2lem3  24683  itg2seq  24907  dvne0  25175  coeeulem  25385  radcnvlt1  25577  argimgt0  25767  cxple2  25852  ressatans  26084  eldmgm  26171  basellem2  26231  issqf  26285  bpos1  26431  bposlem3  26434  bposlem6  26437  2sqreulem1  26594  2sqreunnlem1  26597  pntpbnd2  26735  ostth2lem4  26784  crctcshwlkn0  28186  crctcsh  28189  eucrctshift  28607  ltflcei  35765  poimirlem4  35781  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem31  35808  mblfinlem1  35814  mbfposadd  35824  itgaddnclem2  35836  ftc1anclem1  35850  ftc1anclem5  35854  dvasin  35861  reabsifnpos  41241  reabsifnneg  41243  icccncfext  43428  stoweidlem14  43555  stoweidlem34  43575  ltnltne  44791  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  ply1mulgsumlem2  45728