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 ) C_ RR

Proof

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