Theorem ltnle 10912

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2110   class class class wbr 5053  ℝcr 10728   < clt 10867   ≤ cle 10868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-xp 5557  df-cnv 5559  df-xr 10871  df-le 10873

This theorem is referenced by:  letric  10932  ltnled  10979  leaddsub  11308  mulge0b  11702  nnnle0  11863  nn0n0n1ge2b  12158  znnnlt1  12204  uzwo  12507  qsqueeze  12791  difreicc  13072  fzp1disj  13171  fzneuz  13193  fznuz  13194  uznfz  13195  difelfznle  13226  nelfzo  13248  ssfzoulel  13336  elfzonelfzo  13344  modfzo0difsn  13516  ssnn0fi  13558  discr1  13806  bcval5  13884  swrdnd  14219  swrdnnn0nd  14221  swrdnd0  14222  swrdsbslen  14229  swrdspsleq  14230  pfxnd0  14253  pfxccat3  14299  swrdccat  14300  pfxccat3a  14303  repswswrd  14349  cnpart  14803  absmax  14893  rlimrege0  15140  rpnnen2lem12  15786  alzdvds  15881  algcvgblem  16134  prmndvdsfaclt  16282  pcprendvds  16393  pcdvdsb  16422  pcmpt  16445  prmunb  16467  prmreclem2  16470  prmgaplem5  16608  prmgaplem6  16609  prmlem1  16661  prmlem2  16673  lt6abl  19280  metdseq0  23751  xrhmeo  23843  ovolicc2lem3  24416  itg2seq  24640  dvne0  24908  coeeulem  25118  radcnvlt1  25310  argimgt0  25500  cxple2  25585  ressatans  25817  eldmgm  25904  basellem2  25964  issqf  26018  bpos1  26164  bposlem3  26167  bposlem6  26170  2sqreulem1  26327  2sqreunnlem1  26330  pntpbnd2  26468  ostth2lem4  26517  crctcshwlkn0  27905  crctcsh  27908  eucrctshift  28326  ltflcei  35502  poimirlem4  35518  poimirlem13  35527  poimirlem14  35528  poimirlem15  35529  poimirlem31  35545  mblfinlem1  35551  mbfposadd  35561  itgaddnclem2  35573  ftc1anclem1  35587  ftc1anclem5  35591  dvasin  35598  reabsifnpos  40917  reabsifnneg  40919  icccncfext  43103  stoweidlem14  43230  stoweidlem34  43250  ltnltne  44464  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  ply1mulgsumlem2  45401