Theorem ltnle 11210

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-xr 11168  df-le 11170

This theorem is referenced by:  letric  11231  ltnled  11278  leaddsub  11611  mulge0b  12010  nnnle0  12176  nn0n0n1ge2b  12468  znnnlt1  12516  uzwo  12822  qsqueeze  13114  difreicc  13398  fzp1disj  13497  fzneuz  13522  fznuz  13523  uznfz  13524  difelfznle  13556  nelfzo  13578  ssfzoulel  13674  elfzonelfzo  13683  modfzo0difsn  13864  ssnn0fi  13906  discr1  14160  bcval5  14239  swrdnd  14576  swrdnnn0nd  14578  swrdnd0  14579  swrdsbslen  14586  swrdspsleq  14587  pfxnd0  14610  pfxccat3  14655  swrdccat  14656  pfxccat3a  14659  repswswrd  14705  cnpart  15161  absmax  15251  rlimrege0  15500  rpnnen2lem12  16148  alzdvds  16245  algcvgblem  16502  prmndvdsfaclt  16650  pcprendvds  16766  pcdvdsb  16795  pcmpt  16818  prmunb  16840  prmreclem2  16843  prmgaplem5  16981  prmgaplem6  16982  prmlem1  17033  prmlem2  17045  lt6abl  19822  metdseq0  24797  xrhmeo  24898  ovolicc2lem3  25474  itg2seq  25697  dvne0  25970  coeeulem  26183  radcnvlt1  26381  argimgt0  26575  cxple2  26660  ressatans  26898  eldmgm  26986  basellem2  27046  issqf  27100  bpos1  27248  bposlem3  27251  bposlem6  27254  2sqreulem1  27411  2sqreunnlem1  27414  pntpbnd2  27552  ostth2lem4  27601  crctcshwlkn0  29843  crctcsh  29846  eucrctshift  30267  ltflcei  37748  poimirlem4  37764  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  poimirlem31  37791  mblfinlem1  37797  mbfposadd  37807  itgaddnclem2  37819  ftc1anclem1  37833  ftc1anclem5  37837  dvasin  37844  reabsifnpos  43816  reabsifnneg  43818  icccncfext  46073  stoweidlem14  46200  stoweidlem34  46220  ltnltne  47487  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  ply1mulgsumlem2  48575