isercoll - Metamath Proof Explorer

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

Theorem isercoll 15591

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.

Step	Hyp	Ref	Expression
1		isercoll.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ_≥‘𝑀)
2		uzssz 12772	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
3	1, 2	eqsstri 3980	. . . . . . . . 9 ⊢ 𝑍 ⊆ ℤ
4		isercoll.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)
5	4	ffvelcdmda 7029	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍)
6	3, 5	sselid 3931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ)
7		nnz 12509	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
8	7	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ)
9		fzfid 13896	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin)
10		ffun 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11		funimacnv 6573	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13		inss1 4189	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
14	12, 13	eqsstrdi 3978	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
15	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
16	9, 15	ssfid 9169	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
17		hashcl 14279	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀)
18		nn0z 12512	. . . . . . . . . . . 12 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
19	16, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20		ssid 3956	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℕ
21		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℤ)
22		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))
23	1, 21, 4, 22	isercolllem1 15588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
24	20, 23	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25		ffn 6662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ)
26		fnresdm 6611	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
27		isoeq1 7263	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
28	4, 25, 26, 27	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
29	24, 28	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
30		isof1o 7269	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
31		f1ocnv 6786	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
32		f1ofun 6776	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ^◡𝐺)
33	29, 30, 31, 32	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Fun ^◡𝐺)
34		df-f1 6497	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ^◡𝐺))
35	4, 33, 34	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍)
36	35	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍)
37		fz1ssnn 13471	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
38		ovex 7391	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑛) ∈ V
39	38	f1imaen 8954	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
40	36, 37, 39	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
41		fzfid 13896	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin)
42		enfii 9110	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
43	41, 40, 42	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
44		hashen 14270	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
45	43, 41, 44	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
46	40, 45	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)))
47		nnnn0 12408	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
48	47	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ₀)
49		hashfz1 14269	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(1...𝑛)) = 𝑛)
51	46, 50	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛)
52		elfznn 13469	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
53	52	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
54		zssre 12495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℤ ⊆ ℝ
55	3, 54	sstri 3943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 ⊆ ℝ
56	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍)
57		ffvelcdm 7026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍)
58	56, 52, 57	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍)
59	55, 58	sselid 3931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ)
60	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍)
61	55, 60	sselid 3931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ)
62		eluzelz 12761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ)
63	62	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
64	63	zred 12596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
65		elfzle2 13444	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛)
66	65	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛)
67	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
68		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
69		isorel 7272	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
70	67, 68, 53, 69	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
72	53	nnred 12160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
73	68	nnred 12160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
74	72, 73	lenltd 11279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦))
75	59, 61	lenltd 11279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
76	71, 74, 75	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛)))
77	66, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛))
78		eluzle 12764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
80	59, 61, 64, 77, 79	letrd 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚)
81	58, 1	eleqtrdi 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ_≥‘𝑀))
82		elfz5 13432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑦) ∈ (ℤ_≥‘𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
83	81, 63, 82	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
84	80, 83	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (𝑀...𝑚))
85	56	ffnd 6663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺 Fn ℕ)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ)
87		elpreima 7003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
88	86, 87	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
89	53, 84, 88	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)))
90	89	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑦 ∈ (1...𝑛) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚))))
91	90	ssrdv 3939	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)))
92		imass2 6061	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
93	91, 92	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
94		ssdomg 8937	. . . . . . . . . . . . . 14 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
95	16, 93, 94	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
96		hashdom 14302	. . . . . . . . . . . . . 14 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
97	43, 16, 96	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
98	95, 97	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
99	51, 98	eqbrtrrd 5122	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
100		eluz2 12757	. . . . . . . . . . 11 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
101	8, 19, 99, 100	syl3anbrc 1344	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛))
102		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
103	102	eleq1d 2821	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
104	102	fvoveq1d 7380	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)))
105	104	breq1d 5108	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
106	103, 105	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
107	106	rspcv 3572	. . . . . . . . . 10 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
108	101, 107	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109	108	ralrimdva 3136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝐺‘𝑛)))
111	110	raleqdv 3296	. . . . . . . . 9 ⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112	111	rspcev 3576	. . . . . . . 8 ⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
113	6, 109, 112	syl6an 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114	113	rexlimdva 3137	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
115		1nn 12156	. . . . . . . . 9 ⊢ 1 ∈ ℕ
116		ffvelcdm 7026	. . . . . . . . 9 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
117	4, 115, 116	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ 𝑍)
118	117, 1	eleqtrdi 2846	. . . . . . 7 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
119		eluzelz 12761	. . . . . . 7 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
120		eqid 2736	. . . . . . . 8 ⊢ (ℤ_≥‘(𝐺‘1)) = (ℤ_≥‘(𝐺‘1))
121	120	rexuz3 15272	. . . . . . 7 ⊢ ((𝐺‘1) ∈ ℤ → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
122	118, 119, 121	3syl 18	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
123	114, 122	sylibrd 259	. . . . 5 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
124		fzfid 13896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
125		funimacnv 6573	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
126	4, 10, 125	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
127		inss1 4189	. . . . . . . . . . 11 ⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
128	126, 127	eqsstrdi 3978	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
129	128	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
130	124, 129	ssfid 9169	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
131		hashcl 14279	. . . . . . . 8 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀)
132		nn0p1nn 12440	. . . . . . . 8 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
133	130, 131, 132	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
134		eluzle 12764	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
135	134	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
136	130	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
137		nn0z 12512	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
138	136, 131, 137	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
139		eluzelz 12761	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
140	139	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
141		zltp1le 12541	. . . . . . . . . . . . . . 15 ⊢ (((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
142	138, 140, 141	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
143	135, 142	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘)
144		nn0re 12410	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
145	130, 131, 144	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
146	145	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
147		eluznn 12831	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
148	133, 147	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
149	148	nnred 12160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
150	146, 149	ltnled 11280	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
151	143, 150	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
152		fzss2 13480	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗))
153		imass2 6061	. . . . . . . . . . . . . 14 ⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)))
154		imass2 6061	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
155	152, 153, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
156		ssdomg 8937	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
157	136, 156	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
158	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
159	158	ffvelcdmda 7029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍)
160	159, 1	eleqtrdi 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ_≥‘𝑀))
161	158, 148	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍)
162	3, 161	sselid 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ)
163	162	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ)
164		elfz5 13432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑥) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
165	160, 163, 164	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
166	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
167		nnssre 12149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ ⊆ ℝ
168		ressxr 11176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℝ^*
169	167, 168	sstri 3943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ ⊆ ℝ^*
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ^*)
171		imassrn 6030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 “ ℕ) ⊆ ran 𝐺
172	158	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
173	172	frnd 6670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍)
174	173, 55	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
175	171, 174	sstrid 3945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
176	175, 168	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ^*)
177		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
178	148	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
179		leisorel 14383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ^* ∧ (𝐺 “ ℕ) ⊆ ℝ^*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
180	166, 170, 176, 177, 178, 179	syl122anc 1381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
181	165, 180	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ 𝑥 ≤ 𝑘))
182	181	pm5.32da 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
183		elpreima 7003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
184	158, 25, 183	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
185		fznn 13508	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
186	140, 185	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
187	182, 184, 186	3bitr4d 311	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
188	187	eqrdv 2734	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘))
189	188	imaeq2d 6019	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘)))
190	189	sseq1d 3965	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
191	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍)
192		fz1ssnn 13471	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑘) ⊆ ℕ
193		ovex 7391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑘) ∈ V
194	193	f1imaen 8954	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
195	191, 192, 194	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
196		fzfid 13896	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
197		enfii 9110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
198	196, 195, 197	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
199		hashen 14270	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (1...𝑘) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
200	198, 196, 199	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
201	195, 200	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)))
202		nnnn0 12408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
203		hashfz1 14269	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → (♯‘(1...𝑘)) = 𝑘)
204	148, 202, 203	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘)
205	201, 204	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘)
206	205	breq1d 5108	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
207		hashdom 14302	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
208	198, 136, 207	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
209	206, 208	bitr3d 281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
210	157, 190, 209	3imtr4d 294	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
211	155, 210	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
212	151, 211	mtod 198	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)))
213		eluzelz 12761	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑗 ∈ ℤ)
214	213	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
215		uztric 12775	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
216	162, 214, 215	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
217	216	ord 864	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
218	212, 217	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗))
219		oveq2 7366	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘)))
220	219	imaeq2d 6019	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐺‘𝑘) → (^◡𝐺 “ (𝑀...𝑚)) = (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))
221	220	imaeq2d 6019	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))
222	221	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))))
223	222	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))))
224	223	eleq1d 2821	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ))
225	223	fvoveq1d 7380	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)))
226	225	breq1d 5108	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))
227	224, 226	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
228	227	rspcv 3572	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘) ∈ (ℤ_≥‘𝑗) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
229	218, 228	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
230	189	fveq2d 6838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = (♯‘(𝐺 “ (1...𝑘))))
231	230, 205	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘)
232	231	fveq2d 6838	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
233	232	eleq1d 2821	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
234	232	fvoveq1d 7380	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
235	234	breq1d 5108	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
236	233, 235	anbi12d 632	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
237	229, 236	sylibd 239	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
238	237	ralrimdva 3136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
239		fveq2 6834	. . . . . . . . 9 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)))
240	239	raleqdv 3296	. . . . . . . 8 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
241	240	rspcev 3576	. . . . . . 7 ⊢ ((((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
242	133, 238, 241	syl6an 684	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
243	242	rexlimdva 3137	. . . . 5 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244	123, 243	impbid 212	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
245	244	ralbidv 3159	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
246	245	anbi2d 630	. 2 ⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
247		nnuz 12790	. . 3 ⊢ ℕ = (ℤ_≥‘1)
248		1zzd 12522	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
249		seqex 13926	. . . 4 ⊢ seq1( + , 𝐻) ∈ V
250	249	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐻) ∈ V)
251		eqidd 2737	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
252	247, 248, 250, 251	clim2 15427	. 2 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
253	118, 119	syl 17	. . 3 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
254		seqex 13926	. . . 4 ⊢ seq𝑀( + , 𝐹) ∈ V
255	254	a1i 11	. . 3 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V)
256		isercoll.0	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0)
257		isercoll.f	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ)
258		isercoll.h	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))
259	1, 21, 4, 22, 256, 257, 258	isercolllem3 15590	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
260	120, 253, 255, 259	clim2 15427	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
261	246, 252, 260	3bitr4d 311	1 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∖ cdif 3898 ∩ cin 3900 ⊆ wss 3901 class class class wbr 5098 ^◡ccnv 5623 ran crn 5625 ↾ cres 5626 “ cima 5627 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 –1-1→wf1 6489 –1-1-onto→wf1o 6491 ‘cfv 6492 Isom wiso 6493 (class class class)co 7358 ≈ cen 8880 ≼ cdom 8881 Fincfn 8883 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167 − cmin 11364 ℕcn 12145 ℕ₀cn0 12401 ℤcz 12488 ℤ_≥cuz 12751 ℝ⁺crp 12905 ...cfz 13423 seqcseq 13924 ♯chash 14253 abscabs 15157 ⇝ cli 15407

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-oadd 8401 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-n0 12402 df-xnn0 12475 df-z 12489 df-uz 12752 df-fz 13424 df-seq 13925 df-hash 14254 df-clim 15411

This theorem is referenced by: isercoll2 15592

W3C validator