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 15117

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 12345	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
3	1, 2	eqsstri 3911	. . . . . . . . 9 ⊢ 𝑍 ⊆ ℤ
4		isercoll.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)
5	4	ffvelrnda 6861	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍)
6	3, 5	sseldi 3875	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ)
7		nnz 12085	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
8	7	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ)
9		fzfid 13432	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin)
10		ffun 6507	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11		funimacnv 6420	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13		inss1 4119	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
14	12, 13	eqsstrdi 3931	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
15	14	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
16	9, 15	ssfid 8819	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
17		hashcl 13809	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀)
18		nn0z 12086	. . . . . . . . . . . 12 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
19	16, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20		ssid 3899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℕ
21		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℤ)
22		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))
23	1, 21, 4, 22	isercolllem1 15114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
24	20, 23	mpan2 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25		ffn 6504	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ)
26		fnresdm 6455	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
27		isoeq1 7083	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
28	4, 25, 26, 27	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
29	24, 28	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
30		isof1o 7089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
31		f1ocnv 6630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
32		f1ofun 6620	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ^◡𝐺)
33	29, 30, 31, 32	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Fun ^◡𝐺)
34		df-f1 6344	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ^◡𝐺))
35	4, 33, 34	sylanbrc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍)
36	35	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍)
37		fz1ssnn 13029	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
38		ovex 7203	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑛) ∈ V
39	38	f1imaen 8617	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
40	36, 37, 39	sylancl 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
41		fzfid 13432	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin)
42		enfii 8784	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
43	41, 40, 42	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
44		hashen 13799	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
45	43, 41, 44	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
46	40, 45	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = (♯‘(1...𝑛)))
47		nnnn0 11983	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
48	47	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ₀)
49		hashfz1 13798	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (♯‘(1...𝑛)) = 𝑛)
50	48, 49	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(1...𝑛)) = 𝑛)
51	46, 50	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) = 𝑛)
52		elfznn 13027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
53	52	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
54		zssre 12069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℤ ⊆ ℝ
55	3, 54	sstri 3886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 ⊆ ℝ
56	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍)
57		ffvelrn 6859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍)
58	56, 52, 57	syl2an 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍)
59	55, 58	sseldi 3875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ)
60	5	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍)
61	55, 60	sseldi 3875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ)
62		eluzelz 12334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ)
63	62	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
64	63	zred 12168	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
65		elfzle2 13002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛)
66	65	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛)
67	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
68		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
69		isorel 7092	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
70	67, 68, 53, 69	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
71	70	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
72	53	nnred 11731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
73	68	nnred 11731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
74	72, 73	lenltd 10864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦))
75	59, 61	lenltd 10864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
76	71, 74, 75	3bitr4d 314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛)))
77	66, 76	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛))
78		eluzle 12337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
80	59, 61, 64, 77, 79	letrd 10875	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚)
81	58, 1	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ_≥‘𝑀))
82		elfz5 12990	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑦) ∈ (ℤ_≥‘𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
83	81, 63, 82	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
84	80, 83	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (𝑀...𝑚))
85	56	ffnd 6505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺 Fn ℕ)
86	85	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ)
87		elpreima 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
88	86, 87	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
89	53, 84, 88	mpbir2and 713	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)))
90	89	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑦 ∈ (1...𝑛) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚))))
91	90	ssrdv 3883	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)))
92		imass2 5939	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
93	91, 92	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
94		ssdomg 8601	. . . . . . . . . . . . . 14 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
95	16, 93, 94	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
96		hashdom 13832	. . . . . . . . . . . . . 14 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
97	43, 16, 96	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
98	95, 97	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (1...𝑛))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
99	51, 98	eqbrtrrd 5054	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
100		eluz2 12330	. . . . . . . . . . 11 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
101	8, 19, 99, 100	syl3anbrc 1344	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛))
102		fveq2 6674	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
103	102	eleq1d 2817	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
104	102	fvoveq1d 7192	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)))
105	104	breq1d 5040	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
106	103, 105	anbi12d 634	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
107	106	rspcv 3521	. . . . . . . . . 10 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
108	101, 107	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109	108	ralrimdva 3101	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110		fveq2 6674	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝐺‘𝑛)))
111	110	raleqdv 3316	. . . . . . . . 9 ⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112	111	rspcev 3526	. . . . . . . 8 ⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
113	6, 109, 112	syl6an 684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114	113	rexlimdva 3194	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
115		1nn 11727	. . . . . . . . 9 ⊢ 1 ∈ ℕ
116		ffvelrn 6859	. . . . . . . . 9 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
117	4, 115, 116	sylancl 589	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ 𝑍)
118	117, 1	eleqtrdi 2843	. . . . . . 7 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
119		eluzelz 12334	. . . . . . 7 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
120		eqid 2738	. . . . . . . 8 ⊢ (ℤ_≥‘(𝐺‘1)) = (ℤ_≥‘(𝐺‘1))
121	120	rexuz3 14798	. . . . . . 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 262	. . . . 5 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
124		fzfid 13432	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
125		funimacnv 6420	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
126	4, 10, 125	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
127		inss1 4119	. . . . . . . . . . 11 ⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
128	126, 127	eqsstrdi 3931	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
129	128	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
130	124, 129	ssfid 8819	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
131		hashcl 13809	. . . . . . . 8 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀)
132		nn0p1nn 12015	. . . . . . . 8 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
133	130, 131, 132	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
134		eluzle 12337	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
135	134	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
136	130	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
137		nn0z 12086	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
138	136, 131, 137	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
139		eluzelz 12334	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
140	139	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
141		zltp1le 12113	. . . . . . . . . . . . . . 15 ⊢ (((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
142	138, 140, 141	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
143	135, 142	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘)
144		nn0re 11985	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
145	130, 131, 144	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
146	145	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
147		eluznn 12400	. . . . . . . . . . . . . . . 16 ⊢ ((((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
148	133, 147	sylan 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
149	148	nnred 11731	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
150	146, 149	ltnled 10865	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
151	143, 150	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
152		fzss2 13038	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗))
153		imass2 5939	. . . . . . . . . . . . . 14 ⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)))
154		imass2 5939	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
155	152, 153, 154	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
156		ssdomg 8601	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
157	136, 156	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
158	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
159	158	ffvelrnda 6861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍)
160	159, 1	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ_≥‘𝑀))
161	158, 148	ffvelrnd 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍)
162	3, 161	sseldi 3875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ)
163	162	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ)
164		elfz5 12990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑥) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
165	160, 163, 164	syl2anc 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
166	29	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
167		nnssre 11720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ ⊆ ℝ
168		ressxr 10763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℝ^*
169	167, 168	sstri 3886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ ⊆ ℝ^*
170	169	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ^*)
171		imassrn 5914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 “ ℕ) ⊆ ran 𝐺
172	158	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
173	172	frnd 6512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍)
174	173, 55	sstrdi 3889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
175	171, 174	sstrid 3888	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
176	175, 168	sstrdi 3889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ^*)
177		simpr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
178	148	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
179		leisorel 13912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ^* ∧ (𝐺 “ ℕ) ⊆ ℝ^*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
180	166, 170, 176, 177, 178, 179	syl122anc 1380	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
181	165, 180	bitr4d 285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ 𝑥 ≤ 𝑘))
182	181	pm5.32da 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
183		elpreima 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
184	158, 25, 183	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
185		fznn 13066	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
186	140, 185	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
187	182, 184, 186	3bitr4d 314	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
188	187	eqrdv 2736	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘))
189	188	imaeq2d 5903	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘)))
190	189	sseq1d 3908	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
191	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍)
192		fz1ssnn 13029	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑘) ⊆ ℕ
193		ovex 7203	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑘) ∈ V
194	193	f1imaen 8617	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
195	191, 192, 194	sylancl 589	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
196		fzfid 13432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
197		enfii 8784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
198	196, 195, 197	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
199		hashen 13799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (1...𝑘) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
200	198, 196, 199	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
201	195, 200	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = (♯‘(1...𝑘)))
202		nnnn0 11983	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
203		hashfz1 13798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → (♯‘(1...𝑘)) = 𝑘)
204	148, 202, 203	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(1...𝑘)) = 𝑘)
205	201, 204	eqtrd 2773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (1...𝑘))) = 𝑘)
206	205	breq1d 5040	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
207		hashdom 13832	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
208	198, 136, 207	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((♯‘(𝐺 “ (1...𝑘))) ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
209	206, 208	bitr3d 284	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
210	157, 190, 209	3imtr4d 297	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
211	155, 210	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → 𝑘 ≤ (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
212	151, 211	mtod 201	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)))
213		eluzelz 12334	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑗 ∈ ℤ)
214	213	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
215		uztric 12348	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
216	162, 214, 215	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
217	216	ord 863	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
218	212, 217	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗))
219		oveq2 7178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘)))
220	219	imaeq2d 5903	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐺‘𝑘) → (^◡𝐺 “ (𝑀...𝑚)) = (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))
221	220	imaeq2d 5903	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))
222	221	fveq2d 6678	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) = (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))))
223	222	fveq2d 6678	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))))
224	223	eleq1d 2817	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ))
225	223	fvoveq1d 7192	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)))
226	225	breq1d 5040	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))
227	224, 226	anbi12d 634	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
228	227	rspcv 3521	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘) ∈ (ℤ_≥‘𝑗) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
229	218, 228	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
230	189	fveq2d 6678	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = (♯‘(𝐺 “ (1...𝑘))))
231	230, 205	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘)
232	231	fveq2d 6678	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
233	232	eleq1d 2817	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
234	232	fvoveq1d 7192	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
235	234	breq1d 5040	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
236	233, 235	anbi12d 634	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
237	229, 236	sylibd 242	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
238	237	ralrimdva 3101	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
239		fveq2 6674	. . . . . . . . 9 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)))
240	239	raleqdv 3316	. . . . . . . 8 ⊢ (𝑛 = ((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ_≥‘((♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
241	240	rspcev 3526	. . . . . . 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 3194	. . . . 5 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244	123, 243	impbid 215	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
245	244	ralbidv 3109	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
246	245	anbi2d 632	. 2 ⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
247		nnuz 12363	. . 3 ⊢ ℕ = (ℤ_≥‘1)
248		1zzd 12094	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
249		seqex 13462	. . . 4 ⊢ seq1( + , 𝐻) ∈ V
250	249	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐻) ∈ V)
251		eqidd 2739	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
252	247, 248, 250, 251	clim2 14951	. 2 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
253	118, 119	syl 17	. . 3 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
254		seqex 13462	. . . 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 15116	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
260	120, 253, 255, 259	clim2 14951	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(♯‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
261	246, 252, 260	3bitr4d 314	1 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 846 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ∃wrex 3054 Vcvv 3398 ∖ cdif 3840 ∩ cin 3842 ⊆ wss 3843 class class class wbr 5030 ^◡ccnv 5524 ran crn 5526 ↾ cres 5527 “ cima 5528 Fun wfun 6333 Fn wfn 6334 ⟶wf 6335 –1-1→wf1 6336 –1-1-onto→wf1o 6338 ‘cfv 6339 Isom wiso 6340 (class class class)co 7170 ≈ cen 8552 ≼ cdom 8553 Fincfn 8555 ℂcc 10613 ℝcr 10614 0cc0 10615 1c1 10616 + caddc 10618 ℝ^*cxr 10752 < clt 10753 ≤ cle 10754 − cmin 10948 ℕcn 11716 ℕ₀cn0 11976 ℤcz 12062 ℤ_≥cuz 12324 ℝ⁺crp 12472 ...cfz 12981 seqcseq 13460 ♯chash 13782 abscabs 14683 ⇝ cli 14931

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-inf2 9177 ax-cnex 10671 ax-resscn 10672 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-addrcl 10676 ax-mulcl 10677 ax-mulrcl 10678 ax-mulcom 10679 ax-addass 10680 ax-mulass 10681 ax-distr 10682 ax-i2m1 10683 ax-1ne0 10684 ax-1rid 10685 ax-rnegex 10686 ax-rrecex 10687 ax-cnre 10688 ax-pre-lttri 10689 ax-pre-lttrn 10690 ax-pre-ltadd 10691 ax-pre-mulgt0 10692 ax-pre-sup 10693

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7127 df-ov 7173 df-oprab 7174 df-mpo 7175 df-om 7600 df-1st 7714 df-2nd 7715 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-1o 8131 df-oadd 8135 df-er 8320 df-en 8556 df-dom 8557 df-sdom 8558 df-fin 8559 df-sup 8979 df-card 9441 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-sub 10950 df-neg 10951 df-nn 11717 df-n0 11977 df-xnn0 12049 df-z 12063 df-uz 12325 df-fz 12982 df-seq 13461 df-hash 13783 df-clim 14935

This theorem is referenced by: isercoll2 15118

W3C validator