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
|- ZZ C_ RR*

Proof

Step Hyp Ref Expression
1 zssre
 |-  ZZ C_ RR
2 ressxr
 |-  RR C_ RR*
3 1 2 sstri
 |-  ZZ C_ RR*