Theorem elfzuz3 13253

Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

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

Proof of Theorem elfzuz3

Step	Hyp	Ref	Expression
1		elfzuzb 13250	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 497	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6433  (class class class)co 7275  ℤ_≥cuz 12582  ...cfz 13239

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-1st 7831  df-2nd 7832  df-neg 11208  df-z 12320  df-uz 12583  df-fz 13240

This theorem is referenced by:  elfzel2  13254  elfzle2  13260  peano2fzr  13269  fzsplit2  13281  fzsplit  13282  fznn0sub  13288  fzopth  13293  fzss1  13295  fzss2  13296  fzp1elp1  13309  predfz  13381  fzosplit  13420  fzoend  13478  fzofzp1b  13485  uzindi  13702  seqcl2  13741  seqfveq2  13745  monoord  13753  sermono  13755  seqsplit  13756  seqf1olem2  13763  seqid2  13769  seqhomo  13770  seqz  13771  bcval5  14032  seqcoll  14178  seqcoll2  14179  swrdval2  14359  pfxres  14392  pfxf  14393  spllen  14467  splfv2a  14469  repswpfx  14498  fsum0diag2  15495  climcndslem2  15562  prodfn0  15606  lcmflefac  16353  pcbc  16601  vdwlem2  16683  vdwlem5  16686  vdwlem6  16687  vdwlem8  16689  prmgaplem1  16750  psgnunilem5  19102  efgsres  19344  efgredleme  19349  efgcpbllemb  19361  imasdsf1olem  23526  volsup  24720  dvn2bss  25094  dvtaylp  25529  wilth  26220  ftalem1  26222  ppisval2  26254  dvdsppwf1o  26335  logfaclbnd  26370  bposlem6  26437  wlkres  28038  fzsplit3  31115  wrdres  31211  pfxf1  31216  swrdrn2  31226  swrdrn3  31227  swrdf1  31228  swrdrndisj  31229  splfv3  31230  cycpmco2f1  31391  cycpmco2rn  31392  cycpmco2lem7  31399  ballotlemsima  32482  ballotlemfrc  32493  ballotlemfrceq  32495  fzssfzo  32518  signstres  32554  fsum2dsub  32587  revpfxsfxrev  33077  swrdrevpfx  33078  pfxwlk  33085  erdszelem7  33159  erdszelem8  33160  poimirlem1  35778  poimirlem2  35779  poimirlem3  35780  poimirlem4  35781  poimirlem7  35784  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem23  35800  poimirlem24  35801  poimirlem25  35802  poimirlem29  35806  poimirlem31  35808  mettrifi  35915  fzsplitnd  39991  bcc0  41958  iunincfi  42644  monoordxrv  43022  fmulcl  43122  fmul01lt1lem2  43126  dvnprodlem2  43488  stoweidlem11  43552  stoweidlem17  43558  fourierdlem15  43663  ssfz12  44806  smonoord  44823