Theorem ltnle 11195

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ℝcr 11008   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-xr 11153  df-le 11155

This theorem is referenced by:  letric  11216  ltnled  11263  leaddsub  11596  mulge0b  11995  nnnle0  12161  nn0n0n1ge2b  12453  znnnlt1  12502  uzwo  12812  qsqueeze  13103  difreicc  13387  fzp1disj  13486  fzneuz  13511  fznuz  13512  uznfz  13513  difelfznle  13545  nelfzo  13567  ssfzoulel  13663  elfzonelfzo  13672  modfzo0difsn  13850  ssnn0fi  13892  discr1  14146  bcval5  14225  swrdnd  14561  swrdnnn0nd  14563  swrdnd0  14564  swrdsbslen  14571  swrdspsleq  14572  pfxnd0  14595  pfxccat3  14640  swrdccat  14641  pfxccat3a  14644  repswswrd  14690  cnpart  15147  absmax  15237  rlimrege0  15486  rpnnen2lem12  16134  alzdvds  16231  algcvgblem  16488  prmndvdsfaclt  16636  pcprendvds  16752  pcdvdsb  16781  pcmpt  16804  prmunb  16826  prmreclem2  16829  prmgaplem5  16967  prmgaplem6  16968  prmlem1  17019  prmlem2  17031  lt6abl  19774  metdseq0  24741  xrhmeo  24842  ovolicc2lem3  25418  itg2seq  25641  dvne0  25914  coeeulem  26127  radcnvlt1  26325  argimgt0  26519  cxple2  26604  ressatans  26842  eldmgm  26930  basellem2  26990  issqf  27044  bpos1  27192  bposlem3  27195  bposlem6  27198  2sqreulem1  27355  2sqreunnlem1  27358  pntpbnd2  27496  ostth2lem4  27545  crctcshwlkn0  29766  crctcsh  29769  eucrctshift  30187  ltflcei  37592  poimirlem4  37608  poimirlem13  37617  poimirlem14  37618  poimirlem15  37619  poimirlem31  37635  mblfinlem1  37641  mbfposadd  37651  itgaddnclem2  37663  ftc1anclem1  37677  ftc1anclem5  37681  dvasin  37688  reabsifnpos  43610  reabsifnneg  43612  icccncfext  45872  stoweidlem14  45999  stoweidlem34  46019  ltnltne  47287  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  ply1mulgsumlem2  48376