Theorem eluzfz2 13592

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 12913	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12918	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13579	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 686	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  ℤcz 12639  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-pre-lttri 11258

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  eluzfz2b  13593  elfzubelfz  13596  fzopth  13621  fzsuc  13631  fseq1p1m1  13658  fzm1  13664  fzneuz  13665  fzoend  13807  uzindi  14033  seqcl2  14071  seqfveq2  14075  seqshft2  14079  monoord  14083  monoord2  14084  seqsplit  14086  seqcaopr3  14088  seqf1olem2a  14091  seqf1olem1  14092  seqf1olem2  14093  seqid2  14099  seqhomo  14100  seqcoll  14513  seqcoll2  14514  wrdeqs1cat  14768  pfxccatin12lem2  14779  pfxccatin12lem3  14780  splid  14801  spllen  14802  splval2  14805  summolem2a  15763  fsumm1  15799  telfsumo  15850  telfsumo2  15851  fsumparts  15854  prodfn0  15942  prodfrec  15943  prodmolem2a  15982  fprodm1  16015  sadadd  16513  sadass  16517  smuval2  16528  vdwlem6  17033  efgredleme  19785  efgredlemc  19787  efgcpbllemb  19797  frgpuplem  19814  telgsumfzslem  20030  telgsumfzs  20031  pmatcollpw3fi1lem1  22813  chfacfisf  22881  chfacfisfcpmat  22882  iscmet3lem1  25344  iscmet3lem2  25345  voliunlem1  25604  volsup  25610  mbfi1fseqlem3  25772  wilthlem2  27130  wilthlem3  27131  chtub  27274  dchrisum0flb  27572  pntpbnd1  27648  pntlemf  27667  spthonepeq  29788  wwlksnext  29926  2clwwlk2clwwlklem  30378  clwwlknonclwlknonf1o  30394  wrdsplex  32902  cycpmco2f1  33117  submatres  33752  madjusmdetlem1  33773  madjusmdetlem2  33774  madjusmdetlem3  33775  madjusmdetlem4  33776  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfrci  34492  gsumnunsn  34518  swrdrevpfx  35084  cvmliftlem10  35262  supfz  35691  fwddifnp1  36129  poimirlem3  37583  poimirlem4  37584  poimirlem16  37596  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem31  37611  volsupnfl  37625  sdclem2  37702  fdc  37705  mettrifi  37717  iunincfi  44996  monoordxrv  45397  monoord2xrv  45399  fmul01lt1lem2  45506  limsupubuzlem  45633  dvnmul  45864  dvnprodlem3  45869  stoweidlem3  45924  stoweidlem11  45932  stoweidlem17  45938  stoweidlem34  45955  fourierdlem15  46043  fourierdlem25  46053  fourierdlem50  46077  fourierdlem52  46079  fourierdlem54  46081  fourierdlem65  46092  fourierdlem81  46108  fourierdlem92  46119  fourierdlem102  46129  fourierdlem111  46138  fourierdlem113  46140  fourierdlem114  46141  etransclem35  46190  sge0p1  46335  carageniuncllem1  46442  caratheodorylem1  46447  smfmullem4  46715  ssfz12  47229  elfzlble  47235  smonoord  47245