MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isercoll Structured version   Visualization version   GIF version

Theorem isercoll 15388
Description: Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
isercoll.z 𝑍 = (ℤ𝑀)
isercoll.m (𝜑𝑀 ∈ ℤ)
isercoll.g (𝜑𝐺:ℕ⟶𝑍)
isercoll.i ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
isercoll.0 ((𝜑𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹𝑛) = 0)
isercoll.f ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ ℂ)
isercoll.h ((𝜑𝑘 ∈ ℕ) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
Assertion
Ref Expression
isercoll (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))
Distinct variable groups:   𝑘,𝑛,𝐴   𝑘,𝐹,𝑛   𝜑,𝑘,𝑛   𝑘,𝐺,𝑛   𝑘,𝐻,𝑛   𝑘,𝑀,𝑛   𝑛,𝑍
Allowed substitution hint:   𝑍(𝑘)

Proof of Theorem isercoll
Dummy variables 𝑗 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isercoll.z . . . . . . . . . 10 𝑍 = (ℤ𝑀)
2 uzssz 12612 . . . . . . . . . 10 (ℤ𝑀) ⊆ ℤ
31, 2eqsstri 3956 . . . . . . . . 9 𝑍 ⊆ ℤ
4 isercoll.g . . . . . . . . . 10 (𝜑𝐺:ℕ⟶𝑍)
54ffvelrnda 6970 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ 𝑍)
63, 5sselid 3920 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℤ)
7 nnz 12351 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
87ad2antlr 724 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝑛 ∈ ℤ)
9 fzfid 13702 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝑀...𝑚) ∈ Fin)
10 ffun 6612 . . . . . . . . . . . . . . . 16 (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11 funimacnv 6522 . . . . . . . . . . . . . . . 16 (Fun 𝐺 → (𝐺 “ (𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
124, 10, 113syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 “ (𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13 inss1 4163 . . . . . . . . . . . . . . 15 ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
1412, 13eqsstrdi 3976 . . . . . . . . . . . . . 14 (𝜑 → (𝐺 “ (𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
1514ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
169, 15ssfid 9051 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (𝐺 “ (𝑀...𝑚))) ∈ Fin)
17 hashcl 14080 . . . . . . . . . . . 12 ((𝐺 “ (𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ ℕ0)
18 nn0z 12352 . . . . . . . . . . . 12 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ ℕ0 → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
1916, 17, 183syl 18 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20 ssid 3944 . . . . . . . . . . . . . . . . . . . 20 ℕ ⊆ ℕ
21 isercoll.m . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ ℤ)
22 isercoll.i . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) < (𝐺‘(𝑘 + 1)))
231, 21, 4, 22isercolllem1 15385 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
2420, 23mpan2 688 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25 ffn 6609 . . . . . . . . . . . . . . . . . . . 20 (𝐺:ℕ⟶𝑍𝐺 Fn ℕ)
26 fnresdm 6560 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
27 isoeq1 7197 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
284, 25, 26, 274syl 19 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
2924, 28mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
30 isof1o 7203 . . . . . . . . . . . . . . . . . 18 (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
31 f1ocnv 6737 . . . . . . . . . . . . . . . . . 18 (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → 𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
32 f1ofun 6727 . . . . . . . . . . . . . . . . . 18 (𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun 𝐺)
3329, 30, 31, 324syl 19 . . . . . . . . . . . . . . . . 17 (𝜑 → Fun 𝐺)
34 df-f1 6442 . . . . . . . . . . . . . . . . 17 (𝐺:ℕ–1-1𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun 𝐺))
354, 33, 34sylanbrc 583 . . . . . . . . . . . . . . . 16 (𝜑𝐺:ℕ–1-1𝑍)
3635ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝐺:ℕ–1-1𝑍)
37 fz1ssnn 13296 . . . . . . . . . . . . . . 15 (1...𝑛) ⊆ ℕ
38 ovex 7317 . . . . . . . . . . . . . . . 16 (1...𝑛) ∈ V
3938f1imaen 8811 . . . . . . . . . . . . . . 15 ((𝐺:ℕ–1-1𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
4036, 37, 39sylancl 586 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
41 fzfid 13702 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (1...𝑛) ∈ Fin)
42 enfii 8981 . . . . . . . . . . . . . . . 16 (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
4341, 40, 42syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
44 hashen 14070 . . . . . . . . . . . . . . 15 (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
4543, 41, 44syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
4640, 45mpbird 256 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)))
47 nnnn0 12249 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
4847ad2antlr 724 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝑛 ∈ ℕ0)
49 hashfz1 14069 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (♯‘(1...𝑛)) = 𝑛)
5048, 49syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(1...𝑛)) = 𝑛)
5146, 50eqtrd 2779 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛)
52 elfznn 13294 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
5352adantl 482 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
54 zssre 12335 . . . . . . . . . . . . . . . . . . . . . 22 ℤ ⊆ ℝ
553, 54sstri 3931 . . . . . . . . . . . . . . . . . . . . 21 𝑍 ⊆ ℝ
564ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝐺:ℕ⟶𝑍)
57 ffvelrn 6968 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺:ℕ⟶𝑍𝑦 ∈ ℕ) → (𝐺𝑦) ∈ 𝑍)
5856, 52, 57syl2an 596 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ∈ 𝑍)
5955, 58sselid 3920 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ∈ ℝ)
605ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑛) ∈ 𝑍)
6155, 60sselid 3920 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑛) ∈ ℝ)
62 eluzelz 12601 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (ℤ‘(𝐺𝑛)) → 𝑚 ∈ ℤ)
6362ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
6463zred 12435 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
65 elfzle2 13269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ (1...𝑛) → 𝑦𝑛)
6665adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦𝑛)
6729ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
68 simpllr 773 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
69 isorel 7206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺𝑛) < (𝐺𝑦)))
7067, 68, 53, 69syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺𝑛) < (𝐺𝑦)))
7170notbid 318 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺𝑛) < (𝐺𝑦)))
7253nnred 11997 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
7368nnred 11997 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
7472, 73lenltd 11130 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦𝑛 ↔ ¬ 𝑛 < 𝑦))
7559, 61lenltd 11130 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺𝑦) ≤ (𝐺𝑛) ↔ ¬ (𝐺𝑛) < (𝐺𝑦)))
7671, 74, 753bitr4d 311 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦𝑛 ↔ (𝐺𝑦) ≤ (𝐺𝑛)))
7766, 76mpbid 231 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ≤ (𝐺𝑛))
78 eluzle 12604 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ (ℤ‘(𝐺𝑛)) → (𝐺𝑛) ≤ 𝑚)
7978ad2antlr 724 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑛) ≤ 𝑚)
8059, 61, 64, 77, 79letrd 11141 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ≤ 𝑚)
8158, 1eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ∈ (ℤ𝑀))
82 elfz5 13257 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑦) ∈ (ℤ𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺𝑦) ∈ (𝑀...𝑚) ↔ (𝐺𝑦) ≤ 𝑚))
8381, 63, 82syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺𝑦) ∈ (𝑀...𝑚) ↔ (𝐺𝑦) ≤ 𝑚))
8480, 83mpbird 256 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺𝑦) ∈ (𝑀...𝑚))
8556ffnd 6610 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝐺 Fn ℕ)
8685adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ)
87 elpreima 6944 . . . . . . . . . . . . . . . . . . 19 (𝐺 Fn ℕ → (𝑦 ∈ (𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺𝑦) ∈ (𝑀...𝑚))))
8886, 87syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ∈ (𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺𝑦) ∈ (𝑀...𝑚))))
8953, 84, 88mpbir2and 710 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ (𝐺 “ (𝑀...𝑚)))
9089ex 413 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝑦 ∈ (1...𝑛) → 𝑦 ∈ (𝐺 “ (𝑀...𝑚))))
9190ssrdv 3928 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (1...𝑛) ⊆ (𝐺 “ (𝑀...𝑚)))
92 imass2 6013 . . . . . . . . . . . . . . 15 ((1...𝑛) ⊆ (𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑚))))
9391, 92syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑚))))
94 ssdomg 8795 . . . . . . . . . . . . . 14 ((𝐺 “ (𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑚)))))
9516, 93, 94sylc 65 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑚))))
96 hashdom 14103 . . . . . . . . . . . . . 14 (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (𝐺 “ (𝐺 “ (𝑀...𝑚))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑚)))))
9743, 16, 96syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑚)))))
9895, 97mpbird 256 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))))
9951, 98eqbrtrrd 5099 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))))
100 eluz2 12597 . . . . . . . . . . 11 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ (ℤ𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))))
1018, 19, 99, 100syl3anbrc 1342 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ (ℤ𝑛))
102 fveq2 6783 . . . . . . . . . . . . 13 (𝑘 = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))))
103102eleq1d 2824 . . . . . . . . . . . 12 (𝑘 = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
104102fvoveq1d 7306 . . . . . . . . . . . . 13 (𝑘 = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)))
105104breq1d 5085 . . . . . . . . . . . 12 (𝑘 = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
106103, 105anbi12d 631 . . . . . . . . . . 11 (𝑘 = (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
107106rspcv 3558 . . . . . . . . . 10 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) ∈ (ℤ𝑛) → (∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
108101, 107syl 17 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ‘(𝐺𝑛))) → (∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109108ralrimdva 3107 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ‘(𝐺𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110 fveq2 6783 . . . . . . . . . 10 (𝑗 = (𝐺𝑛) → (ℤ𝑗) = (ℤ‘(𝐺𝑛)))
111110raleqdv 3349 . . . . . . . . 9 (𝑗 = (𝐺𝑛) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ‘(𝐺𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112111rspcev 3562 . . . . . . . 8 (((𝐺𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ‘(𝐺𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
1136, 109, 112syl6an 681 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114113rexlimdva 3214 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
115 1nn 11993 . . . . . . . . 9 1 ∈ ℕ
116 ffvelrn 6968 . . . . . . . . 9 ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
1174, 115, 116sylancl 586 . . . . . . . 8 (𝜑 → (𝐺‘1) ∈ 𝑍)
118117, 1eleqtrdi 2850 . . . . . . 7 (𝜑 → (𝐺‘1) ∈ (ℤ𝑀))
119 eluzelz 12601 . . . . . . 7 ((𝐺‘1) ∈ (ℤ𝑀) → (𝐺‘1) ∈ ℤ)
120 eqid 2739 . . . . . . . 8 (ℤ‘(𝐺‘1)) = (ℤ‘(𝐺‘1))
121120rexuz3 15069 . . . . . . 7 ((𝐺‘1) ∈ ℤ → (∃𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
122118, 119, 1213syl 18 . . . . . 6 (𝜑 → (∃𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
123114, 122sylibrd 258 . . . . 5 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
124 fzfid 13702 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
125 funimacnv 6522 . . . . . . . . . . . 12 (Fun 𝐺 → (𝐺 “ (𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
1264, 10, 1253syl 18 . . . . . . . . . . 11 (𝜑 → (𝐺 “ (𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
127 inss1 4163 . . . . . . . . . . 11 ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
128126, 127eqsstrdi 3976 . . . . . . . . . 10 (𝜑 → (𝐺 “ (𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
129128adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
130124, 129ssfid 9051 . . . . . . . 8 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (𝐺 “ (𝐺 “ (𝑀...𝑗))) ∈ Fin)
131 hashcl 14080 . . . . . . . 8 ((𝐺 “ (𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℕ0)
132 nn0p1nn 12281 . . . . . . . 8 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
133130, 131, 1323syl 18 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
134 eluzle 12604 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
135134adantl 482 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
136130adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (𝐺 “ (𝑀...𝑗))) ∈ Fin)
137 nn0z 12352 . . . . . . . . . . . . . . . 16 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
138136, 131, 1373syl 18 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
139 eluzelz 12601 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
140139adantl 482 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
141 zltp1le 12379 . . . . . . . . . . . . . . 15 (((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
142138, 140, 141syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
143135, 142mpbird 256 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) < 𝑘)
144 nn0re 12251 . . . . . . . . . . . . . . . 16 ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℕ0 → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
145130, 131, 1443syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
146145adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
147 eluznn 12667 . . . . . . . . . . . . . . . 16 ((((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
148133, 147sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
149148nnred 11997 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
150146, 149ltnled 11131 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗))))))
151143, 150mpbid 231 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))))
152 fzss2 13305 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ‘(𝐺𝑘)) → (𝑀...(𝐺𝑘)) ⊆ (𝑀...𝑗))
153 imass2 6013 . . . . . . . . . . . . . 14 ((𝑀...(𝐺𝑘)) ⊆ (𝑀...𝑗) → (𝐺 “ (𝑀...(𝐺𝑘))) ⊆ (𝐺 “ (𝑀...𝑗)))
154 imass2 6013 . . . . . . . . . . . . . 14 ((𝐺 “ (𝑀...(𝐺𝑘))) ⊆ (𝐺 “ (𝑀...𝑗)) → (𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))))
155152, 153, 1543syl 18 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ‘(𝐺𝑘)) → (𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))))
156 ssdomg 8795 . . . . . . . . . . . . . . 15 ((𝐺 “ (𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
157136, 156syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
1584ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
159158ffvelrnda 6970 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑥) ∈ 𝑍)
160159, 1eleqtrdi 2850 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑥) ∈ (ℤ𝑀))
161158, 148ffvelrnd 6971 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺𝑘) ∈ 𝑍)
1623, 161sselid 3920 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺𝑘) ∈ ℤ)
163162adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺𝑘) ∈ ℤ)
164 elfz5 13257 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑥) ∈ (ℤ𝑀) ∧ (𝐺𝑘) ∈ ℤ) → ((𝐺𝑥) ∈ (𝑀...(𝐺𝑘)) ↔ (𝐺𝑥) ≤ (𝐺𝑘)))
165160, 163, 164syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺𝑥) ∈ (𝑀...(𝐺𝑘)) ↔ (𝐺𝑥) ≤ (𝐺𝑘)))
16629ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
167 nnssre 11986 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ ⊆ ℝ
168 ressxr 11028 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ⊆ ℝ*
169167, 168sstri 3931 . . . . . . . . . . . . . . . . . . . . . 22 ℕ ⊆ ℝ*
170169a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ*)
171 imassrn 5983 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 “ ℕ) ⊆ ran 𝐺
172158adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
173172frnd 6617 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺𝑍)
174173, 55sstrdi 3934 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
175171, 174sstrid 3933 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
176175, 168sstrdi 3934 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ*)
177 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
178148adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
179 leisorel 14183 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ* ∧ (𝐺 “ ℕ) ⊆ ℝ*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥𝑘 ↔ (𝐺𝑥) ≤ (𝐺𝑘)))
180166, 170, 176, 177, 178, 179syl122anc 1378 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥𝑘 ↔ (𝐺𝑥) ≤ (𝐺𝑘)))
181165, 180bitr4d 281 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺𝑥) ∈ (𝑀...(𝐺𝑘)) ↔ 𝑥𝑘))
182181pm5.32da 579 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺𝑥) ∈ (𝑀...(𝐺𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥𝑘)))
183 elpreima 6944 . . . . . . . . . . . . . . . . . . 19 (𝐺 Fn ℕ → (𝑥 ∈ (𝐺 “ (𝑀...(𝐺𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺𝑥) ∈ (𝑀...(𝐺𝑘)))))
184158, 25, 1833syl 18 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (𝐺 “ (𝑀...(𝐺𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺𝑥) ∈ (𝑀...(𝐺𝑘)))))
185 fznn 13333 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥𝑘)))
186140, 185syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥𝑘)))
187182, 184, 1863bitr4d 311 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (𝐺 “ (𝑀...(𝐺𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
188187eqrdv 2737 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (𝑀...(𝐺𝑘))) = (1...𝑘))
189188imaeq2d 5972 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))) = (𝐺 “ (1...𝑘)))
190189sseq1d 3953 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
19135ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1𝑍)
192 fz1ssnn 13296 . . . . . . . . . . . . . . . . . . 19 (1...𝑘) ⊆ ℕ
193 ovex 7317 . . . . . . . . . . . . . . . . . . . 20 (1...𝑘) ∈ V
194193f1imaen 8811 . . . . . . . . . . . . . . . . . . 19 ((𝐺:ℕ–1-1𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
195191, 192, 194sylancl 586 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
196 fzfid 13702 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
197 enfii 8981 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
198196, 195, 197syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
199 hashen 14070 . . . . . . . . . . . . . . . . . . 19 (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (1...𝑘) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
200198, 196, 199syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
201195, 200mpbird 256 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)))
202 nnnn0 12249 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
203 hashfz1 14069 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0 → (♯‘(1...𝑘)) = 𝑘)
204148, 202, 2033syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘)
205201, 204eqtrd 2779 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘)
206205breq1d 5085 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗))))))
207 hashdom 14103 . . . . . . . . . . . . . . . 16 (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (𝐺 “ (𝐺 “ (𝑀...𝑗))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
208198, 136, 207syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
209206, 208bitr3d 280 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (𝐺 “ (𝑀...𝑗)))))
210157, 190, 2093imtr4d 294 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))) ⊆ (𝐺 “ (𝐺 “ (𝑀...𝑗))) → 𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗))))))
211155, 210syl5 34 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ‘(𝐺𝑘)) → 𝑘 ≤ (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗))))))
212151, 211mtod 197 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑗 ∈ (ℤ‘(𝐺𝑘)))
213 eluzelz 12601 . . . . . . . . . . . . . 14 (𝑗 ∈ (ℤ‘(𝐺‘1)) → 𝑗 ∈ ℤ)
214213ad2antlr 724 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
215 uztric 12615 . . . . . . . . . . . . 13 (((𝐺𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ‘(𝐺𝑘)) ∨ (𝐺𝑘) ∈ (ℤ𝑗)))
216162, 214, 215syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ‘(𝐺𝑘)) ∨ (𝐺𝑘) ∈ (ℤ𝑗)))
217216ord 861 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ‘(𝐺𝑘)) → (𝐺𝑘) ∈ (ℤ𝑗)))
218212, 217mpd 15 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺𝑘) ∈ (ℤ𝑗))
219 oveq2 7292 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝐺𝑘) → (𝑀...𝑚) = (𝑀...(𝐺𝑘)))
220219imaeq2d 5972 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐺𝑘) → (𝐺 “ (𝑀...𝑚)) = (𝐺 “ (𝑀...(𝐺𝑘))))
221220imaeq2d 5972 . . . . . . . . . . . . . . 15 (𝑚 = (𝐺𝑘) → (𝐺 “ (𝐺 “ (𝑀...𝑚))) = (𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))
222221fveq2d 6787 . . . . . . . . . . . . . 14 (𝑚 = (𝐺𝑘) → (♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘))))))
223222fveq2d 6787 . . . . . . . . . . . . 13 (𝑚 = (𝐺𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))))
224223eleq1d 2824 . . . . . . . . . . . 12 (𝑚 = (𝐺𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ))
225223fvoveq1d 7306 . . . . . . . . . . . . 13 (𝑚 = (𝐺𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)))
226225breq1d 5085 . . . . . . . . . . . 12 (𝑚 = (𝐺𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥))
227224, 226anbi12d 631 . . . . . . . . . . 11 (𝑚 = (𝐺𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥)))
228227rspcv 3558 . . . . . . . . . 10 ((𝐺𝑘) ∈ (ℤ𝑗) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥)))
229218, 228syl 17 . . . . . . . . 9 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥)))
230189fveq2d 6787 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘))))) = (♯‘(𝐺 “ (1...𝑘))))
231230, 205eqtrd 2779 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘))))) = 𝑘)
232231fveq2d 6787 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
233232eleq1d 2824 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
234232fvoveq1d 7306 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
235234breq1d 5085 . . . . . . . . . 10 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
236233, 235anbi12d 631 . . . . . . . . 9 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...(𝐺𝑘)))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
237229, 236sylibd 238 . . . . . . . 8 (((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
238237ralrimdva 3107 . . . . . . 7 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
239 fveq2 6783 . . . . . . . . 9 (𝑛 = ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ𝑛) = (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1)))
240239raleqdv 3349 . . . . . . . 8 (𝑛 = ((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
241240rspcev 3562 . . . . . . 7 ((((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ‘((♯‘(𝐺 “ (𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
242133, 238, 241syl6an 681 . . . . . 6 ((𝜑𝑗 ∈ (ℤ‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
243242rexlimdva 3214 . . . . 5 (𝜑 → (∃𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244123, 243impbid 211 . . . 4 (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
245244ralbidv 3113 . . 3 (𝜑 → (∀𝑥 ∈ ℝ+𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
246245anbi2d 629 . 2 (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
247 nnuz 12630 . . 3 ℕ = (ℤ‘1)
248 1zzd 12360 . . 3 (𝜑 → 1 ∈ ℤ)
249 seqex 13732 . . . 4 seq1( + , 𝐻) ∈ V
250249a1i 11 . . 3 (𝜑 → seq1( + , 𝐻) ∈ V)
251 eqidd 2740 . . 3 ((𝜑𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
252247, 248, 250, 251clim2 15222 . 2 (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
253118, 119syl 17 . . 3 (𝜑 → (𝐺‘1) ∈ ℤ)
254 seqex 13732 . . . 4 seq𝑀( + , 𝐹) ∈ V
255254a1i 11 . . 3 (𝜑 → seq𝑀( + , 𝐹) ∈ V)
256 isercoll.0 . . . 4 ((𝜑𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹𝑛) = 0)
257 isercoll.f . . . 4 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ ℂ)
258 isercoll.h . . . 4 ((𝜑𝑘 ∈ ℕ) → (𝐻𝑘) = (𝐹‘(𝐺𝑘)))
2591, 21, 4, 22, 256, 257, 258isercolllem3 15387 . . 3 ((𝜑𝑚 ∈ (ℤ‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))))
260120, 253, 255, 259clim2 15222 . 2 (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ (ℤ‘(𝐺‘1))∀𝑚 ∈ (ℤ𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
261246, 252, 2603bitr4d 311 1 (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1539  wcel 2107  wral 3065  wrex 3066  Vcvv 3433  cdif 3885  cin 3887  wss 3888   class class class wbr 5075  ccnv 5589  ran crn 5591  cres 5592  cima 5593  Fun wfun 6431   Fn wfn 6432  wf 6433  1-1wf1 6434  1-1-ontowf1o 6436  cfv 6437   Isom wiso 6438  (class class class)co 7284  cen 8739  cdom 8740  Fincfn 8742  cc 10878  cr 10879  0cc0 10880  1c1 10881   + caddc 10883  *cxr 11017   < clt 11018  cle 11019  cmin 11214  cn 11982  0cn0 12242  cz 12328  cuz 12591  +crp 12739  ...cfz 13248  seqcseq 13730  chash 14053  abscabs 14954  cli 15202
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-oadd 8310  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-sup 9210  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-xnn0 12315  df-z 12329  df-uz 12592  df-fz 13249  df-seq 13731  df-hash 14054  df-clim 15206
This theorem is referenced by:  isercoll2  15389
  Copyright terms: Public domain W3C validator