Theorem ltnle 10985

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-xr 10944  df-le 10946

This theorem is referenced by:  letric  11005  ltnled  11052  leaddsub  11381  mulge0b  11775  nnnle0  11936  nn0n0n1ge2b  12231  znnnlt1  12277  uzwo  12580  qsqueeze  12864  difreicc  13145  fzp1disj  13244  fzneuz  13266  fznuz  13267  uznfz  13268  difelfznle  13299  nelfzo  13321  ssfzoulel  13409  elfzonelfzo  13417  modfzo0difsn  13591  ssnn0fi  13633  discr1  13882  bcval5  13960  swrdnd  14295  swrdnnn0nd  14297  swrdnd0  14298  swrdsbslen  14305  swrdspsleq  14306  pfxnd0  14329  pfxccat3  14375  swrdccat  14376  pfxccat3a  14379  repswswrd  14425  cnpart  14879  absmax  14969  rlimrege0  15216  rpnnen2lem12  15862  alzdvds  15957  algcvgblem  16210  prmndvdsfaclt  16358  pcprendvds  16469  pcdvdsb  16498  pcmpt  16521  prmunb  16543  prmreclem2  16546  prmgaplem5  16684  prmgaplem6  16685  prmlem1  16737  prmlem2  16749  lt6abl  19411  metdseq0  23923  xrhmeo  24015  ovolicc2lem3  24588  itg2seq  24812  dvne0  25080  coeeulem  25290  radcnvlt1  25482  argimgt0  25672  cxple2  25757  ressatans  25989  eldmgm  26076  basellem2  26136  issqf  26190  bpos1  26336  bposlem3  26339  bposlem6  26342  2sqreulem1  26499  2sqreunnlem1  26502  pntpbnd2  26640  ostth2lem4  26689  crctcshwlkn0  28087  crctcsh  28090  eucrctshift  28508  ltflcei  35692  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem31  35735  mblfinlem1  35741  mbfposadd  35751  itgaddnclem2  35763  ftc1anclem1  35777  ftc1anclem5  35781  dvasin  35788  reabsifnpos  41130  reabsifnneg  41132  icccncfext  43318  stoweidlem14  43445  stoweidlem34  43465  ltnltne  44679  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  ply1mulgsumlem2  45616