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 15700

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 12896	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
3	1, 2	eqsstri 4029	. . . . . . . . 9 ⊢ 𝑍 ⊆ ℤ
4		isercoll.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)
5	4	ffvelcdmda 7103	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍)
6	3, 5	sselid 3992	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ)
7		nnz 12631	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
8	7	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ)
9		fzfid 14010	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin)
10		ffun 6739	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11		funimacnv 6648	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13		inss1 4244	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
14	12, 13	eqsstrdi 4049	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
15	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
16	9, 15	ssfid 9298	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
17		hashcl 14391	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀)
18		nn0z 12635	. . . . . . . . . . . 12 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
19	16, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20		ssid 4017	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℕ
21		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℤ)
22		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))
23	1, 21, 4, 22	isercolllem1 15697	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
24	20, 23	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25		ffn 6736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ)
26		fnresdm 6687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
27		isoeq1 7336	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
28	4, 25, 26, 27	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
29	24, 28	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
30		isof1o 7342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
31		f1ocnv 6860	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
32		f1ofun 6850	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ^◡𝐺)
33	29, 30, 31, 32	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Fun ^◡𝐺)
34		df-f1 6567	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ^◡𝐺))
35	4, 33, 34	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍)
36	35	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍)
37		fz1ssnn 13591	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
38		ovex 7463	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑛) ∈ V
39	38	f1imaen 9055	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
40	36, 37, 39	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
41		fzfid 14010	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin)
42		enfii 9223	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
43	41, 40, 42	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
44		hashen 14382	. . . . . . . . . . . . . . 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 12530	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
48	47	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ₀)
49		hashfz1 14381	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(1...𝑛)) = 𝑛)
51	46, 50	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛)
52		elfznn 13589	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
53	52	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
54		zssre 12617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℤ ⊆ ℝ
55	3, 54	sstri 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 ⊆ ℝ
56	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍)
57		ffvelcdm 7100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍)
58	56, 52, 57	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍)
59	55, 58	sselid 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ)
60	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍)
61	55, 60	sselid 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ)
62		eluzelz 12885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ)
63	62	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
64	63	zred 12719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
65		elfzle2 13564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛)
66	65	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛)
67	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
68		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
69		isorel 7345	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
70	67, 68, 53, 69	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
72	53	nnred 12278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
73	68	nnred 12278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
74	72, 73	lenltd 11404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦))
75	59, 61	lenltd 11404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
76	71, 74, 75	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛)))
77	66, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛))
78		eluzle 12888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
80	59, 61, 64, 77, 79	letrd 11415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚)
81	58, 1	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ_≥‘𝑀))
82		elfz5 13552	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑦) ∈ (ℤ_≥‘𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
83	81, 63, 82	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
84	80, 83	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (𝑀...𝑚))
85	56	ffnd 6737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺 Fn ℕ)
86	85	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ)
87		elpreima 7077	. . . . . . . . . . . . . . . . . . 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 4000	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)))
92		imass2 6122	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
93	91, 92	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
94		ssdomg 9038	. . . . . . . . . . . . . 14 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
95	16, 93, 94	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
96		hashdom 14414	. . . . . . . . . . . . . 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 5171	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
100		eluz2 12881	. . . . . . . . . . 11 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
101	8, 19, 99, 100	syl3anbrc 1342	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛))
102		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
103	102	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
104	102	fvoveq1d 7452	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)))
105	104	breq1d 5157	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
106	103, 105	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
107	106	rspcv 3617	. . . . . . . . . 10 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
108	101, 107	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109	108	ralrimdva 3151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝐺‘𝑛)))
111	110	raleqdv 3323	. . . . . . . . 9 ⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112	111	rspcev 3621	. . . . . . . 8 ⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
113	6, 109, 112	syl6an 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114	113	rexlimdva 3152	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
115		1nn 12274	. . . . . . . . 9 ⊢ 1 ∈ ℕ
116		ffvelcdm 7100	. . . . . . . . 9 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
117	4, 115, 116	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ 𝑍)
118	117, 1	eleqtrdi 2848	. . . . . . 7 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
119		eluzelz 12885	. . . . . . 7 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
120		eqid 2734	. . . . . . . 8 ⊢ (ℤ_≥‘(𝐺‘1)) = (ℤ_≥‘(𝐺‘1))
121	120	rexuz3 15383	. . . . . . 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 14010	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
125		funimacnv 6648	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
126	4, 10, 125	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
127		inss1 4244	. . . . . . . . . . 11 ⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
128	126, 127	eqsstrdi 4049	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
129	128	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
130	124, 129	ssfid 9298	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
131		hashcl 14391	. . . . . . . 8 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀)
132		nn0p1nn 12562	. . . . . . . 8 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
133	130, 131, 132	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
134		eluzle 12888	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
135	134	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
136	130	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
137		nn0z 12635	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
138	136, 131, 137	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
139		eluzelz 12885	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
140	139	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
141		zltp1le 12664	. . . . . . . . . . . . . . 15 ⊢ (((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
142	138, 140, 141	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
143	135, 142	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘)
144		nn0re 12532	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
145	130, 131, 144	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
146	145	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
147		eluznn 12957	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
148	133, 147	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
149	148	nnred 12278	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
150	146, 149	ltnled 11405	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
151	143, 150	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
152		fzss2 13600	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗))
153		imass2 6122	. . . . . . . . . . . . . 14 ⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)))
154		imass2 6122	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
155	152, 153, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
156		ssdomg 9038	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
157	136, 156	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
158	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
159	158	ffvelcdmda 7103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍)
160	159, 1	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ_≥‘𝑀))
161	158, 148	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍)
162	3, 161	sselid 3992	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ)
163	162	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ)
164		elfz5 13552	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑥) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
165	160, 163, 164	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
166	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
167		nnssre 12267	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ ⊆ ℝ
168		ressxr 11302	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℝ^*
169	167, 168	sstri 4004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ ⊆ ℝ^*
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ^*)
171		imassrn 6090	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 “ ℕ) ⊆ ran 𝐺
172	158	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
173	172	frnd 6744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍)
174	173, 55	sstrdi 4007	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
175	171, 174	sstrid 4006	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
176	175, 168	sstrdi 4007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ^*)
177		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
178	148	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
179		leisorel 14495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ^* ∧ (𝐺 “ ℕ) ⊆ ℝ^*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
180	166, 170, 176, 177, 178, 179	syl122anc 1378	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
181	165, 180	bitr4d 282	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ 𝑥 ≤ 𝑘))
182	181	pm5.32da 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
183		elpreima 7077	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
184	158, 25, 183	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
185		fznn 13628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
186	140, 185	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
187	182, 184, 186	3bitr4d 311	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
188	187	eqrdv 2732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘))
189	188	imaeq2d 6079	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘)))
190	189	sseq1d 4026	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
191	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍)
192		fz1ssnn 13591	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑘) ⊆ ℕ
193		ovex 7463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑘) ∈ V
194	193	f1imaen 9055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
195	191, 192, 194	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
196		fzfid 14010	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
197		enfii 9223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
198	196, 195, 197	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
199		hashen 14382	. . . . . . . . . . . . . . . . . . 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 12530	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
203		hashfz1 14381	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → (♯‘(1...𝑘)) = 𝑘)
204	148, 202, 203	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘)
205	201, 204	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘)
206	205	breq1d 5157	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
207		hashdom 14414	. . . . . . . . . . . . . . . 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 12885	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑗 ∈ ℤ)
214	213	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
215		uztric 12899	. . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘)))
220	219	imaeq2d 6079	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐺‘𝑘) → (^◡𝐺 “ (𝑀...𝑚)) = (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))
221	220	imaeq2d 6079	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))
222	221	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))))
223	222	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))))
224	223	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ))
225	223	fvoveq1d 7452	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)))
226	225	breq1d 5157	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))
227	224, 226	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
228	227	rspcv 3617	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘) ∈ (ℤ_≥‘𝑗) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
229	218, 228	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
230	189	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = (♯‘(𝐺 “ (1...𝑘))))
231	230, 205	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘)
232	231	fveq2d 6910	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
233	232	eleq1d 2823	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
234	232	fvoveq1d 7452	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
235	234	breq1d 5157	. . . . . . . . . 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 3151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
239		fveq2 6906	. . . . . . . . 9 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)))
240	239	raleqdv 3323	. . . . . . . 8 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
241	240	rspcev 3621	. . . . . . 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 3152	. . . . 5 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244	123, 243	impbid 212	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
245	244	ralbidv 3175	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
246	245	anbi2d 630	. 2 ⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
247		nnuz 12918	. . 3 ⊢ ℕ = (ℤ_≥‘1)
248		1zzd 12645	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
249		seqex 14040	. . . 4 ⊢ seq1( + , 𝐻) ∈ V
250	249	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐻) ∈ V)
251		eqidd 2735	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
252	247, 248, 250, 251	clim2 15536	. 2 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
253	118, 119	syl 17	. . 3 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
254		seqex 14040	. . . 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 15699	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
260	120, 253, 255, 259	clim2 15536	. 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 1536 ∈ wcel 2105 ∀wral 3058 ∃wrex 3067 Vcvv 3477 ∖ cdif 3959 ∩ cin 3961 ⊆ wss 3962 class class class wbr 5147 ^◡ccnv 5687 ran crn 5689 ↾ cres 5690 “ cima 5691 Fun wfun 6556 Fn wfn 6557 ⟶wf 6558 –1-1→wf1 6559 –1-1-onto→wf1o 6561 ‘cfv 6562 Isom wiso 6563 (class class class)co 7430 ≈ cen 8980 ≼ cdom 8981 Fincfn 8983 ℂcc 11150 ℝcr 11151 0cc0 11152 1c1 11153 + caddc 11155 ℝ^*cxr 11291 < clt 11292 ≤ cle 11293 − cmin 11489 ℕcn 12263 ℕ₀cn0 12523 ℤcz 12610 ℤ_≥cuz 12875 ℝ⁺crp 13031 ...cfz 13543 seqcseq 14038 ♯chash 14365 abscabs 15269 ⇝ cli 15516

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-inf2 9678 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-isom 6571 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-oadd 8508 df-er 8743 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-sup 9479 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-nn 12264 df-n0 12524 df-xnn0 12597 df-z 12611 df-uz 12876 df-fz 13544 df-seq 14039 df-hash 14366 df-clim 15520

This theorem is referenced by: isercoll2 15701

W3C validator