Theorem elfzuz3 13435

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 13432	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simprbi 496	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  ℤ_≥cuz 12749  ...cfz 13421

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 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

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 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11365  df-z 12487  df-uz 12750  df-fz 13422

This theorem is referenced by:  elfzel2  13436  elfzle2  13442  peano2fzr  13451  fzsplit2  13463  fzsplit  13464  fznn0sub  13470  fzopth  13475  fzss1  13477  fzss2  13478  fzp1elp1  13491  predfz  13567  fzosplit  13606  fzoend  13671  fzofzp1b  13679  uzindi  13903  seqcl2  13941  seqfveq2  13945  monoord  13953  sermono  13955  seqsplit  13956  seqf1olem2  13963  seqid2  13969  seqhomo  13970  seqz  13971  bcval5  14239  seqcoll  14385  seqcoll2  14386  swrdval2  14568  pfxres  14601  pfxf  14602  spllen  14675  splfv2a  14677  repswpfx  14706  fsum0diag2  15704  climcndslem2  15771  prodfn0  15815  lcmflefac  16573  pcbc  16826  vdwlem2  16908  vdwlem5  16911  vdwlem6  16912  vdwlem8  16914  prmgaplem1  16975  pfxchn  18531  psgnunilem5  19421  efgsres  19665  efgredleme  19670  efgcpbllemb  19682  imasdsf1olem  24315  volsup  25511  dvn2bss  25886  dvtaylp  26332  wilth  27035  ftalem1  27037  ppisval2  27069  dvdsppwf1o  27150  logfaclbnd  27187  bposlem6  27254  wlkres  29691  fzsplit3  32822  wrdres  32966  pfxf1  32973  swrdrn2  32985  swrdrn3  32986  swrdf1  32987  swrdrndisj  32988  splfv3  32989  cycpmco2f1  33155  cycpmco2rn  33156  cycpmco2lem7  33163  ballotlemsima  34622  ballotlemfrc  34633  ballotlemfrceq  34635  fzssfzo  34645  signstres  34681  fsum2dsub  34713  revpfxsfxrev  35259  swrdrevpfx  35260  pfxwlk  35267  erdszelem7  35340  erdszelem8  35341  poimirlem1  37761  poimirlem2  37762  poimirlem3  37763  poimirlem4  37764  poimirlem7  37767  poimirlem12  37772  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem23  37783  poimirlem24  37784  poimirlem25  37785  poimirlem29  37789  poimirlem31  37791  mettrifi  37897  fzsplitnd  42175  aks6d1c2lem4  42320  bcc0  44523  iunincfi  45280  monoordxrv  45667  fmulcl  45769  fmul01lt1lem2  45773  dvnprodlem2  46133  stoweidlem11  46197  stoweidlem17  46203  fourierdlem15  46308  ssfz12  47502  smonoord  47559