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 ( 𝑀 ... 𝑁 ) ⊆ ℂ

Proof

Step Hyp Ref Expression
1 fzssz ( 𝑀 ... 𝑁 ) ⊆ ℤ
2 zsscn ℤ ⊆ ℂ
3 1 2 sstri ( 𝑀 ... 𝑁 ) ⊆ ℂ