Theorem ltnle 11212

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 11211	. . 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 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  letric  11233  ltnled  11280  leaddsub  11613  mulge0b  12012  nnnle0  12178  nn0n0n1ge2b  12470  znnnlt1  12518  uzwo  12824  qsqueeze  13116  difreicc  13400  fzp1disj  13499  fzneuz  13524  fznuz  13525  uznfz  13526  difelfznle  13558  nelfzo  13580  ssfzoulel  13676  elfzonelfzo  13685  modfzo0difsn  13866  ssnn0fi  13908  discr1  14162  bcval5  14241  swrdnd  14578  swrdnnn0nd  14580  swrdnd0  14581  swrdsbslen  14588  swrdspsleq  14589  pfxnd0  14612  pfxccat3  14657  swrdccat  14658  pfxccat3a  14661  repswswrd  14707  cnpart  15163  absmax  15253  rlimrege0  15502  rpnnen2lem12  16150  alzdvds  16247  algcvgblem  16504  prmndvdsfaclt  16652  pcprendvds  16768  pcdvdsb  16797  pcmpt  16820  prmunb  16842  prmreclem2  16845  prmgaplem5  16983  prmgaplem6  16984  prmlem1  17035  prmlem2  17047  lt6abl  19824  metdseq0  24799  xrhmeo  24900  ovolicc2lem3  25476  itg2seq  25699  dvne0  25972  coeeulem  26185  radcnvlt1  26383  argimgt0  26577  cxple2  26662  ressatans  26900  eldmgm  26988  basellem2  27048  issqf  27102  bpos1  27250  bposlem3  27253  bposlem6  27256  2sqreulem1  27413  2sqreunnlem1  27416  pntpbnd2  27554  ostth2lem4  27603  crctcshwlkn0  29894  crctcsh  29897  eucrctshift  30318  ltflcei  37809  poimirlem4  37825  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem31  37852  mblfinlem1  37858  mbfposadd  37868  itgaddnclem2  37880  ftc1anclem1  37894  ftc1anclem5  37898  dvasin  37905  reabsifnpos  43874  reabsifnneg  43876  icccncfext  46131  stoweidlem14  46258  stoweidlem34  46278  ltnltne  47545  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  ply1mulgsumlem2  48633