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

Theorem fzsn 12574
Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
fzsn (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})

Proof of Theorem fzsn
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 elfz1eq 12543 . . . 4 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2 elfz3 12542 . . . . 5 (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3 eleq1 2825 . . . . 5 (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
42, 3syl5ibrcom 237 . . . 4 (𝑀 ∈ ℤ → (𝑘 = 𝑀𝑘 ∈ (𝑀...𝑀)))
51, 4impbid2 216 . . 3 (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6 velsn 4335 . . 3 (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
75, 6syl6bbr 278 . 2 (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
87eqrdv 2756 1 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2137  {csn 4319  (class class class)co 6811  cz 11567  ...cfz 12517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-pre-lttri 10200  ax-pre-lttrn 10201
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-1st 7331  df-2nd 7332  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-neg 10459  df-z 11568  df-uz 11878  df-fz 12518
This theorem is referenced by:  fzsuc  12579  fzpred  12580  fzpr  12587  fzsuc2  12589  fz0sn  12631  fz0sn0fz1  12648  fzosn  12731  seqf1o  13034  hashsng  13349  sumsnf  14670  sumsn  14672  fsum1  14673  fsumm1  14677  fsum1p  14679  prodsn  14889  fprod1  14890  prodsnf  14891  fprod1p  14895  fprodabs  14901  binomfallfac  14969  ef0lem  15006  fprodefsum  15022  phi1  15678  4sqlem19  15867  vdwlem8  15892  strle1  16173  gsumws1  17575  telgsumfzs  18584  srgbinom  18743  pmatcollpw3fi1lem1  20791  pmatcollpw3fi1  20793  imasdsf1olem  22377  voliunlem1  23516  ply1termlem  24156  pntpbnd1  25472  0wlkons1  27271  iuninc  29684  fzspl  29857  esumfzf  30438  ballotlemfc0  30861  ballotlemfcc  30862  plymulx0  30931  signstf0  30952  subfac1  31465  subfacp1lem1  31466  subfacp1lem5  31471  subfacp1lem6  31472  cvmliftlem10  31581  fwddifn0  32575  poimirlem2  33722  poimirlem3  33723  poimirlem4  33724  poimirlem6  33726  poimirlem7  33727  poimirlem13  33733  poimirlem14  33734  poimirlem16  33736  poimirlem17  33737  poimirlem18  33738  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  poimirlem26  33746  poimirlem28  33748  poimirlem31  33751  poimirlem32  33752  sdclem1  33850  fdc  33852  trclfvdecomr  38520  k0004val0  38952  sumsnd  39682  fzdifsuc2  40021  dvnmul  40659  stoweidlem17  40735  carageniuncllem1  41239  caratheodorylem1  41244  hoidmvlelem3  41315  fzopredsuc  41841  sbgoldbo  42183  nnsum3primesprm  42186
  Copyright terms: Public domain W3C validator