Metamath Proof Explorer

Theorem uzsscn

Description: An upper set of integers is a subset of the complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Assertion uzsscn 
|- ( ZZ>= ` M ) C_ CC

Proof

Step Hyp Ref Expression
1 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
2 ax-resscn 
 |-  RR C_ CC
3 1 2 sstri 
 |-  ( ZZ>= ` M ) C_ CC