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 *