Theorem elfzuz3 13470

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6494  (class class class)co 7362  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7937  df-2nd 7938  df-neg 11375  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  elfzel2  13471  elfzle2  13477  peano2fzr  13486  fzsplit2  13498  fzsplit  13499  fznn0sub  13505  fzopth  13510  fzss1  13512  fzss2  13513  fzp1elp1  13526  predfz  13602  fzosplit  13642  fzoend  13707  fzofzp1b  13715  uzindi  13939  seqcl2  13977  seqfveq2  13981  monoord  13989  sermono  13991  seqsplit  13992  seqf1olem2  13999  seqid2  14005  seqhomo  14006  seqz  14007  bcval5  14275  seqcoll  14421  seqcoll2  14422  swrdval2  14604  pfxres  14637  pfxf  14638  spllen  14711  splfv2a  14713  repswpfx  14742  fsum0diag2  15740  climcndslem2  15810  prodfn0  15854  lcmflefac  16612  pcbc  16866  vdwlem2  16948  vdwlem5  16951  vdwlem6  16952  vdwlem8  16954  prmgaplem1  17015  pfxchn  18571  psgnunilem5  19464  efgsres  19708  efgredleme  19713  efgcpbllemb  19725  imasdsf1olem  24352  volsup  25537  dvn2bss  25911  dvtaylp  26351  wilth  27052  ftalem1  27054  ppisval2  27086  dvdsppwf1o  27167  logfaclbnd  27203  bposlem6  27270  wlkres  29756  fzsplit3  32885  wrdres  33014  pfxf1  33021  swrdrn2  33033  swrdrn3  33034  swrdf1  33035  swrdrndisj  33036  splfv3  33037  cycpmco2f1  33204  cycpmco2rn  33205  cycpmco2lem7  33212  ballotlemsima  34680  ballotlemfrc  34691  ballotlemfrceq  34693  fzssfzo  34703  signstres  34739  fsum2dsub  34771  revpfxsfxrev  35318  swrdrevpfx  35319  pfxwlk  35326  erdszelem7  35399  erdszelem8  35400  poimirlem1  37960  poimirlem2  37961  poimirlem3  37962  poimirlem4  37963  poimirlem7  37966  poimirlem12  37971  poimirlem15  37974  poimirlem16  37975  poimirlem17  37976  poimirlem19  37978  poimirlem20  37979  poimirlem23  37982  poimirlem24  37983  poimirlem25  37984  poimirlem29  37988  poimirlem31  37990  mettrifi  38096  fzsplitnd  42439  aks6d1c2lem4  42584  bcc0  44789  iunincfi  45546  monoordxrv  45931  fmulcl  46033  fmul01lt1lem2  46037  dvnprodlem2  46397  stoweidlem11  46461  stoweidlem17  46467  fourierdlem15  46572  ssfz12  47778  smonoord  47841