plyco0

Description: Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Assertion	plyco0	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$

Proof

Step	Hyp	Ref	Expression
1		simprr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to A (k) \neq 0$
2		ffun	$⊢ A : ℕ_{0} ⟶ ℂ \to Fun A$
3	2	adantl	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to Fun A$
4		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
5	4	adantr	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N + 1 \in ℕ_{0}$
6		eluznn0	$⊢ (N + 1 \in ℕ_{0} \land k \in ℤ_{\geq (N + 1)}) \to k \in ℕ_{0}$
7	6	ex	$⊢ N + 1 \in ℕ_{0} \to (k \in ℤ_{\geq (N + 1)} \to k \in ℕ_{0})$
8	5 7	syl	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (k \in ℤ_{\geq (N + 1)} \to k \in ℕ_{0})$
9	8	ssrdv	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to ℤ_{\geq (N + 1)} \subseteq ℕ_{0}$
10		fdm	$⊢ A : ℕ_{0} ⟶ ℂ \to dom A = ℕ_{0}$
11	10	adantl	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to dom A = ℕ_{0}$
12	9 11	sseqtrrd	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to ℤ_{\geq (N + 1)} \subseteq dom A$
13		funfvima2	$⊢ (Fun A \land ℤ_{\geq (N + 1)} \subseteq dom A) \to (k \in ℤ_{\geq (N + 1)} \to A (k) \in A [ℤ_{\geq (N + 1)}])$
14	3 12 13	syl2anc	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (k \in ℤ_{\geq (N + 1)} \to A (k) \in A [ℤ_{\geq (N + 1)}])$
15	14	ad2antrr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (k \in ℤ_{\geq (N + 1)} \to A (k) \in A [ℤ_{\geq (N + 1)}])$
16		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
17	16	adantr	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N \in ℤ$
18	17	peano2zd	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N + 1 \in ℤ$
19	18	ad2antrr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to N + 1 \in ℤ$
20		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
21	20	ad2antrl	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to k \in ℤ$
22		eluz	$⊢ (N + 1 \in ℤ \land k \in ℤ) \to (k \in ℤ_{\geq (N + 1)} \leftrightarrow N + 1 \leq k)$
23	19 21 22	syl2anc	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (k \in ℤ_{\geq (N + 1)} \leftrightarrow N + 1 \leq k)$
24		simplr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to A [ℤ_{\geq (N + 1)}] = \{0\}$
25	24	eleq2d	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (A (k) \in A [ℤ_{\geq (N + 1)}] \leftrightarrow A (k) \in \{0\})$
26		fvex	$⊢ A (k) \in V$
27	26	elsn	$⊢ A (k) \in \{0\} \leftrightarrow A (k) = 0$
28	25 27	bitrdi	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (A (k) \in A [ℤ_{\geq (N + 1)}] \leftrightarrow A (k) = 0)$
29	15 23 28	3imtr3d	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (N + 1 \leq k \to A (k) = 0)$
30	29	necon3ad	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (A (k) \neq 0 \to \neg N + 1 \leq k)$
31	1 30	mpd	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to \neg N + 1 \leq k$
32		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
33	32	ad2antrl	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to k \in ℝ$
34	18	zred	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N + 1 \in ℝ$
35	34	ad2antrr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to N + 1 \in ℝ$
36	33 35	ltnled	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (k < N + 1 \leftrightarrow \neg N + 1 \leq k)$
37	31 36	mpbird	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to k < N + 1$
38	17	ad2antrr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to N \in ℤ$
39		zleltp1	$⊢ (k \in ℤ \land N \in ℤ) \to (k \leq N \leftrightarrow k < N + 1)$
40	21 38 39	syl2anc	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to (k \leq N \leftrightarrow k < N + 1)$
41	37 40	mpbird	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land (k \in ℕ_{0} \land A (k) \neq 0)) \to k \leq N$
42	41	expr	$⊢ (((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \land k \in ℕ_{0}) \to (A (k) \neq 0 \to k \leq N)$
43	42	ralrimiva	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land A [ℤ_{\geq (N + 1)}] = \{0\}) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)$
44		simpr	$⊢ (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)}) \to n \in ℤ_{\geq (N + 1)}$
45		eluznn0	$⊢ (N + 1 \in ℕ_{0} \land n \in ℤ_{\geq (N + 1)}) \to n \in ℕ_{0}$
46	5 44 45	syl2an	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to n \in ℕ_{0}$
47		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
48	47	adantr	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N \in ℝ$
49	48	adantr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to N \in ℝ$
50	34	adantr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to N + 1 \in ℝ$
51	46	nn0red	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to n \in ℝ$
52	49	ltp1d	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to N < N + 1$
53		eluzle	$⊢ n \in ℤ_{\geq (N + 1)} \to N + 1 \leq n$
54	53	ad2antll	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to N + 1 \leq n$
55	49 50 51 52 54	ltletrd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to N < n$
56	49 51	ltnled	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to (N < n \leftrightarrow \neg n \leq N)$
57	55 56	mpbid	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to \neg n \leq N$
58		fveq2	$⊢ k = n \to A (k) = A (n)$
59	58	neeq1d	$⊢ k = n \to (A (k) \neq 0 \leftrightarrow A (n) \neq 0)$
60		breq1	$⊢ k = n \to (k \leq N \leftrightarrow n \leq N)$
61	59 60	imbi12d	$⊢ k = n \to ((A (k) \neq 0 \to k \leq N) \leftrightarrow (A (n) \neq 0 \to n \leq N))$
62		simprl	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)$
63	61 62 46	rspcdva	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to (A (n) \neq 0 \to n \leq N)$
64	63	necon1bd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to (\neg n \leq N \to A (n) = 0)$
65	57 64	mpd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to A (n) = 0$
66		ffn	$⊢ A : ℕ_{0} ⟶ ℂ \to A Fn ℕ_{0}$
67	66	ad2antlr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to A Fn ℕ_{0}$
68		fniniseg	$⊢ A Fn ℕ_{0} \to (n \in A^{-1} [\{0\}] \leftrightarrow (n \in ℕ_{0} \land A (n) = 0))$
69	67 68	syl	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to (n \in A^{-1} [\{0\}] \leftrightarrow (n \in ℕ_{0} \land A (n) = 0))$
70	46 65 69	mpbir2and	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land (\forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N) \land n \in ℤ_{\geq (N + 1)})) \to n \in A^{-1} [\{0\}]$
71	70	expr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to (n \in ℤ_{\geq (N + 1)} \to n \in A^{-1} [\{0\}])$
72	71	ssrdv	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to ℤ_{\geq (N + 1)} \subseteq A^{-1} [\{0\}]$
73		funimass3	$⊢ (Fun A \land ℤ_{\geq (N + 1)} \subseteq dom A) \to (A [ℤ_{\geq (N + 1)}] \subseteq \{0\} \leftrightarrow ℤ_{\geq (N + 1)} \subseteq A^{-1} [\{0\}])$
74	3 12 73	syl2anc	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N + 1)}] \subseteq \{0\} \leftrightarrow ℤ_{\geq (N + 1)} \subseteq A^{-1} [\{0\}])$
75	74	adantr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to (A [ℤ_{\geq (N + 1)}] \subseteq \{0\} \leftrightarrow ℤ_{\geq (N + 1)} \subseteq A^{-1} [\{0\}])$
76	72 75	mpbird	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to A [ℤ_{\geq (N + 1)}] \subseteq \{0\}$
77	48	ltp1d	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N < N + 1$
78	48 34	ltnled	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (N < N + 1 \leftrightarrow \neg N + 1 \leq N)$
79	77 78	mpbid	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to \neg N + 1 \leq N$
80	79	adantr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to \neg N + 1 \leq N$
81		fveq2	$⊢ k = N + 1 \to A (k) = A (N + 1)$
82	81	neeq1d	$⊢ k = N + 1 \to (A (k) \neq 0 \leftrightarrow A (N + 1) \neq 0)$
83		breq1	$⊢ k = N + 1 \to (k \leq N \leftrightarrow N + 1 \leq N)$
84	82 83	imbi12d	$⊢ k = N + 1 \to ((A (k) \neq 0 \to k \leq N) \leftrightarrow (A (N + 1) \neq 0 \to N + 1 \leq N))$
85	84	rspcva	$⊢ (N + 1 \in ℕ_{0} \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to (A (N + 1) \neq 0 \to N + 1 \leq N)$
86	5 85	sylan	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to (A (N + 1) \neq 0 \to N + 1 \leq N)$
87	86	necon1bd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to (\neg N + 1 \leq N \to A (N + 1) = 0)$
88	80 87	mpd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to A (N + 1) = 0$
89		uzid	$⊢ N + 1 \in ℤ \to N + 1 \in ℤ_{\geq (N + 1)}$
90	18 89	syl	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to N + 1 \in ℤ_{\geq (N + 1)}$
91		funfvima2	$⊢ (Fun A \land ℤ_{\geq (N + 1)} \subseteq dom A) \to (N + 1 \in ℤ_{\geq (N + 1)} \to A (N + 1) \in A [ℤ_{\geq (N + 1)}])$
92	3 12 91	syl2anc	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (N + 1 \in ℤ_{\geq (N + 1)} \to A (N + 1) \in A [ℤ_{\geq (N + 1)}])$
93	90 92	mpd	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to A (N + 1) \in A [ℤ_{\geq (N + 1)}]$
94	93	adantr	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to A (N + 1) \in A [ℤ_{\geq (N + 1)}]$
95	88 94	eqeltrrd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to 0 \in A [ℤ_{\geq (N + 1)}]$
96	95	snssd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to \{0\} \subseteq A [ℤ_{\geq (N + 1)}]$
97	76 96	eqssd	$⊢ ((N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \land \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N)) \to A [ℤ_{\geq (N + 1)}] = \{0\}$
98	43 97	impbida	$⊢ (N \in ℕ_{0} \land A : ℕ_{0} ⟶ ℂ) \to (A [ℤ_{\geq (N + 1)}] = \{0\} \leftrightarrow \forall k \in ℕ_{0} (A (k) \neq 0 \to k \leq N))$

Metamath Proof Explorer

Theorem plyco0

Proof