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

Metamath Proof Explorer

Theorem suppssfz

Description: Condition for a function over the nonnegative integers to have a support contained in a finite set of sequential integers. (Contributed by AV, 9-Oct-2019)

Ref Expression
Hypotheses suppssfz.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
suppssfz.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
suppssfz.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
suppssfz.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
Assertion suppssfz ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )

Proof

Step Hyp Ref Expression
1 suppssfz.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
2 suppssfz.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) )
3 suppssfz.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 suppssfz.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
5 elmapfn ⊢ ( 𝐹 ∈ ( 𝐵 ↑m ℕ0 ) → 𝐹 Fn ℕ0 )
6 2 5 syl ⊢ ( 𝜑 → 𝐹 Fn ℕ0 )
7 nn0ex ⊢ ℕ0 ∈ V
8 7 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
9 6 8 1 3jca ⊢ ( 𝜑 → ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) )
11 elsuppfn ⊢ ( ( 𝐹 Fn ℕ0 ∧ ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉 ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) ) )
13 breq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑆 < 𝑥 ↔ 𝑆 < 𝑛 ) )
14 fveqeq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝐹 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑛 ) = 𝑍 ) )
15 13 14 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ↔ ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) ) )
16 15 rspcva ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ∈ ℕ0 )
18 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑆 ∈ ℕ0 )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑆 ∈ ℕ0 )
20 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
21 nn0re ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ℝ )
22 3 21 syl ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
23 lenlt ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( 𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛 ) )
24 20 22 23 syl2anr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛 ) )
25 24 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ≤ 𝑆 )
26 elfz2nn0 ⊢ ( 𝑛 ∈ ( 0 ... 𝑆 ) ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0 ∧ 𝑛 ≤ 𝑆 ) )
27 17 19 25 26 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → 𝑛 ∈ ( 0 ... 𝑆 ) )
28 27 a1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑆 < 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
29 28 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ¬ 𝑆 < 𝑛 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
30 eqneqall ⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑍 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
32 29 31 jad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
33 32 com23 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
34 33 ex ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
35 34 com14 ⊢ ( ( 𝑆 < 𝑛 → ( 𝐹 ‘ 𝑛 ) = 𝑍 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
36 16 35 syl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
37 36 ex ⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) ) )
38 37 pm2.43a ⊢ ( 𝑛 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
39 38 com23 ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) ) )
40 39 imp ⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝜑 → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
41 40 com13 ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) ) )
42 41 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≠ 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
43 12 42 sylbid ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑛 ∈ ( 𝐹 supp 𝑍 ) → 𝑛 ∈ ( 0 ... 𝑆 ) ) )
44 43 ssrdv ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝑆 < 𝑥 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )
45 4 44 mpdan ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) )