Metamath Proof Explorer

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 ⊢ φ → F Fn ℕ 0
suppssnn0.n ⊢ φ ∧ k ∈ ℕ 0 ∧ N ≤ k → F ⁡ k = Z
suppssnn0.1 ⊢ φ → N ∈ ℤ
Assertion suppssnn0 ⊢ φ → F supp Z ⊆ 0 ..^ N

Proof

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