Theorem ltnle 11284

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-xr 11242  df-le 11244

This theorem is referenced by:  letric  11305  ltnled  11352  leaddsub  11685  mulge0b  12080  nnnle0  12264  nn0n0n1ge2b  12568  znnnlt1  12616  uzwo  12930  qsqueeze  13222  difreicc  13506  fzp1disj  13607  fzneuz  13632  fznuz  13633  uznfz  13634  difelfznle  13666  nelfzo  13689  ssfzoulel  13785  elfzonelfzo  13794  modfzo0difsn  13975  ssnn0fi  14017  discr1  14271  bcval5  14350  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  pfxnd0  14722  pfxccat3  14767  swrdccat  14768  pfxccat3a  14771  repswswrd  14817  cnpart  15287  absmax  15377  rlimrege0  15626  rpnnen2lem12  16276  alzdvds  16373  algcvgblem  16630  prmndvdsfaclt  16779  pcprendvds  16895  pcdvdsb  16924  pcmpt  16947  prmunb  16969  prmreclem2  16972  prmgaplem5  17110  prmgaplem6  17111  prmlem1  17162  prmlem2  17175  lt6abl  19960  metdseq0  25012  xrhmeo  25105  ovolicc2lem3  25678  itg2seq  25901  dvne0  26170  coeeulem  26381  radcnvlt1  26581  argimgt0  26777  cxple2  26862  ressatans  27099  eldmgm  27186  basellem2  27246  issqf  27300  bpos1  27447  bposlem3  27450  bposlem6  27453  2sqreulem1  27610  2sqreunnlem1  27613  pntpbnd2  27751  ostth2lem4  27800  crctcshwlkn0  30170  crctcsh  30173  eucrctshift  30594  ltflcei  38259  poimirlem4  38275  poimirlem13  38284  poimirlem14  38285  poimirlem15  38286  poimirlem31  38302  mblfinlem1  38308  mbfposadd  38318  itgaddnclem2  38330  ftc1anclem1  38344  ftc1anclem5  38348  dvasin  38355  reabsifnpos  44359  reabsifnneg  44361  icccncfext  46601  stoweidlem14  46728  stoweidlem34  46748  ltnltne  48036  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  ply1mulgsumlem2  49167