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	$$⊢\phi \to FFn{\mathbb{N}}_0$$
	suppssnn0.n	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge N\le k\right)\to F\left(k\right)=Z$$
	suppssnn0.1	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	suppssnn0	$$⊢\phi \to F\mathrm{supp}Z\subseteq \left(0..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		suppssnn0.f	$$⊢\phi \to FFn{\mathbb{N}}_0$$
2		suppssnn0.n	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge N\le k\right)\to F\left(k\right)=Z$$
3		suppssnn0.1	$$⊢\phi \to N\in \mathbb{Z}$$
4		dffn3	$$⊢FFn{\mathbb{N}}_0\leftrightarrow F:{\mathbb{N}}_0⟶\mathrm{ran}F$$
5	1 4	sylib	$$⊢\phi \to F:{\mathbb{N}}_0⟶\mathrm{ran}F$$
6		simpl	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to \phi$$
7		eldifi	$$⊢k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\to k\in {\mathbb{N}}_0$$
8	7	adantl	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\in {\mathbb{N}}_0$$
9	3	zred	$$⊢\phi \to N\in ℝ$$
10	9	adantr	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to N\in ℝ$$
11	8	nn0red	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\in ℝ$$
12	3	adantr	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to N\in \mathbb{Z}$$
13		simpr	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)$$
14	12 13	nn0difffzod	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to \neg k<N$$
15	10 11 14	nltled	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to N\le k$$
16	6 8 15 2	syl21anc	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to F\left(k\right)=Z$$
17	5 16	suppss	$$⊢\phi \to F\mathrm{supp}Z\subseteq \left(0..^N\right)$$