Theorem ltnle 9996

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-xr 9957  df-le 9959

This theorem is referenced by:  letric  10016  ltnled  10063  leaddsub  10383  mulge0b  10772  nnnle0  10928  nn0n0n1ge2b  11236  znnnlt1  11281  uzwo  11627  qsqueeze  11906  difreicc  12175  fzp1disj  12269  fzneuz  12290  fznuz  12291  uznfz  12292  difelfznle  12322  nelfzo  12344  ssfzoulel  12428  elfzonelfzo  12436  modfzo0difsn  12604  ssnn0fi  12646  discr1  12862  facdiv  12936  bcval5  12967  ccatsymb  13219  swrdnd  13284  swrdsbslen  13300  swrdspsleq  13301  swrdccat3  13343  repswswrd  13382  cnpart  13828  absmax  13917  rlimrege0  14158  znnenlem  14779  rpnnen2lem12  14793  alzdvds  14880  algcvgblem  15128  prmndvdsfaclt  15273  pcprendvds  15383  pcdvdsb  15411  pcmpt  15434  prmunb  15456  prmreclem2  15459  prmgaplem5  15597  prmgaplem6  15598  prmlem1  15652  prmlem2  15665  lt6abl  18119  metdseq0  22465  xrhmeo  22553  ovolicc2lem3  23094  itg2seq  23315  dvne0  23578  coeeulem  23784  radcnvlt1  23976  argimgt0  24162  cxple2  24243  ressatans  24461  eldmgm  24548  basellem2  24608  issqf  24662  bpos1  24808  bposlem3  24811  bposlem6  24814  pntpbnd2  25076  ostth2lem4  25125  ltflcei  32567  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem31  32610  mblfinlem1  32616  mbfposadd  32627  itgaddnclem2  32639  ftc1anclem1  32655  ftc1anclem5  32659  dvasin  32666  icccncfext  38773  stoweidlem14  38907  stoweidlem34  38927  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  pfxccat3  40289  pfxccat3a  40292  ltnltne  40345  crctcsh1wlkn0  41024  crctcsh  41027  eucrctshift  41411  ply1mulgsumlem2  41969