Theorem fzssuz 13481

Description: A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.)

Assertion

Ref	Expression
fzssuz	⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)

Proof of Theorem fzssuz

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzuz 13436	. 2 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	ssriv 3937	1 ⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)

Syntax hints:   ⊆ wss 3901  ‘cfv 6492  (class class class)co 7358  ℤ_≥cuz 12751  ...cfz 13423

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-neg 11367  df-z 12489  df-uz 12752  df-fz 13424

This theorem is referenced by:  ltwefz  13886  seqcoll2  14388  caubnd  15282  climsup  15593  summolem2a  15638  fsumss  15648  fsumsers  15651  isumclim3  15682  binomlem  15752  prodmolem2a  15857  fprodntriv  15865  fprodss  15871  iprodclim3  15923  fprodefsum  16018  isprm3  16610  2prm  16619  prmreclem5  16848  4sqlem11  16883  gsumval3  19836  telgsums  19922  fz2ssnn0  32865  elrgspnlem2  33325  esumpcvgval  34235  esumcvg  34243  eulerpartlemsv3  34518  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemiex  34659  ballotlemsima  34673  ballotlemrv2  34679  fsum2dsub  34764  erdszelem4  35388  erdszelem8  35392  volsupnfl  37862  sdclem2  37939  geomcau  37956  diophin  43010  irrapxlem1  43060  fzssnn0  45560  iuneqfzuzlem  45575  fzossuz  45621  uzublem  45670  climinf  45848  sge0uzfsumgt  46684  iundjiun  46700  caratheodorylem1  46766