Theorem fzssuz 13510

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 13465	. 2 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀))
2	1	ssriv 3926	1 ⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀)

Syntax hints:   ⊆ wss 3890  ‘cfv 6492  (class class class)co 7360  ℤ_≥cuz 12779  ...cfz 13452

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 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

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 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 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-neg 11371  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  ltwefz  13916  seqcoll2  14418  caubnd  15312  climsup  15623  summolem2a  15668  fsumss  15678  fsumsers  15681  isumclim3  15712  binomlem  15785  prodmolem2a  15890  fprodntriv  15898  fprodss  15904  iprodclim3  15956  fprodefsum  16051  isprm3  16643  2prm  16652  prmreclem5  16882  4sqlem11  16917  gsumval3  19873  telgsums  19959  fz2ssnn0  32873  elrgspnlem2  33319  esumpcvgval  34238  esumcvg  34246  eulerpartlemsv3  34521  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemiex  34662  ballotlemsima  34676  ballotlemrv2  34682  fsum2dsub  34767  erdszelem4  35392  erdszelem8  35396  volsupnfl  38000  sdclem2  38077  geomcau  38094  diophin  43218  irrapxlem1  43268  fzssnn0  45767  iuneqfzuzlem  45782  fzossuz  45828  uzublem  45876  climinf  46054  sge0uzfsumgt  46890  iundjiun  46906  caratheodorylem1  46972