Metamath Proof Explorer


Theorem 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 = M
isercoll2.w W = N
isercoll2.m φ M
isercoll2.n φ N
isercoll2.g φ G : Z W
isercoll2.i φ k Z G k < G k + 1
isercoll2.0 φ n W ran G F n = 0
isercoll2.f φ n W F n
isercoll2.h φ k Z H k = F G k
Assertion isercoll2 φ seq M + H A seq N + F A

Proof

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