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*