Theorem ltnle 11229

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 11228	. . 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 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  letric  11250  ltnled  11297  leaddsub  11630  mulge0b  12029  nnnle0  12195  nn0n0n1ge2b  12487  znnnlt1  12536  uzwo  12846  qsqueeze  13137  difreicc  13421  fzp1disj  13520  fzneuz  13545  fznuz  13546  uznfz  13547  difelfznle  13579  nelfzo  13601  ssfzoulel  13697  elfzonelfzo  13706  modfzo0difsn  13884  ssnn0fi  13926  discr1  14180  bcval5  14259  swrdnd  14595  swrdnnn0nd  14597  swrdnd0  14598  swrdsbslen  14605  swrdspsleq  14606  pfxnd0  14629  pfxccat3  14675  swrdccat  14676  pfxccat3a  14679  repswswrd  14725  cnpart  15182  absmax  15272  rlimrege0  15521  rpnnen2lem12  16169  alzdvds  16266  algcvgblem  16523  prmndvdsfaclt  16671  pcprendvds  16787  pcdvdsb  16816  pcmpt  16839  prmunb  16861  prmreclem2  16864  prmgaplem5  17002  prmgaplem6  17003  prmlem1  17054  prmlem2  17066  lt6abl  19809  metdseq0  24776  xrhmeo  24877  ovolicc2lem3  25453  itg2seq  25676  dvne0  25949  coeeulem  26162  radcnvlt1  26360  argimgt0  26554  cxple2  26639  ressatans  26877  eldmgm  26965  basellem2  27025  issqf  27079  bpos1  27227  bposlem3  27230  bposlem6  27233  2sqreulem1  27390  2sqreunnlem1  27393  pntpbnd2  27531  ostth2lem4  27580  crctcshwlkn0  29801  crctcsh  29804  eucrctshift  30222  ltflcei  37595  poimirlem4  37611  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem31  37638  mblfinlem1  37644  mbfposadd  37654  itgaddnclem2  37666  ftc1anclem1  37680  ftc1anclem5  37684  dvasin  37691  reabsifnpos  43615  reabsifnneg  43617  icccncfext  45878  stoweidlem14  46005  stoweidlem34  46025  ltnltne  47293  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  ply1mulgsumlem2  48369