seqid2

Description: The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for .+ ) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		seqid2.1	$⊢ (φ \land x \in S) \to x \underset{˙}{+} Z = x$
2		seqid2.2	$⊢ φ \to K \in ℤ_{\geq M}$
3		seqid2.3	$⊢ φ \to N \in ℤ_{\geq K}$
4		seqid2.4	$⊢ φ \to seq M (\underset{˙}{+}, F) (K) \in S$
5		seqid2.5	$⊢ (φ \land x \in (K + 1 \dots N)) \to F (x) = Z$
6		eluzfz2	$⊢ N \in ℤ_{\geq K} \to N \in (K \dots N)$
7	3 6	syl	$⊢ φ \to N \in (K \dots N)$
8		eleq1	$⊢ x = K \to (x \in (K \dots N) \leftrightarrow K \in (K \dots N))$
9		fveq2	$⊢ x = K \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (K)$
10	9	eqeq2d	$⊢ x = K \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K))$
11	8 10	imbi12d	$⊢ x = K \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x)) \leftrightarrow (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K)))$
12	11	imbi2d	$⊢ x = K \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x))) \leftrightarrow (φ \to (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K))))$
13		eleq1	$⊢ x = n \to (x \in (K \dots N) \leftrightarrow n \in (K \dots N))$
14		fveq2	$⊢ x = n \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n)$
15	14	eqeq2d	$⊢ x = n \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n))$
16	13 15	imbi12d	$⊢ x = n \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x)) \leftrightarrow (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n)))$
17	16	imbi2d	$⊢ x = n \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x))) \leftrightarrow (φ \to (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n))))$
18		eleq1	$⊢ x = n + 1 \to (x \in (K \dots N) \leftrightarrow n + 1 \in (K \dots N))$
19		fveq2	$⊢ x = n + 1 \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n + 1)$
20	19	eqeq2d	$⊢ x = n + 1 \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1))$
21	18 20	imbi12d	$⊢ x = n + 1 \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x)) \leftrightarrow (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1)))$
22	21	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x))) \leftrightarrow (φ \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1))))$
23		eleq1	$⊢ x = N \to (x \in (K \dots N) \leftrightarrow N \in (K \dots N))$
24		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (N)$
25	24	eqeq2d	$⊢ x = N \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N))$
26	23 25	imbi12d	$⊢ x = N \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x)) \leftrightarrow (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N)))$
27	26	imbi2d	$⊢ x = N \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (x))) \leftrightarrow (φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N))))$
28		eqidd	$⊢ K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K)$
29	28	2a1i	$⊢ K \in ℤ \to (φ \to (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K)))$
30		peano2fzr	$⊢ (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N)) \to n \in (K \dots N)$
31	30	adantl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n \in (K \dots N)$
32	31	expr	$⊢ (φ \land n \in ℤ_{\geq K}) \to (n + 1 \in (K \dots N) \to n \in (K \dots N))$
33	32	imim1d	$⊢ (φ \land n \in ℤ_{\geq K}) \to ((n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n)) \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n)))$
34		oveq1	$⊢ seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n) \to seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} F (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
35		fveqeq2	$⊢ x = n + 1 \to (F (x) = Z \leftrightarrow F (n + 1) = Z)$
36	5	ralrimiva	$⊢ φ \to \forall x \in (K + 1 \dots N) F (x) = Z$
37	36	adantr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to \forall x \in (K + 1 \dots N) F (x) = Z$
38		eluzp1p1	$⊢ n \in ℤ_{\geq K} \to n + 1 \in ℤ_{\geq (K + 1)}$
39	38	ad2antrl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n + 1 \in ℤ_{\geq (K + 1)}$
40		elfzuz3	$⊢ n + 1 \in (K \dots N) \to N \in ℤ_{\geq (n + 1)}$
41	40	ad2antll	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to N \in ℤ_{\geq (n + 1)}$
42		elfzuzb	$⊢ n + 1 \in (K + 1 \dots N) \leftrightarrow (n + 1 \in ℤ_{\geq (K + 1)} \land N \in ℤ_{\geq (n + 1)})$
43	39 41 42	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n + 1 \in (K + 1 \dots N)$
44	35 37 43	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to F (n + 1) = Z$
45	44	oveq2d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} F (n + 1) = seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} Z$
46		oveq1	$⊢ x = seq M (\underset{˙}{+}, F) (K) \to x \underset{˙}{+} Z = seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} Z$
47		id	$⊢ x = seq M (\underset{˙}{+}, F) (K) \to x = seq M (\underset{˙}{+}, F) (K)$
48	46 47	eqeq12d	$⊢ x = seq M (\underset{˙}{+}, F) (K) \to (x \underset{˙}{+} Z = x \leftrightarrow seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} Z = seq M (\underset{˙}{+}, F) (K))$
49	1	ralrimiva	$⊢ φ \to \forall x \in S x \underset{˙}{+} Z = x$
50	48 49 4	rspcdva	$⊢ φ \to seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} Z = seq M (\underset{˙}{+}, F) (K)$
51	50	adantr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} Z = seq M (\underset{˙}{+}, F) (K)$
52	45 51	eqtr2d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} F (n + 1)$
53		simprl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n \in ℤ_{\geq K}$
54	2	adantr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to K \in ℤ_{\geq M}$
55		uztrn	$⊢ (n \in ℤ_{\geq K} \land K \in ℤ_{\geq M}) \to n \in ℤ_{\geq M}$
56	53 54 55	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n \in ℤ_{\geq M}$
57		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
58	56 57	syl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
59	52 58	eqeq12d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1) \leftrightarrow seq M (\underset{˙}{+}, F) (K) \underset{˙}{+} F (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1))$
60	34 59	syl5ibr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to (seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1))$
61	33 60	animpimp2impd	$⊢ n \in ℤ_{\geq K} \to ((φ \to (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n))) \to (φ \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (n + 1))))$
62	12 17 22 27 29 61	uzind4	$⊢ N \in ℤ_{\geq K} \to (φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N)))$
63	3 62	mpcom	$⊢ φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N))$
64	7 63	mpd	$⊢ φ \to seq M (\underset{˙}{+}, F) (K) = seq M (\underset{˙}{+}, F) (N)$

Metamath Proof Explorer

Theorem seqid2

Proof