Theorem ltnle 11382

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11340  df-le 11342

This theorem is used by:  letric  11403  ltnled  11450  leaddsub  11785  mulge0b  12180  nnnle0  12364  nn0n0n1ge2b  12668  znnnlt1  12716  uzwo  13031  qsqueeze  13324  difreicc  13608  fzp1disj  13710  fzneuz  13735  fznuz  13736  uznfz  13737  difelfznle  13769  nelfzo  13792  ssfzoulel  13888  elfzonelfzo  13897  modfzo0difsn  14079  ssnn0fi  14121  discr1  14376  bcval5  14455  swrdnd  14797  swrdnnn0nd  14799  swrdnd0  14800  swrdsbslen  14807  swrdspsleq  14808  pfxnd0  14831  pfxccat3  14876  swrdccat  14877  pfxccat3a  14880  repswswrd  14928  cnpart  15400  absmax  15490  rlimrege0  15739  rpnnen2lem12  16386  alzdvds  16483  algcvgblem  16745  prmndvdsfaclt  16894  pcprendvds  17011  pcdvdsb  17040  pcmpt  17063  prmunb  17085  prmreclem2  17088  prmgaplem5  17226  prmgaplem6  17227  prmlem1  17278  prmlem2  17291  lt6abl  20102  metdseq0  25167  xrhmeo  25260  ovolicc2lem3  25833  itg2seq  26056  dvne0  26324  coeeulem  26536  radcnvlt1  26738  argimgt0  26933  cxple2  27018  ressatans  27255  eldmgm  27342  basellem2  27402  issqf  27456  bpos1  27603  bposlem3  27606  bposlem6  27609  2sqreulem1  27766  2sqreunnlem1  27769  pntpbnd2  27907  ostth2lem4  27956  crctcshwlkn0  30403  crctcsh  30406  eucrctshift  30837  ltflcei  38511  poimirlem4  38522  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem31  38549  mblfinlem1  38555  mbfposadd  38565  itgaddnclem2  38577  ftc1anclem1  38591  ftc1anclem5  38595  dvasin  38602  reabsifnpos  44618  reabsifnneg  44620  icccncfext  46866  stoweidlem14  46993  stoweidlem34  47013  ltnltne  48338  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  ply1mulgsumlem2  49468