Theorem ltnle 11312

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   < clt 11267   ≤ cle 11268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-xr 11271  df-le 11273

This theorem is referenced by:  letric  11333  ltnled  11380  leaddsub  11711  mulge0b  12110  nnnle0  12271  nn0n0n1ge2b  12568  znnnlt1  12617  uzwo  12925  qsqueeze  13215  difreicc  13499  fzp1disj  13598  fzneuz  13623  fznuz  13624  uznfz  13625  difelfznle  13657  nelfzo  13679  ssfzoulel  13774  elfzonelfzo  13783  modfzo0difsn  13959  ssnn0fi  14001  discr1  14255  bcval5  14334  swrdnd  14670  swrdnnn0nd  14672  swrdnd0  14673  swrdsbslen  14680  swrdspsleq  14681  pfxnd0  14704  pfxccat3  14750  swrdccat  14751  pfxccat3a  14754  repswswrd  14800  cnpart  15257  absmax  15346  rlimrege0  15593  rpnnen2lem12  16241  alzdvds  16337  algcvgblem  16594  prmndvdsfaclt  16742  pcprendvds  16858  pcdvdsb  16887  pcmpt  16910  prmunb  16932  prmreclem2  16935  prmgaplem5  17073  prmgaplem6  17074  prmlem1  17125  prmlem2  17137  lt6abl  19874  metdseq0  24792  xrhmeo  24893  ovolicc2lem3  25470  itg2seq  25693  dvne0  25966  coeeulem  26179  radcnvlt1  26377  argimgt0  26571  cxple2  26656  ressatans  26894  eldmgm  26982  basellem2  27042  issqf  27096  bpos1  27244  bposlem3  27247  bposlem6  27250  2sqreulem1  27407  2sqreunnlem1  27410  pntpbnd2  27548  ostth2lem4  27597  crctcshwlkn0  29749  crctcsh  29752  eucrctshift  30170  ltflcei  37578  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem31  37621  mblfinlem1  37627  mbfposadd  37637  itgaddnclem2  37649  ftc1anclem1  37663  ftc1anclem5  37667  dvasin  37674  reabsifnpos  43604  reabsifnneg  43606  icccncfext  45864  stoweidlem14  45991  stoweidlem34  46011  ltnltne  47276  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  ply1mulgsumlem2  48311