This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzsscn

Description: A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion fzsscn 
|- ( M ... N ) C_ CC

Proof

Step Hyp Ref Expression
1 fzssz 
 |-  ( M ... N ) C_ ZZ
2 zsscn 
 |-  ZZ C_ CC
3 1 2 sstri 
 |-  ( M ... N ) C_ CC