isercoll2

Description: Generalize isercoll so that both sequences have arbitrary starting point. (Contributed by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypotheses	isercoll2.z	$⊢ Z = ℤ_{\geq M}$
	isercoll2.w	$⊢ W = ℤ_{\geq N}$
	isercoll2.m	$⊢ φ \to M \in ℤ$
	isercoll2.n	$⊢ φ \to N \in ℤ$
	isercoll2.g	$⊢ φ \to G : Z ⟶ W$
	isercoll2.i	$⊢ (φ \land k \in Z) \to G (k) < G (k + 1)$
	isercoll2.0	$⊢ (φ \land n \in (W ∖ ran G)) \to F (n) = 0$
	isercoll2.f	$⊢ (φ \land n \in W) \to F (n) \in ℂ$
	isercoll2.h	$⊢ (φ \land k \in Z) \to H (k) = F (G (k))$
Assertion	isercoll2	$⊢ φ \to (seq M (+ H) ⇝ A \leftrightarrow seq N (+ F) ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		isercoll2.z	$⊢ Z = ℤ_{\geq M}$
2		isercoll2.w	$⊢ W = ℤ_{\geq N}$
3		isercoll2.m	$⊢ φ \to M \in ℤ$
4		isercoll2.n	$⊢ φ \to N \in ℤ$
5		isercoll2.g	$⊢ φ \to G : Z ⟶ W$
6		isercoll2.i	$⊢ (φ \land k \in Z) \to G (k) < G (k + 1)$
7		isercoll2.0	$⊢ (φ \land n \in (W ∖ ran G)) \to F (n) = 0$
8		isercoll2.f	$⊢ (φ \land n \in W) \to F (n) \in ℂ$
9		isercoll2.h	$⊢ (φ \land k \in Z) \to H (k) = F (G (k))$
10		1z	$⊢ 1 \in ℤ$
11		zsubcl	$⊢ (1 \in ℤ \land M \in ℤ) \to 1 - M \in ℤ$
12	10 3 11	sylancr	$⊢ φ \to 1 - M \in ℤ$
13		seqex	$⊢ seq M (+ H) \in V$
14	13	a1i	$⊢ φ \to seq M (+ H) \in V$
15		seqex	$⊢ seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) \in V$
16	15	a1i	$⊢ φ \to seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) \in V$
17		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
18	17 1	eleqtrdi	$⊢ (φ \land k \in Z) \to k \in ℤ_{\geq M}$
19	12	adantr	$⊢ (φ \land k \in Z) \to 1 - M \in ℤ$
20		simpl	$⊢ (φ \land k \in Z) \to φ$
21		elfzuz	$⊢ j \in (M \dots k) \to j \in ℤ_{\geq M}$
22	21 1	eleqtrrdi	$⊢ j \in (M \dots k) \to j \in Z$
23		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
24	23 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
25		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
26	24 25	syl	$⊢ (φ \land j \in Z) \to j \in ℤ$
27	26	zcnd	$⊢ (φ \land j \in Z) \to j \in ℂ$
28	3	zcnd	$⊢ φ \to M \in ℂ$
29	28	adantr	$⊢ (φ \land j \in Z) \to M \in ℂ$
30		1cnd	$⊢ (φ \land j \in Z) \to 1 \in ℂ$
31	27 29 30	subadd23d	$⊢ (φ \land j \in Z) \to j - M + 1 = j + 1 - M$
32		uznn0sub	$⊢ j \in ℤ_{\geq M} \to j - M \in ℕ_{0}$
33	24 32	syl	$⊢ (φ \land j \in Z) \to j - M \in ℕ_{0}$
34		nn0p1nn	$⊢ j - M \in ℕ_{0} \to j - M + 1 \in ℕ$
35	33 34	syl	$⊢ (φ \land j \in Z) \to j - M + 1 \in ℕ$
36	31 35	eqeltrrd	$⊢ (φ \land j \in Z) \to j + 1 - M \in ℕ$
37		oveq1	$⊢ x = j + 1 - M \to x - 1 = j + (1 - M) - 1$
38	37	oveq2d	$⊢ x = j + 1 - M \to M + x - 1 = M + (j + 1 - M) - 1$
39	38	fveq2d	$⊢ x = j + 1 - M \to H (M + x - 1) = H (M + (j + 1 - M) - 1)$
40		eqid	$⊢ (x \in ℕ ⟼ H (M + x - 1)) = (x \in ℕ ⟼ H (M + x - 1))$
41		fvex	$⊢ H (M + (j + 1 - M) - 1) \in V$
42	39 40 41	fvmpt	$⊢ j + 1 - M \in ℕ \to (x \in ℕ ⟼ H (M + x - 1)) (j + 1 - M) = H (M + (j + 1 - M) - 1)$
43	36 42	syl	$⊢ (φ \land j \in Z) \to (x \in ℕ ⟼ H (M + x - 1)) (j + 1 - M) = H (M + (j + 1 - M) - 1)$
44	31	oveq1d	$⊢ (φ \land j \in Z) \to (j - M) + 1 - 1 = j + (1 - M) - 1$
45	33	nn0cnd	$⊢ (φ \land j \in Z) \to j - M \in ℂ$
46		ax-1cn	$⊢ 1 \in ℂ$
47		pncan	$⊢ (j - M \in ℂ \land 1 \in ℂ) \to (j - M) + 1 - 1 = j - M$
48	45 46 47	sylancl	$⊢ (φ \land j \in Z) \to (j - M) + 1 - 1 = j - M$
49	44 48	eqtr3d	$⊢ (φ \land j \in Z) \to j + (1 - M) - 1 = j - M$
50	49	oveq2d	$⊢ (φ \land j \in Z) \to M + (j + 1 - M) - 1 = M + j - M$
51	29 27	pncan3d	$⊢ (φ \land j \in Z) \to M + j - M = j$
52	50 51	eqtrd	$⊢ (φ \land j \in Z) \to M + (j + 1 - M) - 1 = j$
53	52	fveq2d	$⊢ (φ \land j \in Z) \to H (M + (j + 1 - M) - 1) = H (j)$
54	43 53	eqtr2d	$⊢ (φ \land j \in Z) \to H (j) = (x \in ℕ ⟼ H (M + x - 1)) (j + 1 - M)$
55	20 22 54	syl2an	$⊢ ((φ \land k \in Z) \land j \in (M \dots k)) \to H (j) = (x \in ℕ ⟼ H (M + x - 1)) (j + 1 - M)$
56	18 19 55	seqshft2	$⊢ (φ \land k \in Z) \to seq M (+ H) (k) = seq (M + 1 - M) (+ (x \in ℕ ⟼ H (M + x - 1))) (k + 1 - M)$
57	28	adantr	$⊢ (φ \land k \in Z) \to M \in ℂ$
58		pncan3	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - M = 1$
59	57 46 58	sylancl	$⊢ (φ \land k \in Z) \to M + 1 - M = 1$
60	59	seqeq1d	$⊢ (φ \land k \in Z) \to seq (M + 1 - M) (+ (x \in ℕ ⟼ H (M + x - 1))) = seq 1 (+ (x \in ℕ ⟼ H (M + x - 1)))$
61	60	fveq1d	$⊢ (φ \land k \in Z) \to seq (M + 1 - M) (+ (x \in ℕ ⟼ H (M + x - 1))) (k + 1 - M) = seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) (k + 1 - M)$
62	56 61	eqtr2d	$⊢ (φ \land k \in Z) \to seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) (k + 1 - M) = seq M (+ H) (k)$
63	1 3 12 14 16 62	climshft2	$⊢ φ \to (seq M (+ H) ⇝ A \leftrightarrow seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) ⇝ A)$
64	5	adantr	$⊢ (φ \land x \in ℕ) \to G : Z ⟶ W$
65		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
66	3 65	syl	$⊢ φ \to M \in ℤ_{\geq M}$
67		nnm1nn0	$⊢ x \in ℕ \to x - 1 \in ℕ_{0}$
68		uzaddcl	$⊢ (M \in ℤ_{\geq M} \land x - 1 \in ℕ_{0}) \to M + x - 1 \in ℤ_{\geq M}$
69	66 67 68	syl2an	$⊢ (φ \land x \in ℕ) \to M + x - 1 \in ℤ_{\geq M}$
70	69 1	eleqtrrdi	$⊢ (φ \land x \in ℕ) \to M + x - 1 \in Z$
71	64 70	ffvelcdmd	$⊢ (φ \land x \in ℕ) \to G (M + x - 1) \in W$
72	71	fmpttd	$⊢ φ \to (x \in ℕ ⟼ G (M + x - 1)) : ℕ ⟶ W$
73		fveq2	$⊢ k = M + j - 1 \to G (k) = G (M + j - 1)$
74		fvoveq1	$⊢ k = M + j - 1 \to G (k + 1) = G (M + (j - 1) + 1)$
75	73 74	breq12d	$⊢ k = M + j - 1 \to (G (k) < G (k + 1) \leftrightarrow G (M + j - 1) < G (M + (j - 1) + 1))$
76	6	ralrimiva	$⊢ φ \to \forall k \in Z G (k) < G (k + 1)$
77	76	adantr	$⊢ (φ \land j \in ℕ) \to \forall k \in Z G (k) < G (k + 1)$
78		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
79		uzaddcl	$⊢ (M \in ℤ_{\geq M} \land j - 1 \in ℕ_{0}) \to M + j - 1 \in ℤ_{\geq M}$
80	66 78 79	syl2an	$⊢ (φ \land j \in ℕ) \to M + j - 1 \in ℤ_{\geq M}$
81	80 1	eleqtrrdi	$⊢ (φ \land j \in ℕ) \to M + j - 1 \in Z$
82	75 77 81	rspcdva	$⊢ (φ \land j \in ℕ) \to G (M + j - 1) < G (M + (j - 1) + 1)$
83		nncn	$⊢ j \in ℕ \to j \in ℂ$
84	83	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℂ$
85		1cnd	$⊢ (φ \land j \in ℕ) \to 1 \in ℂ$
86	84 85 85	addsubd	$⊢ (φ \land j \in ℕ) \to j + 1 - 1 = j - 1 + 1$
87	86	oveq2d	$⊢ (φ \land j \in ℕ) \to M + (j + 1) - 1 = M + (j - 1) + 1$
88	28	adantr	$⊢ (φ \land j \in ℕ) \to M \in ℂ$
89	78	adantl	$⊢ (φ \land j \in ℕ) \to j - 1 \in ℕ_{0}$
90	89	nn0cnd	$⊢ (φ \land j \in ℕ) \to j - 1 \in ℂ$
91	88 90 85	addassd	$⊢ (φ \land j \in ℕ) \to M + (j - 1) + 1 = M + (j - 1) + 1$
92	87 91	eqtr4d	$⊢ (φ \land j \in ℕ) \to M + (j + 1) - 1 = M + (j - 1) + 1$
93	92	fveq2d	$⊢ (φ \land j \in ℕ) \to G (M + (j + 1) - 1) = G (M + (j - 1) + 1)$
94	82 93	breqtrrd	$⊢ (φ \land j \in ℕ) \to G (M + j - 1) < G (M + (j + 1) - 1)$
95		oveq1	$⊢ x = j \to x - 1 = j - 1$
96	95	oveq2d	$⊢ x = j \to M + x - 1 = M + j - 1$
97	96	fveq2d	$⊢ x = j \to G (M + x - 1) = G (M + j - 1)$
98		eqid	$⊢ (x \in ℕ ⟼ G (M + x - 1)) = (x \in ℕ ⟼ G (M + x - 1))$
99		fvex	$⊢ G (M + j - 1) \in V$
100	97 98 99	fvmpt	$⊢ j \in ℕ \to (x \in ℕ ⟼ G (M + x - 1)) (j) = G (M + j - 1)$
101	100	adantl	$⊢ (φ \land j \in ℕ) \to (x \in ℕ ⟼ G (M + x - 1)) (j) = G (M + j - 1)$
102		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
103	102	adantl	$⊢ (φ \land j \in ℕ) \to j + 1 \in ℕ$
104		oveq1	$⊢ x = j + 1 \to x - 1 = j + 1 - 1$
105	104	oveq2d	$⊢ x = j + 1 \to M + x - 1 = M + (j + 1) - 1$
106	105	fveq2d	$⊢ x = j + 1 \to G (M + x - 1) = G (M + (j + 1) - 1)$
107		fvex	$⊢ G (M + (j + 1) - 1) \in V$
108	106 98 107	fvmpt	$⊢ j + 1 \in ℕ \to (x \in ℕ ⟼ G (M + x - 1)) (j + 1) = G (M + (j + 1) - 1)$
109	103 108	syl	$⊢ (φ \land j \in ℕ) \to (x \in ℕ ⟼ G (M + x - 1)) (j + 1) = G (M + (j + 1) - 1)$
110	94 101 109	3brtr4d	$⊢ (φ \land j \in ℕ) \to (x \in ℕ ⟼ G (M + x - 1)) (j) < (x \in ℕ ⟼ G (M + x - 1)) (j + 1)$
111	5	ffnd	$⊢ φ \to G Fn Z$
112		uznn0sub	$⊢ k \in ℤ_{\geq M} \to k - M \in ℕ_{0}$
113	18 112	syl	$⊢ (φ \land k \in Z) \to k - M \in ℕ_{0}$
114		nn0p1nn	$⊢ k - M \in ℕ_{0} \to k - M + 1 \in ℕ$
115	113 114	syl	$⊢ (φ \land k \in Z) \to k - M + 1 \in ℕ$
116	113	nn0cnd	$⊢ (φ \land k \in Z) \to k - M \in ℂ$
117		pncan	$⊢ (k - M \in ℂ \land 1 \in ℂ) \to (k - M) + 1 - 1 = k - M$
118	116 46 117	sylancl	$⊢ (φ \land k \in Z) \to (k - M) + 1 - 1 = k - M$
119	118	oveq2d	$⊢ (φ \land k \in Z) \to M + (k - M + 1) - 1 = M + k - M$
120		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
121	120 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
122	121	zcnd	$⊢ k \in Z \to k \in ℂ$
123		pncan3	$⊢ (M \in ℂ \land k \in ℂ) \to M + k - M = k$
124	28 122 123	syl2an	$⊢ (φ \land k \in Z) \to M + k - M = k$
125	119 124	eqtr2d	$⊢ (φ \land k \in Z) \to k = M + (k - M + 1) - 1$
126	125	fveq2d	$⊢ (φ \land k \in Z) \to G (k) = G (M + (k - M + 1) - 1)$
127		oveq1	$⊢ x = k - M + 1 \to x - 1 = (k - M) + 1 - 1$
128	127	oveq2d	$⊢ x = k - M + 1 \to M + x - 1 = M + (k - M + 1) - 1$
129	128	fveq2d	$⊢ x = k - M + 1 \to G (M + x - 1) = G (M + (k - M + 1) - 1)$
130	129	rspceeqv	$⊢ (k - M + 1 \in ℕ \land G (k) = G (M + (k - M + 1) - 1)) \to \exists x \in ℕ G (k) = G (M + x - 1)$
131	115 126 130	syl2anc	$⊢ (φ \land k \in Z) \to \exists x \in ℕ G (k) = G (M + x - 1)$
132		fvex	$⊢ G (k) \in V$
133	98	elrnmpt	$⊢ G (k) \in V \to (G (k) \in ran (x \in ℕ ⟼ G (M + x - 1)) \leftrightarrow \exists x \in ℕ G (k) = G (M + x - 1))$
134	132 133	ax-mp	$⊢ G (k) \in ran (x \in ℕ ⟼ G (M + x - 1)) \leftrightarrow \exists x \in ℕ G (k) = G (M + x - 1)$
135	131 134	sylibr	$⊢ (φ \land k \in Z) \to G (k) \in ran (x \in ℕ ⟼ G (M + x - 1))$
136	135	ralrimiva	$⊢ φ \to \forall k \in Z G (k) \in ran (x \in ℕ ⟼ G (M + x - 1))$
137		ffnfv	$⊢ G : Z ⟶ ran (x \in ℕ ⟼ G (M + x - 1)) \leftrightarrow (G Fn Z \land \forall k \in Z G (k) \in ran (x \in ℕ ⟼ G (M + x - 1)))$
138	111 136 137	sylanbrc	$⊢ φ \to G : Z ⟶ ran (x \in ℕ ⟼ G (M + x - 1))$
139	138	frnd	$⊢ φ \to ran G \subseteq ran (x \in ℕ ⟼ G (M + x - 1))$
140	139	sscond	$⊢ φ \to W ∖ ran (x \in ℕ ⟼ G (M + x - 1)) \subseteq W ∖ ran G$
141	140	sselda	$⊢ (φ \land n \in (W ∖ ran (x \in ℕ ⟼ G (M + x - 1)))) \to n \in (W ∖ ran G)$
142	141 7	syldan	$⊢ (φ \land n \in (W ∖ ran (x \in ℕ ⟼ G (M + x - 1)))) \to F (n) = 0$
143		fveq2	$⊢ k = M + j - 1 \to H (k) = H (M + j - 1)$
144	73	fveq2d	$⊢ k = M + j - 1 \to F (G (k)) = F (G (M + j - 1))$
145	143 144	eqeq12d	$⊢ k = M + j - 1 \to (H (k) = F (G (k)) \leftrightarrow H (M + j - 1) = F (G (M + j - 1)))$
146	9	ralrimiva	$⊢ φ \to \forall k \in Z H (k) = F (G (k))$
147	146	adantr	$⊢ (φ \land j \in ℕ) \to \forall k \in Z H (k) = F (G (k))$
148	145 147 81	rspcdva	$⊢ (φ \land j \in ℕ) \to H (M + j - 1) = F (G (M + j - 1))$
149	96	fveq2d	$⊢ x = j \to H (M + x - 1) = H (M + j - 1)$
150		fvex	$⊢ H (M + j - 1) \in V$
151	149 40 150	fvmpt	$⊢ j \in ℕ \to (x \in ℕ ⟼ H (M + x - 1)) (j) = H (M + j - 1)$
152	151	adantl	$⊢ (φ \land j \in ℕ) \to (x \in ℕ ⟼ H (M + x - 1)) (j) = H (M + j - 1)$
153	101	fveq2d	$⊢ (φ \land j \in ℕ) \to F ((x \in ℕ ⟼ G (M + x - 1)) (j)) = F (G (M + j - 1))$
154	148 152 153	3eqtr4d	$⊢ (φ \land j \in ℕ) \to (x \in ℕ ⟼ H (M + x - 1)) (j) = F ((x \in ℕ ⟼ G (M + x - 1)) (j))$
155	2 4 72 110 142 8 154	isercoll	$⊢ φ \to (seq 1 (+ (x \in ℕ ⟼ H (M + x - 1))) ⇝ A \leftrightarrow seq N (+ F) ⇝ A)$
156	63 155	bitrd	$⊢ φ \to (seq M (+ H) ⇝ A \leftrightarrow seq N (+ F) ⇝ A)$

Metamath Proof Explorer

Theorem isercoll2

Proof