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 MN

Proof

Step Hyp Ref Expression
1 fzssz MN
2 zssre
3 1 2 sstri MN