This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isercoll2.w ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
isercoll2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isercoll2.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
isercoll2.g ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ 𝑊 )
isercoll2.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
isercoll2.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑊 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
isercoll2.f ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
isercoll2.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
Assertion isercoll2 ( 𝜑 → ( seq 𝑀 ( + , 𝐻 ) ⇝ 𝐴 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐴 ) )

Proof

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