Theorem ltnle 10720

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   < clt 10675   ≤ cle 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-xr 10679  df-le 10681

This theorem is referenced by:  letric  10740  ltnled  10787  leaddsub  11116  mulge0b  11510  nnnle0  11671  nn0n0n1ge2b  11964  znnnlt1  12010  uzwo  12312  qsqueeze  12595  difreicc  12871  fzp1disj  12967  fzneuz  12989  fznuz  12990  uznfz  12991  difelfznle  13022  nelfzo  13044  ssfzoulel  13132  elfzonelfzo  13140  modfzo0difsn  13312  ssnn0fi  13354  discr1  13601  bcval5  13679  swrdnd  14016  swrdnnn0nd  14018  swrdnd0  14019  swrdsbslen  14026  swrdspsleq  14027  pfxnd0  14050  pfxccat3  14096  swrdccat  14097  pfxccat3a  14100  repswswrd  14146  cnpart  14599  absmax  14689  rlimrege0  14936  rpnnen2lem12  15578  alzdvds  15670  algcvgblem  15921  prmndvdsfaclt  16067  pcprendvds  16177  pcdvdsb  16205  pcmpt  16228  prmunb  16250  prmreclem2  16253  prmgaplem5  16391  prmgaplem6  16392  prmlem1  16441  prmlem2  16453  lt6abl  19015  metdseq0  23462  xrhmeo  23550  ovolicc2lem3  24120  itg2seq  24343  dvne0  24608  coeeulem  24814  radcnvlt1  25006  argimgt0  25195  cxple2  25280  ressatans  25512  eldmgm  25599  basellem2  25659  issqf  25713  bpos1  25859  bposlem3  25862  bposlem6  25865  2sqreulem1  26022  2sqreunnlem1  26025  pntpbnd2  26163  ostth2lem4  26212  crctcshwlkn0  27599  crctcsh  27602  eucrctshift  28022  ltflcei  34895  poimirlem4  34911  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem31  34938  mblfinlem1  34944  mbfposadd  34954  itgaddnclem2  34966  ftc1anclem1  34982  ftc1anclem5  34986  dvasin  34993  icccncfext  42190  stoweidlem14  42319  stoweidlem34  42339  ltnltne  43519  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  ply1mulgsumlem2  44461