seqid

Description: Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for .+ ) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqid.1	$⊢ (φ \land x \in S) \to Z \underset{˙}{+} x = x$
	seqid.2	$⊢ φ \to Z \in S$
	seqid.3	$⊢ φ \to N \in ℤ_{\geq M}$
	seqid.4	$⊢ φ \to F (N) \in S$
	seqid.5	$⊢ (φ \land x \in (M \dots N - 1)) \to F (x) = Z$
Assertion	seqid	$⊢ φ \to {seq M (\underset{˙}{+}, F) ↾}_{ℤ_{\geq N}} = seq N (\underset{˙}{+}, F)$

Proof

Step	Hyp	Ref	Expression
1		seqid.1	$⊢ (φ \land x \in S) \to Z \underset{˙}{+} x = x$
2		seqid.2	$⊢ φ \to Z \in S$
3		seqid.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		seqid.4	$⊢ φ \to F (N) \in S$
5		seqid.5	$⊢ (φ \land x \in (M \dots N - 1)) \to F (x) = Z$
6		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
7		seq1	$⊢ N \in ℤ \to seq N (\underset{˙}{+}, F) (N) = F (N)$
8	3 6 7	3syl	$⊢ φ \to seq N (\underset{˙}{+}, F) (N) = F (N)$
9		seqeq1	$⊢ N = M \to seq N (\underset{˙}{+}, F) = seq M (\underset{˙}{+}, F)$
10	9	fveq1d	$⊢ N = M \to seq N (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (N)$
11	10	eqeq1d	$⊢ N = M \to (seq N (\underset{˙}{+}, F) (N) = F (N) \leftrightarrow seq M (\underset{˙}{+}, F) (N) = F (N))$
12	8 11	syl5ibcom	$⊢ φ \to (N = M \to seq M (\underset{˙}{+}, F) (N) = F (N))$
13		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
14	3 13	syl	$⊢ φ \to M \in ℤ$
15		seqm1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N)$
16	14 15	sylan	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N)$
17		oveq2	$⊢ x = Z \to Z \underset{˙}{+} x = Z \underset{˙}{+} Z$
18		id	$⊢ x = Z \to x = Z$
19	17 18	eqeq12d	$⊢ x = Z \to (Z \underset{˙}{+} x = x \leftrightarrow Z \underset{˙}{+} Z = Z)$
20	1	ralrimiva	$⊢ φ \to \forall x \in S Z \underset{˙}{+} x = x$
21	19 20 2	rspcdva	$⊢ φ \to Z \underset{˙}{+} Z = Z$
22	21	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to Z \underset{˙}{+} Z = Z$
23		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
24	14 23	sylan	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
25	5	adantlr	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land x \in (M \dots N - 1)) \to F (x) = Z$
26	22 24 25	seqid3	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N - 1) = Z$
27	26	oveq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N - 1) \underset{˙}{+} F (N) = Z \underset{˙}{+} F (N)$
28		oveq2	$⊢ x = F (N) \to Z \underset{˙}{+} x = Z \underset{˙}{+} F (N)$
29		id	$⊢ x = F (N) \to x = F (N)$
30	28 29	eqeq12d	$⊢ x = F (N) \to (Z \underset{˙}{+} x = x \leftrightarrow Z \underset{˙}{+} F (N) = F (N))$
31	20	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \forall x \in S Z \underset{˙}{+} x = x$
32	4	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to F (N) \in S$
33	30 31 32	rspcdva	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to Z \underset{˙}{+} F (N) = F (N)$
34	16 27 33	3eqtrd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (N) = F (N)$
35	34	ex	$⊢ φ \to (N \in ℤ_{\geq (M + 1)} \to seq M (\underset{˙}{+}, F) (N) = F (N))$
36		uzp1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
37	3 36	syl	$⊢ φ \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
38	12 35 37	mpjaod	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = F (N)$
39		eqidd	$⊢ (φ \land x \in ℤ_{\geq (N + 1)}) \to F (x) = F (x)$
40	3 38 39	seqfeq2	$⊢ φ \to {seq M (\underset{˙}{+}, F) ↾}_{ℤ_{\geq N}} = seq N (\underset{˙}{+}, F)$

Metamath Proof Explorer

Theorem seqid

Proof