Theorem ltnle 11340

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-xr 11299  df-le 11301

This theorem is referenced by:  letric  11361  ltnled  11408  leaddsub  11739  mulge0b  12138  nnnle0  12299  nn0n0n1ge2b  12595  znnnlt1  12644  uzwo  12953  qsqueeze  13243  difreicc  13524  fzp1disj  13623  fzneuz  13648  fznuz  13649  uznfz  13650  difelfznle  13682  nelfzo  13704  ssfzoulel  13799  elfzonelfzo  13808  modfzo0difsn  13984  ssnn0fi  14026  discr1  14278  bcval5  14357  swrdnd  14692  swrdnnn0nd  14694  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  pfxnd0  14726  pfxccat3  14772  swrdccat  14773  pfxccat3a  14776  repswswrd  14822  cnpart  15279  absmax  15368  rlimrege0  15615  rpnnen2lem12  16261  alzdvds  16357  algcvgblem  16614  prmndvdsfaclt  16762  pcprendvds  16878  pcdvdsb  16907  pcmpt  16930  prmunb  16952  prmreclem2  16955  prmgaplem5  17093  prmgaplem6  17094  prmlem1  17145  prmlem2  17157  lt6abl  19913  metdseq0  24876  xrhmeo  24977  ovolicc2lem3  25554  itg2seq  25777  dvne0  26050  coeeulem  26263  radcnvlt1  26461  argimgt0  26654  cxple2  26739  ressatans  26977  eldmgm  27065  basellem2  27125  issqf  27179  bpos1  27327  bposlem3  27330  bposlem6  27333  2sqreulem1  27490  2sqreunnlem1  27493  pntpbnd2  27631  ostth2lem4  27680  crctcshwlkn0  29841  crctcsh  29844  eucrctshift  30262  ltflcei  37615  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem31  37658  mblfinlem1  37664  mbfposadd  37674  itgaddnclem2  37686  ftc1anclem1  37700  ftc1anclem5  37704  dvasin  37711  reabsifnpos  43646  reabsifnneg  43648  icccncfext  45902  stoweidlem14  46029  stoweidlem34  46049  ltnltne  47311  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  ply1mulgsumlem2  48304