Theorem ltnle 11293

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2107   class class class wbr 5149  ℝcr 11109   < clt 11248   ≤ cle 11249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-xr 11252  df-le 11254

This theorem is referenced by:  letric  11314  ltnled  11361  leaddsub  11690  mulge0b  12084  nnnle0  12245  nn0n0n1ge2b  12540  znnnlt1  12589  uzwo  12895  qsqueeze  13180  difreicc  13461  fzp1disj  13560  fzneuz  13582  fznuz  13583  uznfz  13584  difelfznle  13615  nelfzo  13637  ssfzoulel  13726  elfzonelfzo  13734  modfzo0difsn  13908  ssnn0fi  13950  discr1  14202  bcval5  14278  swrdnd  14604  swrdnnn0nd  14606  swrdnd0  14607  swrdsbslen  14614  swrdspsleq  14615  pfxnd0  14638  pfxccat3  14684  swrdccat  14685  pfxccat3a  14688  repswswrd  14734  cnpart  15187  absmax  15276  rlimrege0  15523  rpnnen2lem12  16168  alzdvds  16263  algcvgblem  16514  prmndvdsfaclt  16662  pcprendvds  16773  pcdvdsb  16802  pcmpt  16825  prmunb  16847  prmreclem2  16850  prmgaplem5  16988  prmgaplem6  16989  prmlem1  17041  prmlem2  17053  lt6abl  19763  metdseq0  24370  xrhmeo  24462  ovolicc2lem3  25036  itg2seq  25260  dvne0  25528  coeeulem  25738  radcnvlt1  25930  argimgt0  26120  cxple2  26205  ressatans  26439  eldmgm  26526  basellem2  26586  issqf  26640  bpos1  26786  bposlem3  26789  bposlem6  26792  2sqreulem1  26949  2sqreunnlem1  26952  pntpbnd2  27090  ostth2lem4  27139  crctcshwlkn0  29075  crctcsh  29078  eucrctshift  29496  ltflcei  36476  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem31  36519  mblfinlem1  36525  mbfposadd  36535  itgaddnclem2  36547  ftc1anclem1  36561  ftc1anclem5  36565  dvasin  36572  reabsifnpos  42384  reabsifnneg  42386  icccncfext  44603  stoweidlem14  44730  stoweidlem34  44750  ltnltne  46007  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  ply1mulgsumlem2  47068