Theorem fzossz

Description: A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Assertion	fzossz	|- ( M ..^ N ) C_ ZZ

Proof

Step	Hyp	Ref	Expression
1		fzossfz	|- ( M ..^ N ) C_ ( M ... N )
2		fzssz	|- ( M ... N ) C_ ZZ
3	1 2	sstri	|- ( M ..^ N ) C_ ZZ