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	⊢ ( 𝜑 → 𝐹 Fn ℕ0 )
	suppssnn0.n	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑘 ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
	suppssnn0.1	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	suppssnn0	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		suppssnn0.f	⊢ ( 𝜑 → 𝐹 Fn ℕ0 )
2		suppssnn0.n	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑘 ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
3		suppssnn0.1	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		dffn3	⊢ ( 𝐹 Fn ℕ0 ↔ 𝐹 : ℕ0 ⟶ ran 𝐹 )
5	1 4	sylib	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ran 𝐹 )
6		simpl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝜑 )
7		eldifi	⊢ ( 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
9	3	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℝ )
11	8	nn0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ℝ )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ∈ ℤ )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) )
14	12 13	nn0difffzod	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ¬ 𝑘 < 𝑁 )
15	10 11 14	nltled	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑁 ≤ 𝑘 )
16	6 8 15 2	syl21anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
17	5 16	suppss	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ..^ 𝑁 ) )