Theorem ltnle 11313

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 11312	. . 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 2145   class class class wbr 5103  ℝcr 11123   < clt 11267   ≤ cle 11268

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-xr 11271  df-le 11273

This theorem is used by:  letric  11334  ltnled  11381  leaddsub  11714  mulge0b  12109  nnnle0  12293  nn0n0n1ge2b  12597  znnnlt1  12645  uzwo  12960  qsqueeze  13253  difreicc  13537  fzp1disj  13638  fzneuz  13663  fznuz  13664  uznfz  13665  difelfznle  13697  nelfzo  13720  ssfzoulel  13816  elfzonelfzo  13825  modfzo0difsn  14007  ssnn0fi  14049  discr1  14303  bcval5  14382  swrdnd  14724  swrdnnn0nd  14726  swrdnd0  14727  swrdsbslen  14734  swrdspsleq  14735  pfxnd0  14758  pfxccat3  14803  swrdccat  14804  pfxccat3a  14807  repswswrd  14855  cnpart  15327  absmax  15417  rlimrege0  15666  rpnnen2lem12  16313  alzdvds  16410  algcvgblem  16667  prmndvdsfaclt  16816  pcprendvds  16932  pcdvdsb  16961  pcmpt  16984  prmunb  17006  prmreclem2  17009  prmgaplem5  17147  prmgaplem6  17148  prmlem1  17199  prmlem2  17212  lt6abl  20022  metdseq0  25081  xrhmeo  25174  ovolicc2lem3  25747  itg2seq  25970  dvne0  26238  coeeulem  26450  radcnvlt1  26654  argimgt0  26849  cxple2  26934  ressatans  27171  eldmgm  27258  basellem2  27318  issqf  27372  bpos1  27519  bposlem3  27522  bposlem6  27525  2sqreulem1  27682  2sqreunnlem1  27685  pntpbnd2  27823  ostth2lem4  27872  crctcshwlkn0  30289  crctcsh  30292  eucrctshift  30723  ltflcei  38362  poimirlem4  38373  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem31  38400  mblfinlem1  38406  mbfposadd  38416  itgaddnclem2  38428  ftc1anclem1  38442  ftc1anclem5  38446  dvasin  38453  reabsifnpos  44473  reabsifnneg  44475  icccncfext  46715  stoweidlem14  46842  stoweidlem34  46862  ltnltne  48187  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  ply1mulgsumlem2  49317