Theorem suppssnn0

Description: Show that the support of a function is contained in an half-open nonnegative integer range. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	suppssnn0.f	|- ( ph -> F Fn NN0 )
	suppssnn0.n	|- ( ( ( ph /\ k e. NN0 ) /\ N <_ k ) -> ( F ` k ) = Z )
	suppssnn0.1	|- ( ph -> N e. ZZ )
Assertion	suppssnn0	|- ( ph -> ( F supp Z ) C_ ( 0 ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		suppssnn0.f	|- ( ph -> F Fn NN0 )
2		suppssnn0.n	|- ( ( ( ph /\ k e. NN0 ) /\ N <_ k ) -> ( F ` k ) = Z )
3		suppssnn0.1	|- ( ph -> N e. ZZ )
4		dffn3	|- ( F Fn NN0 <-> F : NN0 --> ran F )
5	1 4	sylib	|- ( ph -> F : NN0 --> ran F )
6		simpl	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ph )
7		eldifi	|- ( k e. ( NN0 \ ( 0 ..^ N ) ) -> k e. NN0 )
8	7	adantl	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. NN0 )
9	3	zred	|- ( ph -> N e. RR )
10	9	adantr	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N e. RR )
11	8	nn0red	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. RR )
12	3	adantr	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N e. ZZ )
13		simpr	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> k e. ( NN0 \ ( 0 ..^ N ) ) )
14	12 13	nn0difffzod	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> -. k < N )
15	10 11 14	nltled	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> N <_ k )
16	6 8 15 2	syl21anc	|- ( ( ph /\ k e. ( NN0 \ ( 0 ..^ N ) ) ) -> ( F ` k ) = Z )
17	5 16	suppss	|- ( ph -> ( F supp Z ) C_ ( 0 ..^ N ) )