This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 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 ..^ 𝑁 ) )