Metamath Proof Explorer

Theorem isercoll

Description: Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
isercoll.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
isercoll.f ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
isercoll.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
Assertion isercoll ( 𝜑 → ( seq 1 ( + , 𝐻 ) ⇝ 𝐴 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
4 isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
5 isercoll.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑍 ∖ ran 𝐺 ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
6 isercoll.f ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
7 isercoll.h ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
8 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
9 1 8 eqsstri ⊢ 𝑍 ⊆ ℤ
10 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ 𝑍 )
11 9 10 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℤ )
12 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
13 12 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝑛 ∈ ℤ )
14 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝑀 ... 𝑚 ) ∈ Fin )
15 ffun ⊢ ( 𝐺 : ℕ ⟶ 𝑍 → Fun 𝐺 )
16 funimacnv ⊢ ( Fun 𝐺 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) = ( ( 𝑀 ... 𝑚 ) ∩ ran 𝐺 ) )
17 3 15 16 3syl ⊢ ( 𝜑 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) = ( ( 𝑀 ... 𝑚 ) ∩ ran 𝐺 ) )
18 inss1 ⊢ ( ( 𝑀 ... 𝑚 ) ∩ ran 𝐺 ) ⊆ ( 𝑀 ... 𝑚 )
19 17 18 eqsstrdi ⊢ ( 𝜑 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ⊆ ( 𝑀 ... 𝑚 ) )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ⊆ ( 𝑀 ... 𝑚 ) )
21 14 20 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ∈ Fin )
22 hashcl ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ℕ0 )
23 nn0z ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ℤ )
24 21 22 23 3syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ℤ )
25 ssid ⊢ ℕ ⊆ ℕ
26 1 2 3 4 isercolllem1 ⊢ ( ( 𝜑 ∧ ℕ ⊆ ℕ ) → ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) )
27 25 26 mpan2 ⊢ ( 𝜑 → ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) )
28 ffn ⊢ ( 𝐺 : ℕ ⟶ 𝑍 → 𝐺 Fn ℕ )
29 fnresdm ⊢ ( 𝐺 Fn ℕ → ( 𝐺 ↾ ℕ ) = 𝐺 )
30 isoeq1 ⊢ ( ( 𝐺 ↾ ℕ ) = 𝐺 → ( ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ↔ 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) )
31 3 28 29 30 4syl ⊢ ( 𝜑 → ( ( 𝐺 ↾ ℕ ) Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ↔ 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ) )
32 27 31 mpbid ⊢ ( 𝜑 → 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) )
33 isof1o ⊢ ( 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) → 𝐺 : ℕ –1-1-onto→ ( 𝐺 “ ℕ ) )
34 f1ocnv ⊢ ( 𝐺 : ℕ –1-1-onto→ ( 𝐺 “ ℕ ) → ◡ 𝐺 : ( 𝐺 “ ℕ ) –1-1-onto→ ℕ )
35 f1ofun ⊢ ( ◡ 𝐺 : ( 𝐺 “ ℕ ) –1-1-onto→ ℕ → Fun ◡ 𝐺 )
36 32 33 34 35 4syl ⊢ ( 𝜑 → Fun ◡ 𝐺 )
37 df-f1 ⊢ ( 𝐺 : ℕ –1-1→ 𝑍 ↔ ( 𝐺 : ℕ ⟶ 𝑍 ∧ Fun ◡ 𝐺 ) )
38 3 36 37 sylanbrc ⊢ ( 𝜑 → 𝐺 : ℕ –1-1→ 𝑍 )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝐺 : ℕ –1-1→ 𝑍 )
40 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
41 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
42 41 f1imaen ⊢ ( ( 𝐺 : ℕ –1-1→ 𝑍 ∧ ( 1 ... 𝑛 ) ⊆ ℕ ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ≈ ( 1 ... 𝑛 ) )
43 39 40 42 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ≈ ( 1 ... 𝑛 ) )
44 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
45 enfii ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ ( 𝐺 “ ( 1 ... 𝑛 ) ) ≈ ( 1 ... 𝑛 ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ∈ Fin )
46 44 43 45 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ∈ Fin )
47 hashen ⊢ ( ( ( 𝐺 “ ( 1 ... 𝑛 ) ) ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ ( 𝐺 “ ( 1 ... 𝑛 ) ) ≈ ( 1 ... 𝑛 ) ) )
48 46 44 47 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ ( 𝐺 “ ( 1 ... 𝑛 ) ) ≈ ( 1 ... 𝑛 ) ) )
49 43 48 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) )
50 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
51 50 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝑛 ∈ ℕ0 )
52 hashfz1 ⊢ ( 𝑛 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
53 51 52 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
54 49 53 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) = 𝑛 )
55 elfznn ⊢ ( 𝑦 ∈ ( 1 ... 𝑛 ) → 𝑦 ∈ ℕ )
56 55 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑦 ∈ ℕ )
57 zssre ⊢ ℤ ⊆ ℝ
58 9 57 sstri ⊢ 𝑍 ⊆ ℝ
59 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝐺 : ℕ ⟶ 𝑍 )
60 ffvelrn ⊢ ( ( 𝐺 : ℕ ⟶ 𝑍 ∧ 𝑦 ∈ ℕ ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝑍 )
61 59 55 60 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝑍 )
62 58 61 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
63 10 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ 𝑍 )
64 58 63 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
65 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) → 𝑚 ∈ ℤ )
66 65 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑚 ∈ ℤ )
67 66 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑚 ∈ ℝ )
68 elfzle2 ⊢ ( 𝑦 ∈ ( 1 ... 𝑛 ) → 𝑦 ≤ 𝑛 )
69 68 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑦 ≤ 𝑛 )
70 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) )
71 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑛 ∈ ℕ )
72 isorel ⊢ ( ( 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑛 < 𝑦 ↔ ( 𝐺 ‘ 𝑛 ) < ( 𝐺 ‘ 𝑦 ) ) )
73 70 71 56 72 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝑛 < 𝑦 ↔ ( 𝐺 ‘ 𝑛 ) < ( 𝐺 ‘ 𝑦 ) ) )
74 73 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( ¬ 𝑛 < 𝑦 ↔ ¬ ( 𝐺 ‘ 𝑛 ) < ( 𝐺 ‘ 𝑦 ) ) )
75 56 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑦 ∈ ℝ )
76 71 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑛 ∈ ℝ )
77 75 76 lenltd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦 ) )
78 62 64 lenltd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐺 ‘ 𝑦 ) ≤ ( 𝐺 ‘ 𝑛 ) ↔ ¬ ( 𝐺 ‘ 𝑛 ) < ( 𝐺 ‘ 𝑦 ) ) )
79 74 77 78 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝑦 ≤ 𝑛 ↔ ( 𝐺 ‘ 𝑦 ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
80 69 79 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ≤ ( 𝐺 ‘ 𝑛 ) )
81 eluzle ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ 𝑚 )
82 81 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑛 ) ≤ 𝑚 )
83 62 64 67 80 82 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ≤ 𝑚 )
84 61 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
85 elfz5 ⊢ ( ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐺 ‘ 𝑦 ) ∈ ( 𝑀 ... 𝑚 ) ↔ ( 𝐺 ‘ 𝑦 ) ≤ 𝑚 ) )
86 84 66 85 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝐺 ‘ 𝑦 ) ∈ ( 𝑀 ... 𝑚 ) ↔ ( 𝐺 ‘ 𝑦 ) ≤ 𝑚 ) )
87 83 86 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( 𝑀 ... 𝑚 ) )
88 59 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝐺 Fn ℕ )
89 88 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝐺 Fn ℕ )
90 elpreima ⊢ ( 𝐺 Fn ℕ → ( 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ↔ ( 𝑦 ∈ ℕ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝑀 ... 𝑚 ) ) ) )
91 89 90 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → ( 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ↔ ( 𝑦 ∈ ℕ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( 𝑀 ... 𝑚 ) ) ) )
92 56 87 91 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) ∧ 𝑦 ∈ ( 1 ... 𝑛 ) ) → 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) )
93 92 ex ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝑦 ∈ ( 1 ... 𝑛 ) → 𝑦 ∈ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) )
94 93 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 1 ... 𝑛 ) ⊆ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) )
95 imass2 ⊢ ( ( 1 ... 𝑛 ) ⊆ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) )
96 94 95 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) )
97 ssdomg ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ∈ Fin → ( ( 𝐺 “ ( 1 ... 𝑛 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) )
98 21 96 97 sylc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( 𝐺 “ ( 1 ... 𝑛 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) )
99 hashdom ⊢ ( ( ( 𝐺 “ ( 1 ... 𝑛 ) ) ∈ Fin ∧ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑛 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) )
100 46 21 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑛 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) )
101 98 100 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑛 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) )
102 54 101 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → 𝑛 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) )
103 eluz2 ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ( ℤ≥ ‘ 𝑛 ) ↔ ( 𝑛 ∈ ℤ ∧ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ℤ ∧ 𝑛 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) )
104 13 24 102 103 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ( ℤ≥ ‘ 𝑛 ) )
105 fveq2 ⊢ ( 𝑘 = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) )
106 105 eleq1d ⊢ ( 𝑘 = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ↔ ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ) )
107 105 fvoveq1d ⊢ ( 𝑘 = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) )
108 107 breq1d ⊢ ( 𝑘 = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) )
109 106 108 anbi12d ⊢ ( 𝑘 = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
110 109 rspcv ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ∈ ( ℤ≥ ‘ 𝑛 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
111 104 110 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
112 111 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
113 fveq2 ⊢ ( 𝑗 = ( 𝐺 ‘ 𝑛 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) )
114 113 raleqdv ⊢ ( 𝑗 = ( 𝐺 ‘ 𝑛 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
115 114 rspcev ⊢ ( ( ( 𝐺 ‘ 𝑛 ) ∈ ℤ ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑛 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑗 ∈ ℤ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) )
116 11 112 115 syl6an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
117 116 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
118 1nn ⊢ 1 ∈ ℕ
119 ffvelrn ⊢ ( ( 𝐺 : ℕ ⟶ 𝑍 ∧ 1 ∈ ℕ ) → ( 𝐺 ‘ 1 ) ∈ 𝑍 )
120 3 118 119 sylancl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ 𝑍 )
121 120 1 eleqtrdi ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
122 eluzelz ⊢ ( ( 𝐺 ‘ 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐺 ‘ 1 ) ∈ ℤ )
123 eqid ⊢ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) = ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) )
124 123 rexuz3 ⊢ ( ( 𝐺 ‘ 1 ) ∈ ℤ → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
125 121 122 124 3syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
126 117 125 sylibrd ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
127 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝑀 ... 𝑗 ) ∈ Fin )
128 funimacnv ⊢ ( Fun 𝐺 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) = ( ( 𝑀 ... 𝑗 ) ∩ ran 𝐺 ) )
129 3 15 128 3syl ⊢ ( 𝜑 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) = ( ( 𝑀 ... 𝑗 ) ∩ ran 𝐺 ) )
130 inss1 ⊢ ( ( 𝑀 ... 𝑗 ) ∩ ran 𝐺 ) ⊆ ( 𝑀 ... 𝑗 )
131 129 130 eqsstrdi ⊢ ( 𝜑 → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ⊆ ( 𝑀 ... 𝑗 ) )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ⊆ ( 𝑀 ... 𝑗 ) )
133 127 132 ssfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ∈ Fin )
134 hashcl ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ∈ Fin → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℕ0 )
135 nn0p1nn ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℕ0 → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ∈ ℕ )
136 133 134 135 3syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ∈ ℕ )
137 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ≤ 𝑘 )
138 137 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ≤ 𝑘 )
139 133 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ∈ Fin )
140 nn0z ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℤ )
141 139 134 140 3syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℤ )
142 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) → 𝑘 ∈ ℤ )
143 142 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝑘 ∈ ℤ )
144 zltp1le ⊢ ( ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) < 𝑘 ↔ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ≤ 𝑘 ) )
145 141 143 144 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) < 𝑘 ↔ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ≤ 𝑘 ) )
146 138 145 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) < 𝑘 )
147 nn0re ⊢ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℝ )
148 133 134 147 3syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℝ )
149 148 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ∈ ℝ )
150 eluznn ⊢ ( ( ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝑘 ∈ ℕ )
151 136 150 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝑘 ∈ ℕ )
152 151 nnred ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝑘 ∈ ℝ )
153 149 152 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) < 𝑘 ↔ ¬ 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ) )
154 146 153 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ¬ 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
155 fzss2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) → ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 𝑀 ... 𝑗 ) )
156 imass2 ⊢ ( ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 𝑀 ... 𝑗 ) → ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ⊆ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) )
157 imass2 ⊢ ( ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ⊆ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) )
158 155 156 157 3syl ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) )
159 ssdomg ⊢ ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ∈ Fin → ( ( 𝐺 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
160 139 159 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( 𝐺 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
161 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝐺 : ℕ ⟶ 𝑍 )
162 161 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑍 )
163 162 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
164 161 151 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑍 )
165 9 164 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℤ )
166 165 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℤ )
167 elfz5 ⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝐺 ‘ 𝑘 ) ∈ ℤ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
168 163 166 167 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
169 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) )
170 nnssre ⊢ ℕ ⊆ ℝ
171 ressxr ⊢ ℝ ⊆ ℝ*
172 170 171 sstri ⊢ ℕ ⊆ ℝ*
173 172 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ℕ ⊆ ℝ* )
174 imassrn ⊢ ( 𝐺 “ ℕ ) ⊆ ran 𝐺
175 161 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝐺 : ℕ ⟶ 𝑍 )
176 175 frnd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ran 𝐺 ⊆ 𝑍 )
177 176 58 sstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ran 𝐺 ⊆ ℝ )
178 174 177 sstrid ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 “ ℕ ) ⊆ ℝ )
179 178 171 sstrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 “ ℕ ) ⊆ ℝ* )
180 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ )
181 151 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → 𝑘 ∈ ℕ )
182 leisorel ⊢ ( ( 𝐺 Isom < , < ( ℕ , ( 𝐺 “ ℕ ) ) ∧ ( ℕ ⊆ ℝ* ∧ ( 𝐺 “ ℕ ) ⊆ ℝ* ) ∧ ( 𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑥 ≤ 𝑘 ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
183 169 173 179 180 181 182 syl122anc ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝑥 ≤ 𝑘 ↔ ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
184 168 183 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ↔ 𝑥 ≤ 𝑘 ) )
185 184 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( 𝑥 ∈ ℕ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘 ) ) )
186 elpreima ⊢ ( 𝐺 Fn ℕ → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) )
187 161 28 186 3syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ↔ ( 𝑥 ∈ ℕ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) )
188 fznn ⊢ ( 𝑘 ∈ ℤ → ( 𝑥 ∈ ( 1 ... 𝑘 ) ↔ ( 𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘 ) ) )
189 143 188 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑥 ∈ ( 1 ... 𝑘 ) ↔ ( 𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘 ) ) )
190 185 187 189 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑥 ∈ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ↔ 𝑥 ∈ ( 1 ... 𝑘 ) ) )
191 190 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) = ( 1 ... 𝑘 ) )
192 191 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) = ( 𝐺 “ ( 1 ... 𝑘 ) ) )
193 192 sseq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
194 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝐺 : ℕ –1-1→ 𝑍 )
195 fz1ssnn ⊢ ( 1 ... 𝑘 ) ⊆ ℕ
196 ovex ⊢ ( 1 ... 𝑘 ) ∈ V
197 196 f1imaen ⊢ ( ( 𝐺 : ℕ –1-1→ 𝑍 ∧ ( 1 ... 𝑘 ) ⊆ ℕ ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ≈ ( 1 ... 𝑘 ) )
198 194 195 197 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ≈ ( 1 ... 𝑘 ) )
199 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 1 ... 𝑘 ) ∈ Fin )
200 enfii ⊢ ( ( ( 1 ... 𝑘 ) ∈ Fin ∧ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≈ ( 1 ... 𝑘 ) ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ∈ Fin )
201 199 198 200 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 “ ( 1 ... 𝑘 ) ) ∈ Fin )
202 hashen ⊢ ( ( ( 𝐺 “ ( 1 ... 𝑘 ) ) ∈ Fin ∧ ( 1 ... 𝑘 ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) = ( ♯ ‘ ( 1 ... 𝑘 ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≈ ( 1 ... 𝑘 ) ) )
203 201 199 202 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) = ( ♯ ‘ ( 1 ... 𝑘 ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≈ ( 1 ... 𝑘 ) ) )
204 198 203 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) = ( ♯ ‘ ( 1 ... 𝑘 ) ) )
205 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
206 hashfz1 ⊢ ( 𝑘 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑘 ) ) = 𝑘 )
207 151 205 206 3syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 1 ... 𝑘 ) ) = 𝑘 )
208 204 207 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) = 𝑘 )
209 208 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ↔ 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ) )
210 hashdom ⊢ ( ( ( 𝐺 “ ( 1 ... 𝑘 ) ) ∈ Fin ∧ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
211 201 139 210 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
212 209 211 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ↔ ( 𝐺 “ ( 1 ... 𝑘 ) ) ≼ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) )
213 160 193 212 3imtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ⊆ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) → 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ) )
214 158 213 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) → 𝑘 ≤ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) ) )
215 154 214 mtod ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ¬ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) )
216 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) → 𝑗 ∈ ℤ )
217 216 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → 𝑗 ∈ ℤ )
218 uztric ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) ∨ ( 𝐺 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) )
219 165 217 218 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) ∨ ( 𝐺 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) )
220 219 ord ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ¬ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 𝑘 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) )
221 215 220 mpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
222 oveq2 ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( 𝑀 ... 𝑚 ) = ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) )
223 222 imaeq2d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) = ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) )
224 223 imaeq2d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) = ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) )
225 224 fveq2d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) = ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) )
226 225 fveq2d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) )
227 226 eleq1d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ↔ ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ) )
228 226 fvoveq1d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) )
229 228 breq1d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) )
230 227 229 anbi12d ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑘 ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
231 230 rspcv ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
232 221 231 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
233 192 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) = ( ♯ ‘ ( 𝐺 “ ( 1 ... 𝑘 ) ) ) )
234 233 208 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) = 𝑘 )
235 234 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) )
236 235 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ↔ ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ) )
237 235 fvoveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) )
238 237 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ↔ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
239 236 238 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... ( 𝐺 ‘ 𝑘 ) ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ↔ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
240 232 239 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
241 240 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
242 fveq2 ⊢ ( 𝑛 = ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) )
243 242 raleqdv ⊢ ( 𝑛 = ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
244 243 rspcev ⊢ ( ( ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑗 ) ) ) ) + 1 ) ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
245 136 241 244 syl6an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
246 245 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) )
247 126 246 impbid ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
248 247 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) )
249 248 anbi2d ⊢ ( 𝜑 → ( ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) ) )
250 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
251 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
252 seqex ⊢ seq 1 ( + , 𝐻 ) ∈ V
253 252 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐻 ) ∈ V )
254 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) = ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) )
255 250 251 253 254 clim2 ⊢ ( 𝜑 → ( seq 1 ( + , 𝐻 ) ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) ) ) )
256 121 122 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 1 ) ∈ ℤ )
257 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
258 257 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ V )
259 1 2 3 4 5 6 7 isercolllem3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) = ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) )
260 123 256 258 259 clim2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ↔ ( 𝐴 ∈ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ ( 𝐺 ‘ 1 ) ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) ∈ ℂ ∧ ( abs ‘ ( ( seq 1 ( + , 𝐻 ) ‘ ( ♯ ‘ ( 𝐺 “ ( ◡ 𝐺 “ ( 𝑀 ... 𝑚 ) ) ) ) ) − 𝐴 ) ) < 𝑥 ) ) ) )
261 249 255 260 3bitr4d ⊢ ( 𝜑 → ( seq 1 ( + , 𝐻 ) ⇝ 𝐴 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 ) )