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

Theorem fzsn 13482
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 13451 . . . 4 (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀)
2 elfz3 13450 . . . . 5 (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀))
3 eleq1 2825 . . . . 5 (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀)))
42, 3syl5ibrcom 246 . . . 4 (𝑀 ∈ ℤ → (𝑘 = 𝑀𝑘 ∈ (𝑀...𝑀)))
51, 4impbid2 225 . . 3 (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀))
6 velsn 4602 . . 3 (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀)
75, 6bitr4di 288 . 2 (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀}))
87eqrdv 2734 1 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  {csn 4586  (class class class)co 7356  cz 12498  ...cfz 13423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-cnex 11106  ax-resscn 11107  ax-pre-lttri 11124  ax-pre-lttrn 11125
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7920  df-2nd 7921  df-er 8647  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194  df-neg 11387  df-z 12499  df-uz 12763  df-fz 13424
This theorem is referenced by:  fzsuc  13487  fzpred  13488  fzpr  13495  fzsuc2  13498  fz0sn  13540  fz0sn0fz1  13557  fzosn  13642  seqf1o  13948  hashsng  14268  sumsnf  15627  fsum1  15631  fsumm1  15635  fsum1p  15637  prodsn  15844  fprod1  15845  prodsnf  15846  fprod1p  15850  fprodabs  15856  fprodefsum  15976  phi1  16644  vdwlem8  16859  strle1  17029  telgsumfzs  19764  pmatcollpw3fi1  22135  imasdsf1olem  23724  ehl1eudis  24782  voliunlem1  24912  ply1termlem  25562  pntpbnd1  26932  0wlkons1  29012  iuninc  31426  fzspl  31637  esumfzf  32608  ballotlemfc0  33032  ballotlemfcc  33033  plymulx0  33099  signstf0  33120  subfac1  33712  subfacp1lem1  33713  subfacp1lem5  33718  subfacp1lem6  33719  cvmliftlem10  33828  fwddifn0  34739  poimirlem2  36070  poimirlem3  36071  poimirlem4  36072  poimirlem6  36074  poimirlem7  36075  poimirlem13  36081  poimirlem14  36082  poimirlem16  36084  poimirlem17  36085  poimirlem18  36086  poimirlem19  36087  poimirlem20  36088  poimirlem21  36089  poimirlem22  36090  poimirlem26  36094  poimirlem28  36096  poimirlem31  36099  poimirlem32  36100  sdclem1  36192  fdc  36194  sticksstones9  40552  sticksstones11  40554  metakunt18  40584  metakunt20  40586  metakunt24  40590  trclfvdecomr  41981  k0004val0  42407  sumsnd  43212  fzdifsuc2  43519  dvnmul  44155  stoweidlem17  44229  carageniuncllem1  44733  caratheodorylem1  44738  hoidmvlelem3  44809  fzopredsuc  45526  sbgoldbo  45950  nnsum3primesprm  45953
  Copyright terms: Public domain W3C validator