Theorem ltnle 11253

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 11252	. . 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 5107  ℝcr 11067   < clt 11208   ≤ cle 11209

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-xr 11212  df-le 11214

This theorem is referenced by:  letric  11274  ltnled  11321  leaddsub  11654  mulge0b  12053  nnnle0  12219  nn0n0n1ge2b  12511  znnnlt1  12560  uzwo  12870  qsqueeze  13161  difreicc  13445  fzp1disj  13544  fzneuz  13569  fznuz  13570  uznfz  13571  difelfznle  13603  nelfzo  13625  ssfzoulel  13721  elfzonelfzo  13730  modfzo0difsn  13908  ssnn0fi  13950  discr1  14204  bcval5  14283  swrdnd  14619  swrdnnn0nd  14621  swrdnd0  14622  swrdsbslen  14629  swrdspsleq  14630  pfxnd0  14653  pfxccat3  14699  swrdccat  14700  pfxccat3a  14703  repswswrd  14749  cnpart  15206  absmax  15296  rlimrege0  15545  rpnnen2lem12  16193  alzdvds  16290  algcvgblem  16547  prmndvdsfaclt  16695  pcprendvds  16811  pcdvdsb  16840  pcmpt  16863  prmunb  16885  prmreclem2  16888  prmgaplem5  17026  prmgaplem6  17027  prmlem1  17078  prmlem2  17090  lt6abl  19825  metdseq0  24743  xrhmeo  24844  ovolicc2lem3  25420  itg2seq  25643  dvne0  25916  coeeulem  26129  radcnvlt1  26327  argimgt0  26521  cxple2  26606  ressatans  26844  eldmgm  26932  basellem2  26992  issqf  27046  bpos1  27194  bposlem3  27197  bposlem6  27200  2sqreulem1  27357  2sqreunnlem1  27360  pntpbnd2  27498  ostth2lem4  27547  crctcshwlkn0  29751  crctcsh  29754  eucrctshift  30172  ltflcei  37602  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem31  37645  mblfinlem1  37651  mbfposadd  37661  itgaddnclem2  37673  ftc1anclem1  37687  ftc1anclem5  37691  dvasin  37698  reabsifnpos  43622  reabsifnneg  43624  icccncfext  45885  stoweidlem14  46012  stoweidlem34  46032  ltnltne  47300  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  ply1mulgsumlem2  48376