Metamath Proof Explorer


Theorem zssxr

Description: The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion zssxr ⊢ ℤ ⊆ ℝ *

Proof

Step Hyp Ref Expression
1 zssre ⊢ ℤ ⊆ ℝ
2 ressxr ⊢ ℝ ⊆ ℝ *
3 1 2 sstri ⊢ ℤ ⊆ ℝ *