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