Theorem ltnle 11428

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   < clt 11382   ≤ cle 11383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-xr 11386  df-le 11388

This theorem is used by:  letric  11449  ltnled  11496  leaddsub  11832  mulge0b  12227  nnnle0  12411  nn0n0n1ge2b  12715  znnnlt1  12763  uzwo  13078  qsqueeze  13371  difreicc  13655  fzp1disj  13757  fzneuz  13782  fznuz  13783  uznfz  13784  difelfznle  13816  nelfzo  13839  ssfzoulel  13935  elfzonelfzo  13944  modfzo0difsn  14126  ssnn0fi  14168  discr1  14424  bcval5  14503  swrdnd  14846  swrdnnn0nd  14848  swrdnd0  14849  swrdsbslen  14856  swrdspsleq  14857  pfxnd0  14880  pfxccat3  14925  swrdccat  14926  pfxccat3a  14929  repswswrd  14977  cnpart  15450  absmax  15540  rlimrege0  15790  rpnnen2lem12  16437  alzdvds  16534  algcvgblem  16796  prmndvdsfaclt  16945  pcprendvds  17062  pcdvdsb  17091  pcmpt  17114  prmunb  17136  prmreclem2  17139  prmgaplem5  17277  prmgaplem6  17278  prmlem1  17329  prmlem2  17342  lt6abl  20160  metdseq0  25229  xrhmeo  25322  ovolicc2lem3  25895  itg2seq  26118  dvne0  26386  coeeulem  26598  radcnvlt1  26802  argimgt0  26997  cxple2  27082  ressatans  27319  eldmgm  27406  basellem2  27466  issqf  27520  bpos1  27667  bposlem3  27670  bposlem6  27673  2sqreulem1  27830  2sqreunnlem1  27833  pntpbnd2  27971  ostth2lem4  28020  crctcshwlkn0  30467  crctcsh  30470  eucrctshift  30901  ltflcei  38799  poimirlem4  38810  poimirlem13  38819  poimirlem14  38820  poimirlem15  38821  poimirlem31  38837  mblfinlem1  38843  mbfposadd  38853  itgaddnclem2  38865  ftc1anclem1  38879  ftc1anclem5  38883  dvasin  38890  reabsifnpos  44894  reabsifnneg  44896  icccncfext  47170  stoweidlem14  47297  stoweidlem34  47317  ltnltne  48642  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  ply1mulgsumlem2  49830