Theorem ltnle 11304

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 11303	. . 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 2146   class class class wbr 5111  ℝcr 11114   < clt 11258   ≤ cle 11259

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11262  df-le 11264

This theorem is used by:  letric  11325  ltnled  11372  leaddsub  11705  mulge0b  12100  nnnle0  12284  nn0n0n1ge2b  12588  znnnlt1  12636  uzwo  12951  qsqueeze  13243  difreicc  13527  fzp1disj  13628  fzneuz  13653  fznuz  13654  uznfz  13655  difelfznle  13687  nelfzo  13710  ssfzoulel  13806  elfzonelfzo  13815  modfzo0difsn  13997  ssnn0fi  14039  discr1  14293  bcval5  14372  swrdnd  14714  swrdnnn0nd  14716  swrdnd0  14717  swrdsbslen  14724  swrdspsleq  14725  pfxnd0  14748  pfxccat3  14793  swrdccat  14794  pfxccat3a  14797  repswswrd  14845  cnpart  15315  absmax  15405  rlimrege0  15654  rpnnen2lem12  16303  alzdvds  16400  algcvgblem  16657  prmndvdsfaclt  16806  pcprendvds  16922  pcdvdsb  16951  pcmpt  16974  prmunb  16996  prmreclem2  16999  prmgaplem5  17137  prmgaplem6  17138  prmlem1  17189  prmlem2  17202  lt6abl  20009  metdseq0  25063  xrhmeo  25156  ovolicc2lem3  25729  itg2seq  25952  dvne0  26221  coeeulem  26432  radcnvlt1  26632  argimgt0  26828  cxple2  26913  ressatans  27150  eldmgm  27237  basellem2  27297  issqf  27351  bpos1  27498  bposlem3  27501  bposlem6  27504  2sqreulem1  27661  2sqreunnlem1  27664  pntpbnd2  27802  ostth2lem4  27851  crctcshwlkn0  30237  crctcsh  30240  eucrctshift  30665  ltflcei  38316  poimirlem4  38332  poimirlem13  38341  poimirlem14  38342  poimirlem15  38343  poimirlem31  38359  mblfinlem1  38365  mbfposadd  38375  itgaddnclem2  38387  ftc1anclem1  38401  ftc1anclem5  38405  dvasin  38412  reabsifnpos  44417  reabsifnneg  44419  icccncfext  46659  stoweidlem14  46786  stoweidlem34  46806  ltnltne  48094  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  ply1mulgsumlem2  49224