Theorem ltnle 11337

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-xr 11296  df-le 11298

This theorem is referenced by:  letric  11358  ltnled  11405  leaddsub  11736  mulge0b  12135  nnnle0  12296  nn0n0n1ge2b  12592  znnnlt1  12641  uzwo  12950  qsqueeze  13239  difreicc  13520  fzp1disj  13619  fzneuz  13644  fznuz  13645  uznfz  13646  difelfznle  13678  nelfzo  13700  ssfzoulel  13795  elfzonelfzo  13804  modfzo0difsn  13980  ssnn0fi  14022  discr1  14274  bcval5  14353  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  swrdsbslen  14698  swrdspsleq  14699  pfxnd0  14722  pfxccat3  14768  swrdccat  14769  pfxccat3a  14772  repswswrd  14818  cnpart  15275  absmax  15364  rlimrege0  15611  rpnnen2lem12  16257  alzdvds  16353  algcvgblem  16610  prmndvdsfaclt  16758  pcprendvds  16873  pcdvdsb  16902  pcmpt  16925  prmunb  16947  prmreclem2  16950  prmgaplem5  17088  prmgaplem6  17089  prmlem1  17141  prmlem2  17153  lt6abl  19927  metdseq0  24889  xrhmeo  24990  ovolicc2lem3  25567  itg2seq  25791  dvne0  26064  coeeulem  26277  radcnvlt1  26475  argimgt0  26668  cxple2  26753  ressatans  26991  eldmgm  27079  basellem2  27139  issqf  27193  bpos1  27341  bposlem3  27344  bposlem6  27347  2sqreulem1  27504  2sqreunnlem1  27507  pntpbnd2  27645  ostth2lem4  27694  crctcshwlkn0  29850  crctcsh  29853  eucrctshift  30271  ltflcei  37594  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem31  37637  mblfinlem1  37643  mbfposadd  37653  itgaddnclem2  37665  ftc1anclem1  37679  ftc1anclem5  37683  dvasin  37690  reabsifnpos  43622  reabsifnneg  43624  icccncfext  45842  stoweidlem14  45969  stoweidlem34  45989  ltnltne  47248  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  ply1mulgsumlem2  48232