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 ⊆ ℂ

Proof

Step Hyp Ref Expression
1 fzssz ⊢ M … N ⊆ ℤ
2 zsscn ⊢ ℤ ⊆ ℂ
3 1 2 sstri ⊢ M … N ⊆ ℂ