Theorem eluzfz2 13434

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
eluzfz2	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Proof of Theorem eluzfz2

Step	Hyp	Ref	Expression
1		eluzelz 12748	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12753	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13421	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 687	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6486  (class class class)co 7352  ℤcz 12475  ℤ_≥cuz 12738  ...cfz 13409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-pre-lttri 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-neg 11354  df-z 12476  df-uz 12739  df-fz 13410

This theorem is referenced by:  eluzfz2b  13435  elfzubelfz  13438  fzopth  13463  fzsuc  13473  fseq1p1m1  13500  fzm1  13509  fzneuz  13510  fzoend  13659  uzindi  13891  seqcl2  13929  seqfveq2  13933  seqshft2  13937  monoord  13941  monoord2  13942  seqsplit  13944  seqcaopr3  13946  seqf1olem2a  13949  seqf1olem1  13950  seqf1olem2  13951  seqid2  13957  seqhomo  13958  seqcoll  14373  seqcoll2  14374  wrdeqs1cat  14629  pfxccatin12lem2  14640  pfxccatin12lem3  14641  splid  14662  spllen  14663  splval2  14666  summolem2a  15624  fsumm1  15660  telfsumo  15711  telfsumo2  15712  fsumparts  15715  prodfn0  15803  prodfrec  15804  prodmolem2a  15843  fprodm1  15876  sadadd  16380  sadass  16384  smuval2  16395  vdwlem6  16900  efgredleme  19657  efgredlemc  19659  efgcpbllemb  19669  frgpuplem  19686  telgsumfzslem  19902  telgsumfzs  19903  pmatcollpw3fi1lem1  22702  chfacfisf  22770  chfacfisfcpmat  22771  iscmet3lem1  25219  iscmet3lem2  25220  voliunlem1  25479  volsup  25485  mbfi1fseqlem3  25646  wilthlem2  27007  wilthlem3  27008  chtub  27151  dchrisum0flb  27449  pntpbnd1  27525  pntlemf  27544  spthonepeq  29732  wwlksnext  29873  2clwwlk2clwwlklem  30328  clwwlknonclwlknonf1o  30344  wrdsplex  32924  cycpmco2f1  33100  submatres  33840  madjusmdetlem1  33861  madjusmdetlem2  33862  madjusmdetlem3  33863  madjusmdetlem4  33864  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemfrci  34562  gsumnunsn  34575  swrdrevpfx  35182  cvmliftlem10  35359  supfz  35794  fwddifnp1  36230  poimirlem3  37683  poimirlem4  37684  poimirlem16  37696  poimirlem19  37699  poimirlem20  37700  poimirlem23  37703  poimirlem31  37711  volsupnfl  37725  sdclem2  37802  fdc  37805  mettrifi  37817  iunincfi  45215  monoordxrv  45603  monoord2xrv  45605  fmul01lt1lem2  45709  limsupubuzlem  45834  dvnmul  46065  dvnprodlem3  46070  stoweidlem3  46125  stoweidlem11  46133  stoweidlem17  46139  stoweidlem34  46156  fourierdlem15  46244  fourierdlem25  46254  fourierdlem50  46278  fourierdlem52  46280  fourierdlem54  46282  fourierdlem65  46293  fourierdlem81  46309  fourierdlem92  46320  fourierdlem102  46330  fourierdlem111  46339  fourierdlem113  46341  fourierdlem114  46342  etransclem35  46391  sge0p1  46536  carageniuncllem1  46643  caratheodorylem1  46648  smfmullem4  46916  ssfz12  47438  elfzlble  47444  smonoord  47495  gpg3kgrtriexlem5  48211  gpg5grlim  48217  gpg5grlic  48218