Theorem ltnle 11295

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105   < clt 11249   ≤ cle 11250

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-xp 5666  df-cnv 5668  df-xr 11253  df-le 11255

This theorem is used by:  letric  11316  ltnled  11363  leaddsub  11696  mulge0b  12091  nnnle0  12275  nn0n0n1ge2b  12579  znnnlt1  12627  uzwo  12941  qsqueeze  13233  difreicc  13517  fzp1disj  13618  fzneuz  13643  fznuz  13644  uznfz  13645  difelfznle  13677  nelfzo  13700  ssfzoulel  13796  elfzonelfzo  13805  modfzo0difsn  13986  ssnn0fi  14028  discr1  14282  bcval5  14361  swrdnd  14699  swrdnnn0nd  14701  swrdnd0  14702  swrdsbslen  14709  swrdspsleq  14710  pfxnd0  14733  pfxccat3  14778  swrdccat  14779  pfxccat3a  14782  repswswrd  14828  cnpart  15298  absmax  15388  rlimrege0  15637  rpnnen2lem12  16287  alzdvds  16384  algcvgblem  16641  prmndvdsfaclt  16790  pcprendvds  16906  pcdvdsb  16935  pcmpt  16958  prmunb  16980  prmreclem2  16983  prmgaplem5  17121  prmgaplem6  17122  prmlem1  17173  prmlem2  17186  lt6abl  19971  metdseq0  25023  xrhmeo  25116  ovolicc2lem3  25689  itg2seq  25912  dvne0  26181  coeeulem  26392  radcnvlt1  26592  argimgt0  26788  cxple2  26873  ressatans  27110  eldmgm  27197  basellem2  27257  issqf  27311  bpos1  27458  bposlem3  27461  bposlem6  27464  2sqreulem1  27621  2sqreunnlem1  27624  pntpbnd2  27762  ostth2lem4  27811  crctcshwlkn0  30181  crctcsh  30184  eucrctshift  30605  ltflcei  38287  poimirlem4  38303  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem31  38330  mblfinlem1  38336  mbfposadd  38346  itgaddnclem2  38358  ftc1anclem1  38372  ftc1anclem5  38376  dvasin  38383  reabsifnpos  44387  reabsifnneg  44389  icccncfext  46629  stoweidlem14  46756  stoweidlem34  46776  ltnltne  48064  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  ply1mulgsumlem2  49195