Metamath Proof Explorer


Theorem fzssre

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

Ref Expression
Assertion fzssre M N

Proof

Step Hyp Ref Expression
1 fzssz M N
2 zssre
3 1 2 sstri M N