# 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}={ℤ}_{\ge {M}}$
isercoll2.w ${⊢}{W}={ℤ}_{\ge {N}}$
isercoll2.m ${⊢}{\phi }\to {M}\in ℤ$
isercoll2.n ${⊢}{\phi }\to {N}\in ℤ$
isercoll2.g ${⊢}{\phi }\to {G}:{Z}⟶{W}$
isercoll2.i ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}\left({k}\right)<{G}\left({k}+1\right)$
isercoll2.0 ${⊢}\left({\phi }\wedge {n}\in \left({W}\setminus \mathrm{ran}{G}\right)\right)\to {F}\left({n}\right)=0$
isercoll2.f ${⊢}\left({\phi }\wedge {n}\in {W}\right)\to {F}\left({n}\right)\in ℂ$
isercoll2.h ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {H}\left({k}\right)={F}\left({G}\left({k}\right)\right)$
Assertion isercoll2 ${⊢}{\phi }\to \left(seq{M}\left(+,{H}\right)⇝{A}↔seq{N}\left(+,{F}\right)⇝{A}\right)$

### Proof

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