seqfveq2

Description: Equality of sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		seqfveq2.1	$⊢ φ \to K \in ℤ_{\geq M}$
2		seqfveq2.2	$⊢ φ \to seq M (\underset{˙}{+}, F) (K) = G (K)$
3		seqfveq2.3	$⊢ φ \to N \in ℤ_{\geq K}$
4		seqfveq2.4	$⊢ (φ \land k \in (K + 1 \dots N)) \to F (k) = G (k)$
5		eluzfz2	$⊢ N \in ℤ_{\geq K} \to N \in (K \dots N)$
6	3 5	syl	$⊢ φ \to N \in (K \dots N)$
7		eleq1	$⊢ x = K \to (x \in (K \dots N) \leftrightarrow K \in (K \dots N))$
8		fveq2	$⊢ x = K \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (K)$
9		fveq2	$⊢ x = K \to seq K (\underset{˙}{+}, G) (x) = seq K (\underset{˙}{+}, G) (K)$
10	8 9	eqeq12d	$⊢ x = K \to (seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (K) = seq K (\underset{˙}{+}, G) (K))$
11	7 10	imbi12d	$⊢ x = K \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x)) \leftrightarrow (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq K (\underset{˙}{+}, G) (K)))$
12	11	imbi2d	$⊢ x = K \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x))) \leftrightarrow (φ \to (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq K (\underset{˙}{+}, G) (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		fveq2	$⊢ x = n \to seq K (\underset{˙}{+}, G) (x) = seq K (\underset{˙}{+}, G) (n)$
16	14 15	eqeq12d	$⊢ x = n \to (seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n))$
17	13 16	imbi12d	$⊢ x = n \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x)) \leftrightarrow (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n)))$
18	17	imbi2d	$⊢ x = n \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x))) \leftrightarrow (φ \to (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n))))$
19		eleq1	$⊢ x = n + 1 \to (x \in (K \dots N) \leftrightarrow n + 1 \in (K \dots N))$
20		fveq2	$⊢ x = n + 1 \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (n + 1)$
21		fveq2	$⊢ x = n + 1 \to seq K (\underset{˙}{+}, G) (x) = seq K (\underset{˙}{+}, G) (n + 1)$
22	20 21	eqeq12d	$⊢ x = n + 1 \to (seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1))$
23	19 22	imbi12d	$⊢ x = n + 1 \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x)) \leftrightarrow (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1)))$
24	23	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x))) \leftrightarrow (φ \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1))))$
25		eleq1	$⊢ x = N \to (x \in (K \dots N) \leftrightarrow N \in (K \dots N))$
26		fveq2	$⊢ x = N \to seq M (\underset{˙}{+}, F) (x) = seq M (\underset{˙}{+}, F) (N)$
27		fveq2	$⊢ x = N \to seq K (\underset{˙}{+}, G) (x) = seq K (\underset{˙}{+}, G) (N)$
28	26 27	eqeq12d	$⊢ x = N \to (seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x) \leftrightarrow seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N))$
29	25 28	imbi12d	$⊢ x = N \to ((x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x)) \leftrightarrow (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N)))$
30	29	imbi2d	$⊢ x = N \to ((φ \to (x \in (K \dots N) \to seq M (\underset{˙}{+}, F) (x) = seq K (\underset{˙}{+}, G) (x))) \leftrightarrow (φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N))))$
31		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
32		seq1	$⊢ K \in ℤ \to seq K (\underset{˙}{+}, G) (K) = G (K)$
33	1 31 32	3syl	$⊢ φ \to seq K (\underset{˙}{+}, G) (K) = G (K)$
34	2 33	eqtr4d	$⊢ φ \to seq M (\underset{˙}{+}, F) (K) = seq K (\underset{˙}{+}, G) (K)$
35	34	a1d	$⊢ φ \to (K \in (K \dots N) \to seq M (\underset{˙}{+}, F) (K) = seq K (\underset{˙}{+}, G) (K))$
36		peano2fzr	$⊢ (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N)) \to n \in (K \dots N)$
37	36	adantl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n \in (K \dots N)$
38	37	expr	$⊢ (φ \land n \in ℤ_{\geq K}) \to (n + 1 \in (K \dots N) \to n \in (K \dots N))$
39	38	imim1d	$⊢ (φ \land n \in ℤ_{\geq K}) \to ((n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n)) \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n)))$
40		oveq1	$⊢ seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} F (n + 1)$
41		simpl	$⊢ (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N)) \to n \in ℤ_{\geq K}$
42		uztrn	$⊢ (n \in ℤ_{\geq K} \land K \in ℤ_{\geq M}) \to n \in ℤ_{\geq M}$
43	41 1 42	syl2anr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n \in ℤ_{\geq M}$
44		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\underset{˙}{+}, F) (n + 1) = seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1)$
45	43 44	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)$
46		seqp1	$⊢ n \in ℤ_{\geq K} \to seq K (\underset{˙}{+}, G) (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
47	46	ad2antrl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq K (\underset{˙}{+}, G) (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
48		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
49		fveq2	$⊢ k = n + 1 \to G (k) = G (n + 1)$
50	48 49	eqeq12d	$⊢ k = n + 1 \to (F (k) = G (k) \leftrightarrow F (n + 1) = G (n + 1))$
51	4	ralrimiva	$⊢ φ \to \forall k \in (K + 1 \dots N) F (k) = G (k)$
52	51	adantr	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to \forall k \in (K + 1 \dots N) F (k) = G (k)$
53		eluzp1p1	$⊢ n \in ℤ_{\geq K} \to n + 1 \in ℤ_{\geq (K + 1)}$
54	53	ad2antrl	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n + 1 \in ℤ_{\geq (K + 1)}$
55		elfzuz3	$⊢ n + 1 \in (K \dots N) \to N \in ℤ_{\geq (n + 1)}$
56	55	ad2antll	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to N \in ℤ_{\geq (n + 1)}$
57		elfzuzb	$⊢ n + 1 \in (K + 1 \dots N) \leftrightarrow (n + 1 \in ℤ_{\geq (K + 1)} \land N \in ℤ_{\geq (n + 1)})$
58	54 56 57	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to n + 1 \in (K + 1 \dots N)$
59	50 52 58	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to F (n + 1) = G (n + 1)$
60	59	oveq2d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} F (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} G (n + 1)$
61	47 60	eqtr4d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to seq K (\underset{˙}{+}, G) (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} F (n + 1)$
62	45 61	eqeq12d	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to (seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1) \leftrightarrow seq M (\underset{˙}{+}, F) (n) \underset{˙}{+} F (n + 1) = seq K (\underset{˙}{+}, G) (n) \underset{˙}{+} F (n + 1))$
63	40 62	imbitrrid	$⊢ (φ \land (n \in ℤ_{\geq K} \land n + 1 \in (K \dots N))) \to (seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n) \to seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1))$
64	39 63	animpimp2impd	$⊢ n \in ℤ_{\geq K} \to ((φ \to (n \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n) = seq K (\underset{˙}{+}, G) (n))) \to (φ \to (n + 1 \in (K \dots N) \to seq M (\underset{˙}{+}, F) (n + 1) = seq K (\underset{˙}{+}, G) (n + 1))))$
65	12 18 24 30 35 64	uzind4i	$⊢ N \in ℤ_{\geq K} \to (φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N)))$
66	3 65	mpcom	$⊢ φ \to (N \in (K \dots N) \to seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N))$
67	6 66	mpd	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, G) (N)$

Metamath Proof Explorer

Theorem seqfveq2

Proof