![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzsn | Structured version Visualization version GIF version |
Description: A finite interval of integers with one element. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
fzsn | ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfz1eq 13512 | . . . 4 ⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀) | |
2 | elfz3 13511 | . . . . 5 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (𝑀...𝑀)) | |
3 | eleq1 2822 | . . . . 5 ⊢ (𝑘 = 𝑀 → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑀 ∈ (𝑀...𝑀))) | |
4 | 2, 3 | syl5ibrcom 246 | . . . 4 ⊢ (𝑀 ∈ ℤ → (𝑘 = 𝑀 → 𝑘 ∈ (𝑀...𝑀))) |
5 | 1, 4 | impbid2 225 | . . 3 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 = 𝑀)) |
6 | velsn 4645 | . . 3 ⊢ (𝑘 ∈ {𝑀} ↔ 𝑘 = 𝑀) | |
7 | 5, 6 | bitr4di 289 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑘 ∈ (𝑀...𝑀) ↔ 𝑘 ∈ {𝑀})) |
8 | 7 | eqrdv 2731 | 1 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 {csn 4629 (class class class)co 7409 ℤcz 12558 ...cfz 13484 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-1st 7975 df-2nd 7976 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-neg 11447 df-z 12559 df-uz 12823 df-fz 13485 |
This theorem is referenced by: fzsuc 13548 fzpred 13549 fzpr 13556 fzsuc2 13559 fz0sn 13601 fz0sn0fz1 13618 fzosn 13703 seqf1o 14009 hashsng 14329 sumsnf 15689 fsum1 15693 fsumm1 15697 fsum1p 15699 prodsn 15906 fprod1 15907 prodsnf 15908 fprod1p 15912 fprodabs 15918 fprodefsum 16038 phi1 16706 vdwlem8 16921 strle1 17091 telgsumfzs 19857 pmatcollpw3fi1 22290 imasdsf1olem 23879 ehl1eudis 24937 voliunlem1 25067 ply1termlem 25717 pntpbnd1 27089 0wlkons1 29374 iuninc 31792 fzspl 32001 esumfzf 33067 ballotlemfc0 33491 ballotlemfcc 33492 plymulx0 33558 signstf0 33579 subfac1 34169 subfacp1lem1 34170 subfacp1lem5 34175 subfacp1lem6 34176 cvmliftlem10 34285 fwddifn0 35136 poimirlem2 36490 poimirlem3 36491 poimirlem4 36492 poimirlem6 36494 poimirlem7 36495 poimirlem13 36501 poimirlem14 36502 poimirlem16 36504 poimirlem17 36505 poimirlem18 36506 poimirlem19 36507 poimirlem20 36508 poimirlem21 36509 poimirlem22 36510 poimirlem26 36514 poimirlem28 36516 poimirlem31 36519 poimirlem32 36520 sdclem1 36611 fdc 36613 sticksstones9 40970 sticksstones11 40972 metakunt18 41002 metakunt20 41004 metakunt24 41008 trclfvdecomr 42479 k0004val0 42905 sumsnd 43710 fzdifsuc2 44020 dvnmul 44659 stoweidlem17 44733 carageniuncllem1 45237 caratheodorylem1 45242 hoidmvlelem3 45313 fzopredsuc 46031 sbgoldbo 46455 nnsum3primesprm 46458 |
Copyright terms: Public domain | W3C validator |