Theorem ltnle 11288

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 11287	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 463	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 357	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   class class class wbr 5113  ℝcr 11098   < clt 11242   ≤ cle 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-xr 11246  df-le 11248

This theorem is referenced by:  letric  11309  ltnled  11356  leaddsub  11689  mulge0b  12084  nnnle0  12268  nn0n0n1ge2b  12572  znnnlt1  12620  uzwo  12934  qsqueeze  13226  difreicc  13510  fzp1disj  13610  fzneuz  13635  fznuz  13636  uznfz  13637  difelfznle  13669  nelfzo  13692  ssfzoulel  13788  elfzonelfzo  13797  modfzo0difsn  13978  ssnn0fi  14020  discr1  14274  bcval5  14353  swrdnd  14691  swrdnnn0nd  14693  swrdnd0  14694  swrdsbslen  14701  swrdspsleq  14702  pfxnd0  14725  pfxccat3  14770  swrdccat  14771  pfxccat3a  14774  repswswrd  14820  cnpart  15290  absmax  15380  rlimrege0  15629  rpnnen2lem12  16280  alzdvds  16377  algcvgblem  16634  prmndvdsfaclt  16783  pcprendvds  16899  pcdvdsb  16928  pcmpt  16951  prmunb  16973  prmreclem2  16976  prmgaplem5  17114  prmgaplem6  17115  prmlem1  17166  prmlem2  17179  lt6abl  19964  metdseq0  24980  xrhmeo  25073  ovolicc2lem3  25646  itg2seq  25869  dvne0  26138  coeeulem  26349  radcnvlt1  26546  argimgt0  26742  cxple2  26827  ressatans  27064  eldmgm  27151  basellem2  27211  issqf  27265  bpos1  27412  bposlem3  27415  bposlem6  27418  2sqreulem1  27575  2sqreunnlem1  27578  pntpbnd2  27716  ostth2lem4  27765  crctcshwlkn0  30110  crctcsh  30113  eucrctshift  30534  ltflcei  38146  poimirlem4  38162  poimirlem13  38171  poimirlem14  38172  poimirlem15  38173  poimirlem31  38189  mblfinlem1  38195  mbfposadd  38205  itgaddnclem2  38217  ftc1anclem1  38231  ftc1anclem5  38235  dvasin  38242  reabsifnpos  44250  reabsifnneg  44252  icccncfext  46492  stoweidlem14  46619  stoweidlem34  46639  ltnltne  47924  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  ply1mulgsumlem2  49051