Metamath Proof Explorer
Description: A finite set of sequential integers that is a subset of NN0 .
(Contributed by Glauco Siliprandi, 5Apr2020)


Ref 
Expression 

Assertion 
fzssnn0 
⊢ ( 0 ... 𝑁 ) ⊆ ℕ_{0} 
Proof
Step 
Hyp 
Ref 
Expression 
1 

fzssuz 
⊢ ( 0 ... 𝑁 ) ⊆ ( ℤ_{≥} ‘ 0 ) 
2 

nn0uz 
⊢ ℕ_{0} = ( ℤ_{≥} ‘ 0 ) 
3 
2

eqcomi 
⊢ ( ℤ_{≥} ‘ 0 ) = ℕ_{0} 
4 
1 3

sseqtri 
⊢ ( 0 ... 𝑁 ) ⊆ ℕ_{0} 