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	$⊢ φ \to Z \in V$
	suppssfz.f	$⊢ φ \to F \in (B^{ℕ_{0}})$
	suppssfz.s	$⊢ φ \to S \in ℕ_{0}$
	suppssfz.b	$⊢ φ \to \forall x \in ℕ_{0} (S < x \to F (x) = Z)$
Assertion	suppssfz	$⊢ φ \to F supp Z \subseteq (0 \dots S)$

Proof

Step	Hyp	Ref	Expression
1		suppssfz.z	$⊢ φ \to Z \in V$
2		suppssfz.f	$⊢ φ \to F \in (B^{ℕ_{0}})$
3		suppssfz.s	$⊢ φ \to S \in ℕ_{0}$
4		suppssfz.b	$⊢ φ \to \forall x \in ℕ_{0} (S < x \to F (x) = Z)$
5		elmapfn	$⊢ F \in (B^{ℕ_{0}}) \to F Fn ℕ_{0}$
6	2 5	syl	$⊢ φ \to F Fn ℕ_{0}$
7		nn0ex	$⊢ ℕ_{0} \in V$
8	7	a1i	$⊢ φ \to ℕ_{0} \in V$
9	6 8 1	3jca	$⊢ φ \to (F Fn ℕ_{0} \land ℕ_{0} \in V \land Z \in V)$
10	9	adantr	$⊢ (φ \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to (F Fn ℕ_{0} \land ℕ_{0} \in V \land Z \in V)$
11		elsuppfn	$⊢ (F Fn ℕ_{0} \land ℕ_{0} \in V \land Z \in V) \to (n \in {supp}_{Z} (F) \leftrightarrow (n \in ℕ_{0} \land F (n) \neq Z))$
12	10 11	syl	$⊢ (φ \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to (n \in {supp}_{Z} (F) \leftrightarrow (n \in ℕ_{0} \land F (n) \neq Z))$
13		breq2	$⊢ x = n \to (S < x \leftrightarrow S < n)$
14		fveqeq2	$⊢ x = n \to (F (x) = Z \leftrightarrow F (n) = Z)$
15	13 14	imbi12d	$⊢ x = n \to ((S < x \to F (x) = Z) \leftrightarrow (S < n \to F (n) = Z))$
16	15	rspcva	$⊢ (n \in ℕ_{0} \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to (S < n \to F (n) = Z)$
17		simplr	$⊢ ((φ \land n \in ℕ_{0}) \land \neg S < n) \to n \in ℕ_{0}$
18	3	adantr	$⊢ (φ \land n \in ℕ_{0}) \to S \in ℕ_{0}$
19	18	adantr	$⊢ ((φ \land n \in ℕ_{0}) \land \neg S < n) \to S \in ℕ_{0}$
20		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
21		nn0re	$⊢ S \in ℕ_{0} \to S \in ℝ$
22	3 21	syl	$⊢ φ \to S \in ℝ$
23		lenlt	$⊢ (n \in ℝ \land S \in ℝ) \to (n \leq S \leftrightarrow \neg S < n)$
24	20 22 23	syl2anr	$⊢ (φ \land n \in ℕ_{0}) \to (n \leq S \leftrightarrow \neg S < n)$
25	24	biimpar	$⊢ ((φ \land n \in ℕ_{0}) \land \neg S < n) \to n \leq S$
26		elfz2nn0	$⊢ n \in (0 \dots S) \leftrightarrow (n \in ℕ_{0} \land S \in ℕ_{0} \land n \leq S)$
27	17 19 25 26	syl3anbrc	$⊢ ((φ \land n \in ℕ_{0}) \land \neg S < n) \to n \in (0 \dots S)$
28	27	a1d	$⊢ ((φ \land n \in ℕ_{0}) \land \neg S < n) \to (F (n) \neq Z \to n \in (0 \dots S))$
29	28	ex	$⊢ (φ \land n \in ℕ_{0}) \to (\neg S < n \to (F (n) \neq Z \to n \in (0 \dots S)))$
30		eqneqall	$⊢ F (n) = Z \to (F (n) \neq Z \to n \in (0 \dots S))$
31	30	a1i	$⊢ (φ \land n \in ℕ_{0}) \to (F (n) = Z \to (F (n) \neq Z \to n \in (0 \dots S)))$
32	29 31	jad	$⊢ (φ \land n \in ℕ_{0}) \to ((S < n \to F (n) = Z) \to (F (n) \neq Z \to n \in (0 \dots S)))$
33	32	com23	$⊢ (φ \land n \in ℕ_{0}) \to (F (n) \neq Z \to ((S < n \to F (n) = Z) \to n \in (0 \dots S)))$
34	33	ex	$⊢ φ \to (n \in ℕ_{0} \to (F (n) \neq Z \to ((S < n \to F (n) = Z) \to n \in (0 \dots S))))$
35	34	com14	$⊢ (S < n \to F (n) = Z) \to (n \in ℕ_{0} \to (F (n) \neq Z \to (φ \to n \in (0 \dots S))))$
36	16 35	syl	$⊢ (n \in ℕ_{0} \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to (n \in ℕ_{0} \to (F (n) \neq Z \to (φ \to n \in (0 \dots S))))$
37	36	ex	$⊢ n \in ℕ_{0} \to (\forall x \in ℕ_{0} (S < x \to F (x) = Z) \to (n \in ℕ_{0} \to (F (n) \neq Z \to (φ \to n \in (0 \dots S)))))$
38	37	pm2.43a	$⊢ n \in ℕ_{0} \to (\forall x \in ℕ_{0} (S < x \to F (x) = Z) \to (F (n) \neq Z \to (φ \to n \in (0 \dots S))))$
39	38	com23	$⊢ n \in ℕ_{0} \to (F (n) \neq Z \to (\forall x \in ℕ_{0} (S < x \to F (x) = Z) \to (φ \to n \in (0 \dots S))))$
40	39	imp	$⊢ (n \in ℕ_{0} \land F (n) \neq Z) \to (\forall x \in ℕ_{0} (S < x \to F (x) = Z) \to (φ \to n \in (0 \dots S)))$
41	40	com13	$⊢ φ \to (\forall x \in ℕ_{0} (S < x \to F (x) = Z) \to ((n \in ℕ_{0} \land F (n) \neq Z) \to n \in (0 \dots S)))$
42	41	imp	$⊢ (φ \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to ((n \in ℕ_{0} \land F (n) \neq Z) \to n \in (0 \dots S))$
43	12 42	sylbid	$⊢ (φ \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to (n \in {supp}_{Z} (F) \to n \in (0 \dots S))$
44	43	ssrdv	$⊢ (φ \land \forall x \in ℕ_{0} (S < x \to F (x) = Z)) \to F supp Z \subseteq (0 \dots S)$
45	4 44	mpdan	$⊢ φ \to F supp Z \subseteq (0 \dots S)$

Metamath Proof Explorer

Theorem suppssfz

Proof