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 15704

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 12899	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
3	1, 2	eqsstri 4030	. . . . . . . . 9 ⊢ 𝑍 ⊆ ℤ
4		isercoll.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)
5	4	ffvelcdmda 7104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍)
6	3, 5	sselid 3981	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ)
7		nnz 12634	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
8	7	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ)
9		fzfid 14014	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin)
10		ffun 6739	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11		funimacnv 6647	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13		inss1 4237	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
14	12, 13	eqsstrdi 4028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
15	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
16	9, 15	ssfid 9301	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
17		hashcl 14395	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀)
18		nn0z 12638	. . . . . . . . . . . 12 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
19	16, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20		ssid 4006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℕ
21		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℤ)
22		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))
23	1, 21, 4, 22	isercolllem1 15701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
24	20, 23	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25		ffn 6736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ)
26		fnresdm 6687	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
27		isoeq1 7337	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
28	4, 25, 26, 27	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
29	24, 28	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
30		isof1o 7343	. . . . . . . . . . . . . . . . . 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 6566	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ^◡𝐺))
35	4, 33, 34	sylanbrc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍)
36	35	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍)
37		fz1ssnn 13595	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
38		ovex 7464	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑛) ∈ V
39	38	f1imaen 9057	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
40	36, 37, 39	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
41		fzfid 14014	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin)
42		enfii 9226	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
43	41, 40, 42	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
44		hashen 14386	. . . . . . . . . . . . . . 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 12533	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
48	47	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ₀)
49		hashfz1 14385	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(1...𝑛)) = 𝑛)
51	46, 50	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛)
52		elfznn 13593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
53	52	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
54		zssre 12620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℤ ⊆ ℝ
55	3, 54	sstri 3993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 ⊆ ℝ
56	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍)
57		ffvelcdm 7101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍)
58	56, 52, 57	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍)
59	55, 58	sselid 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ)
60	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍)
61	55, 60	sselid 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ)
62		eluzelz 12888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ)
63	62	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
64	63	zred 12722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
65		elfzle2 13568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛)
66	65	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛)
67	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
68		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
69		isorel 7346	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
70	67, 68, 53, 69	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
72	53	nnred 12281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
73	68	nnred 12281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
74	72, 73	lenltd 11407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦))
75	59, 61	lenltd 11407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
76	71, 74, 75	3bitr4d 311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛)))
77	66, 76	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛))
78		eluzle 12891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
80	59, 61, 64, 77, 79	letrd 11418	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚)
81	58, 1	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ_≥‘𝑀))
82		elfz5 13556	. . . . . . . . . . . . . . . . . . . 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 7078	. . . . . . . . . . . . . . . . . . 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 3989	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)))
92		imass2 6120	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
93	91, 92	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
94		ssdomg 9040	. . . . . . . . . . . . . 14 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
95	16, 93, 94	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
96		hashdom 14418	. . . . . . . . . . . . . 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 5167	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
100		eluz2 12884	. . . . . . . . . . 11 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
101	8, 19, 99, 100	syl3anbrc 1344	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛))
102		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
103	102	eleq1d 2826	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
104	102	fvoveq1d 7453	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)))
105	104	breq1d 5153	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
106	103, 105	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
107	106	rspcv 3618	. . . . . . . . . 10 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
108	101, 107	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109	108	ralrimdva 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110		fveq2 6906	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝐺‘𝑛)))
111	110	raleqdv 3326	. . . . . . . . 9 ⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112	111	rspcev 3622	. . . . . . . 8 ⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
113	6, 109, 112	syl6an 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114	113	rexlimdva 3155	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
115		1nn 12277	. . . . . . . . 9 ⊢ 1 ∈ ℕ
116		ffvelcdm 7101	. . . . . . . . 9 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
117	4, 115, 116	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ 𝑍)
118	117, 1	eleqtrdi 2851	. . . . . . 7 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
119		eluzelz 12888	. . . . . . 7 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
120		eqid 2737	. . . . . . . 8 ⊢ (ℤ_≥‘(𝐺‘1)) = (ℤ_≥‘(𝐺‘1))
121	120	rexuz3 15387	. . . . . . 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 14014	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
125		funimacnv 6647	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
126	4, 10, 125	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
127		inss1 4237	. . . . . . . . . . 11 ⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
128	126, 127	eqsstrdi 4028	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
129	128	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
130	124, 129	ssfid 9301	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
131		hashcl 14395	. . . . . . . 8 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀)
132		nn0p1nn 12565	. . . . . . . 8 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
133	130, 131, 132	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
134		eluzle 12891	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
135	134	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
136	130	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
137		nn0z 12638	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
138	136, 131, 137	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
139		eluzelz 12888	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
140	139	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
141		zltp1le 12667	. . . . . . . . . . . . . . 15 ⊢ (((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
142	138, 140, 141	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
143	135, 142	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘)
144		nn0re 12535	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
145	130, 131, 144	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
146	145	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
147		eluznn 12960	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
148	133, 147	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
149	148	nnred 12281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
150	146, 149	ltnled 11408	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
151	143, 150	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
152		fzss2 13604	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗))
153		imass2 6120	. . . . . . . . . . . . . 14 ⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)))
154		imass2 6120	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
155	152, 153, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
156		ssdomg 9040	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
157	136, 156	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
158	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
159	158	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍)
160	159, 1	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ_≥‘𝑀))
161	158, 148	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍)
162	3, 161	sselid 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ)
163	162	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ)
164		elfz5 13556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑥) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
165	160, 163, 164	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
166	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
167		nnssre 12270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ ⊆ ℝ
168		ressxr 11305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℝ^*
169	167, 168	sstri 3993	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ ⊆ ℝ^*
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ^*)
171		imassrn 6089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 “ ℕ) ⊆ ran 𝐺
172	158	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
173	172	frnd 6744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍)
174	173, 55	sstrdi 3996	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
175	171, 174	sstrid 3995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
176	175, 168	sstrdi 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ^*)
177		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
178	148	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
179		leisorel 14499	. . . . . . . . . . . . . . . . . . . . 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 7078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
184	158, 25, 183	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
185		fznn 13632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
186	140, 185	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
187	182, 184, 186	3bitr4d 311	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
188	187	eqrdv 2735	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘))
189	188	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘)))
190	189	sseq1d 4015	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
191	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍)
192		fz1ssnn 13595	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑘) ⊆ ℕ
193		ovex 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑘) ∈ V
194	193	f1imaen 9057	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
195	191, 192, 194	sylancl 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
196		fzfid 14014	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
197		enfii 9226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
198	196, 195, 197	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
199		hashen 14386	. . . . . . . . . . . . . . . . . . 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 12533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
203		hashfz1 14385	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → (♯‘(1...𝑘)) = 𝑘)
204	148, 202, 203	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘)
205	201, 204	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘)
206	205	breq1d 5153	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
207		hashdom 14418	. . . . . . . . . . . . . . . 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 12888	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑗 ∈ ℤ)
214	213	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
215		uztric 12902	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
216	162, 214, 215	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
217	216	ord 865	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
218	212, 217	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗))
219		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘)))
220	219	imaeq2d 6078	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐺‘𝑘) → (^◡𝐺 “ (𝑀...𝑚)) = (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))
221	220	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))
222	221	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))))
223	222	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))))
224	223	eleq1d 2826	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ))
225	223	fvoveq1d 7453	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)))
226	225	breq1d 5153	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))
227	224, 226	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
228	227	rspcv 3618	. . . . . . . . . 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 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘)
232	231	fveq2d 6910	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
233	232	eleq1d 2826	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
234	232	fvoveq1d 7453	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
235	234	breq1d 5153	. . . . . . . . . 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 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
239		fveq2 6906	. . . . . . . . 9 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)))
240	239	raleqdv 3326	. . . . . . . 8 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
241	240	rspcev 3622	. . . . . . 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 3155	. . . . 5 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244	123, 243	impbid 212	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
245	244	ralbidv 3178	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
246	245	anbi2d 630	. 2 ⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
247		nnuz 12921	. . 3 ⊢ ℕ = (ℤ_≥‘1)
248		1zzd 12648	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
249		seqex 14044	. . . 4 ⊢ seq1( + , 𝐻) ∈ V
250	249	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐻) ∈ V)
251		eqidd 2738	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
252	247, 248, 250, 251	clim2 15540	. 2 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
253	118, 119	syl 17	. . 3 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
254		seqex 14044	. . . 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 15703	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
260	120, 253, 255, 259	clim2 15540	. 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 848 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∖ cdif 3948 ∩ cin 3950 ⊆ wss 3951 class class class wbr 5143 ^◡ccnv 5684 ran crn 5686 ↾ cres 5687 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 ≈ cen 8982 ≼ cdom 8983 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 ℝ⁺crp 13034 ...cfz 13547 seqcseq 14042 ♯chash 14369 abscabs 15273 ⇝ cli 15520

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-oadd 8510 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-fz 13548 df-seq 14043 df-hash 14370 df-clim 15524

This theorem is referenced by: isercoll2 15705

W3C validator