MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzsn Structured version   Unicode version

Theorem fzsn 11848
Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
fzsn  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )

Proof of Theorem fzsn
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 elfz1eq 11818 . . . 4  |-  ( k  e.  ( M ... M )  ->  k  =  M )
2 elfz3 11817 . . . . 5  |-  ( M  e.  ZZ  ->  M  e.  ( M ... M
) )
3 eleq1 2495 . . . . 5  |-  ( k  =  M  ->  (
k  e.  ( M ... M )  <->  M  e.  ( M ... M ) ) )
42, 3syl5ibrcom 225 . . . 4  |-  ( M  e.  ZZ  ->  (
k  =  M  -> 
k  e.  ( M ... M ) ) )
51, 4impbid2 207 . . 3  |-  ( M  e.  ZZ  ->  (
k  e.  ( M ... M )  <->  k  =  M ) )
6 elsn 4012 . . 3  |-  ( k  e.  { M }  <->  k  =  M )
75, 6syl6bbr 266 . 2  |-  ( M  e.  ZZ  ->  (
k  e.  ( M ... M )  <->  k  e.  { M } ) )
87eqrdv 2419 1  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872   {csn 3998  (class class class)co 6306   ZZcz 10945   ...cfz 11792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-pre-lttri 9621  ax-pre-lttrn 9622
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-1st 6808  df-2nd 6809  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-neg 9871  df-z 10946  df-uz 11168  df-fz 11793
This theorem is referenced by:  fzsuc  11851  fzpred  11852  fzpr  11859  fzsuc2  11861  1fv  11916  fzosn  11991  seqf1o  12261  hashsng  12556  sumsn  13807  fsum1  13808  fsumm1  13812  fsum1p  13814  prodsn  14016  fprod1  14017  prodsnf  14018  fprod1p  14022  fprodabs  14028  binomfallfac  14094  ef0lem  14133  fprodefsum  14149  phi1  14721  4sqlem19  14913  vdwlem8  14938  strle1  15221  gsumws1  16623  telgsumfzs  17619  srgbinom  17778  psrbaglefi  18596  pmatcollpw3fi1lem1  19809  pmatcollpw3fi1  19811  imasdsf1olem  21387  voliunlem1  22502  ply1termlem  23156  pntpbnd1  24423  0spth  25300  eupa0  25701  iuninc  28179  fzspl  28375  esumfzf  28899  ballotlemfc0  29334  ballotlemfcc  29335  plymulx0  29445  signstf0  29466  subfac1  29910  subfacp1lem1  29911  subfacp1lem5  29916  subfacp1lem6  29917  cvmliftlem10  30026  fwddifn0  30937  poimirlem2  31907  poimirlem3  31908  poimirlem4  31909  poimirlem6  31911  poimirlem7  31912  poimirlem13  31918  poimirlem14  31919  poimirlem16  31921  poimirlem17  31922  poimirlem18  31923  poimirlem19  31924  poimirlem20  31925  poimirlem21  31926  poimirlem22  31927  poimirlem26  31931  poimirlem28  31933  poimirlem31  31936  poimirlem32  31937  sdclem1  32037  fdc  32039  trclfvdecomr  36291  sumsnd  37321  fzdifsuc2  37485  sumsnf  37590  dvnmul  37759  stoweidlem17  37818  carageniuncllem1  38251  caratheodorylem1  38256  hoidmvlelem3  38324  fzopredsuc  38591  nnsum3primesprm  38756
  Copyright terms: Public domain W3C validator