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 14398

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 11707	. . . . . . . . . 10 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
3	1, 2	eqsstri 3635	. . . . . . . . 9 ⊢ 𝑍 ⊆ ℤ
4		isercoll.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺:ℕ⟶𝑍)
5	4	ffvelrnda 6359	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ 𝑍)
6	3, 5	sseldi 3601	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℤ)
7		nnz 11399	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
8	7	ad2antlr 763	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℤ)
9		fzfid 12772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑀...𝑚) ∈ Fin)
10		ffun 6048	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:ℕ⟶𝑍 → Fun 𝐺)
11		funimacnv 5970	. . . . . . . . . . . . . . . 16 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
12	4, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = ((𝑀...𝑚) ∩ ran 𝐺))
13		inss1 3833	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...𝑚) ∩ ran 𝐺) ⊆ (𝑀...𝑚)
14	12, 13	syl6eqss 3655	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
15	14	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚))
16		ssfi 8180	. . . . . . . . . . . . 13 ⊢ (((𝑀...𝑚) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ⊆ (𝑀...𝑚)) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
17	9, 15, 16	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin)
18		hashcl 13147	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀)
19		nn0z 11400	. . . . . . . . . . . 12 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℕ₀ → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
20	17, 18, 19	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ)
21		ssid 3624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℕ ⊆ ℕ
22		isercoll.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℤ)
23		isercoll.i	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) < (𝐺‘(𝑘 + 1)))
24	1, 22, 4, 23	isercolllem1 14395	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ℕ ⊆ ℕ) → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
25	21, 24	mpan2 707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)))
26		ffn 6045	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:ℕ⟶𝑍 → 𝐺 Fn ℕ)
27		fnresdm 6000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn ℕ → (𝐺 ↾ ℕ) = 𝐺)
28		isoeq1 6567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ↾ ℕ) = 𝐺 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
29	4, 26, 27, 28	4syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐺 ↾ ℕ) Isom < , < (ℕ, (𝐺 “ ℕ)) ↔ 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ))))
30	25, 29	mpbid 222	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
31		isof1o 6573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) → 𝐺:ℕ–1-1-onto→(𝐺 “ ℕ))
32		f1ocnv 6149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺:ℕ–1-1-onto→(𝐺 “ ℕ) → ^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ)
33		f1ofun 6139	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐺:(𝐺 “ ℕ)–1-1-onto→ℕ → Fun ^◡𝐺)
34	30, 31, 32, 33	4syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Fun ^◡𝐺)
35		df-f1 5893	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺:ℕ–1-1→𝑍 ↔ (𝐺:ℕ⟶𝑍 ∧ Fun ^◡𝐺))
36	4, 34, 35	sylanbrc 698	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ–1-1→𝑍)
37	36	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ–1-1→𝑍)
38		elfznn 12370	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ∈ ℕ)
39	38	ssriv 3607	. . . . . . . . . . . . . . 15 ⊢ (1...𝑛) ⊆ ℕ
40		ovex 6678	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑛) ∈ V
41	40	f1imaen 8018	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑛) ⊆ ℕ) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
42	37, 39, 41	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≈ (1...𝑛))
43		fzfid 12772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ∈ Fin)
44		enfii 8177	. . . . . . . . . . . . . . . 16 ⊢ (((1...𝑛) ∈ Fin ∧ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)) → (𝐺 “ (1...𝑛)) ∈ Fin)
45	43, 42, 44	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ∈ Fin)
46		hashen 13135	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((#‘(𝐺 “ (1...𝑛))) = (#‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
47	45, 43, 46	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((#‘(𝐺 “ (1...𝑛))) = (#‘(1...𝑛)) ↔ (𝐺 “ (1...𝑛)) ≈ (1...𝑛)))
48	42, 47	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(𝐺 “ (1...𝑛))) = (#‘(1...𝑛)))
49		nnnn0 11299	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
50	49	ad2antlr 763	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ∈ ℕ₀)
51		hashfz1 13134	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ₀ → (#‘(1...𝑛)) = 𝑛)
52	50, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(1...𝑛)) = 𝑛)
53	48, 52	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(𝐺 “ (1...𝑛))) = 𝑛)
54	38	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℕ)
55		zssre 11384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℤ ⊆ ℝ
56	3, 55	sstri 3612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑍 ⊆ ℝ
57	4	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺:ℕ⟶𝑍)
58		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 𝑦 ∈ ℕ) → (𝐺‘𝑦) ∈ 𝑍)
59	57, 38, 58	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ 𝑍)
60	56, 59	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ ℝ)
61	5	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ 𝑍)
62	56, 61	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ∈ ℝ)
63		eluzelz 11697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → 𝑚 ∈ ℤ)
64	63	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℤ)
65	64	zred 11482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑚 ∈ ℝ)
66		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑛) → 𝑦 ≤ 𝑛)
67	66	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ≤ 𝑛)
68	30	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
69		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℕ)
70		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ ℕ)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
71	68, 69, 54, 70	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑛 < 𝑦 ↔ (𝐺‘𝑛) < (𝐺‘𝑦)))
72	71	notbid 308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (¬ 𝑛 < 𝑦 ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
73	54	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ ℝ)
74	69	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑛 ∈ ℝ)
75	73, 74	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ ¬ 𝑛 < 𝑦))
76	60, 62	lenltd 10183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ≤ (𝐺‘𝑛) ↔ ¬ (𝐺‘𝑛) < (𝐺‘𝑦)))
77	72, 75, 76	3bitr4d 300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ≤ 𝑛 ↔ (𝐺‘𝑦) ≤ (𝐺‘𝑛)))
78	67, 77	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ (𝐺‘𝑛))
79		eluzle 11700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
80	79	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑛) ≤ 𝑚)
81	60, 62, 65, 78, 80	letrd 10194	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ≤ 𝑚)
82	59, 1	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (ℤ_≥‘𝑀))
83		elfz5 12334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑦) ∈ (ℤ_≥‘𝑀) ∧ 𝑚 ∈ ℤ) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
84	82, 64, 83	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → ((𝐺‘𝑦) ∈ (𝑀...𝑚) ↔ (𝐺‘𝑦) ≤ 𝑚))
85	81, 84	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝐺‘𝑦) ∈ (𝑀...𝑚))
86	57, 26	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝐺 Fn ℕ)
87	86	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝐺 Fn ℕ)
88		elpreima 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → (𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)) ↔ (𝑦 ∈ ℕ ∧ (𝐺‘𝑦) ∈ (𝑀...𝑚))))
90	54, 85, 89	mpbir2and 957	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) ∧ 𝑦 ∈ (1...𝑛)) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚)))
91	90	ex 450	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝑦 ∈ (1...𝑛) → 𝑦 ∈ (^◡𝐺 “ (𝑀...𝑚))))
92	91	ssrdv 3609	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)))
93		imass2 5501	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑛) ⊆ (^◡𝐺 “ (𝑀...𝑚)) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
94	92, 93	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
95		ssdomg 8001	. . . . . . . . . . . . . 14 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin → ((𝐺 “ (1...𝑛)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
96	17, 94, 95	sylc 65	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))
97		hashdom 13168	. . . . . . . . . . . . . 14 ⊢ (((𝐺 “ (1...𝑛)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) ∈ Fin) → ((#‘(𝐺 “ (1...𝑛))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
98	45, 17, 97	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → ((#‘(𝐺 “ (1...𝑛))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ↔ (𝐺 “ (1...𝑛)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
99	96, 98	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(𝐺 “ (1...𝑛))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
100	53, 99	eqbrtrrd 4677	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → 𝑛 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))))
101		eluz2 11693	. . . . . . . . . . 11 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) ↔ (𝑛 ∈ ℤ ∧ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ ℤ ∧ 𝑛 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
102	8, 20, 100, 101	syl3anbrc 1246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛))
103		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
104	103	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ↔ (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ))
105	103	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((seq1( + , 𝐻)‘𝑘) − 𝐴) = ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴))
106	105	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)))
107	106	breq1d 4663	. . . . . . . . . . . 12 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → ((abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
108	104, 107	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑘 = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) → (((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
109	108	rspcv 3305	. . . . . . . . . 10 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) ∈ (ℤ_≥‘𝑛) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
110	102, 109	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
111	110	ralrimdva 2969	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
112		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑗 = (𝐺‘𝑛) → (ℤ_≥‘𝑗) = (ℤ_≥‘(𝐺‘𝑛)))
113	112	raleqdv 3144	. . . . . . . . 9 ⊢ (𝑗 = (𝐺‘𝑛) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
114	113	rspcev 3309	. . . . . . . 8 ⊢ (((𝐺‘𝑛) ∈ ℤ ∧ ∀𝑚 ∈ (ℤ_≥‘(𝐺‘𝑛))((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))
115	6, 111, 114	syl6an 568	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
116	115	rexlimdva 3031	. . . . . 6 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
117		1nn 11031	. . . . . . . . 9 ⊢ 1 ∈ ℕ
118		ffvelrn 6357	. . . . . . . . 9 ⊢ ((𝐺:ℕ⟶𝑍 ∧ 1 ∈ ℕ) → (𝐺‘1) ∈ 𝑍)
119	4, 117, 118	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘1) ∈ 𝑍)
120	119, 1	syl6eleq 2711	. . . . . . 7 ⊢ (𝜑 → (𝐺‘1) ∈ (ℤ_≥‘𝑀))
121		eluzelz 11697	. . . . . . 7 ⊢ ((𝐺‘1) ∈ (ℤ_≥‘𝑀) → (𝐺‘1) ∈ ℤ)
122		eqid 2622	. . . . . . . 8 ⊢ (ℤ_≥‘(𝐺‘1)) = (ℤ_≥‘(𝐺‘1))
123	122	rexuz3 14088	. . . . . . 7 ⊢ ((𝐺‘1) ∈ ℤ → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
124	120, 121, 123	3syl 18	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ ℤ ∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
125	116, 124	sylibrd 249	. . . . 5 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) → ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
126		fzfid 12772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝑀...𝑗) ∈ Fin)
127		funimacnv 5970	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
128	4, 10, 127	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) = ((𝑀...𝑗) ∩ ran 𝐺))
129		inss1 3833	. . . . . . . . . . 11 ⊢ ((𝑀...𝑗) ∩ ran 𝐺) ⊆ (𝑀...𝑗)
130	128, 129	syl6eqss 3655	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
131	130	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗))
132		ssfi 8180	. . . . . . . . 9 ⊢ (((𝑀...𝑗) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ⊆ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
133	126, 131, 132	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
134		hashcl 13147	. . . . . . . 8 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀)
135		nn0p1nn 11332	. . . . . . . 8 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
136	133, 134, 135	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ)
137		eluzle 11700	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
138	137	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘)
139	133	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin)
140		nn0z 11400	. . . . . . . . . . . . . . . 16 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
141	139, 134, 140	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ)
142		eluzelz 11697	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)) → 𝑘 ∈ ℤ)
143	142	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℤ)
144		zltp1le 11427	. . . . . . . . . . . . . . 15 ⊢ (((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
145	141, 143, 144	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ≤ 𝑘))
146	138, 145	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘)
147		nn0re 11301	. . . . . . . . . . . . . . . 16 ⊢ ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℕ₀ → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
148	133, 134, 147	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
149	148	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ∈ ℝ)
150		eluznn 11758	. . . . . . . . . . . . . . . 16 ⊢ ((((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
151	136, 150	sylan 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℕ)
152	151	nnred 11035	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑘 ∈ ℝ)
153	149, 152	ltnled 10184	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) < 𝑘 ↔ ¬ 𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
154	146, 153	mpbid 222	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
155		fzss2 12381	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗))
156		imass2 5501	. . . . . . . . . . . . . 14 ⊢ ((𝑀...(𝐺‘𝑘)) ⊆ (𝑀...𝑗) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)))
157		imass2 5501	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ⊆ (^◡𝐺 “ (𝑀...𝑗)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
158	155, 156, 157	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))
159		ssdomg 8001	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
160	139, 159	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
161	4	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ⟶𝑍)
162	161	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ 𝑍)
163	162, 1	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑥) ∈ (ℤ_≥‘𝑀))
164	161, 151	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ 𝑍)
165	3, 164	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ ℤ)
166	165	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺‘𝑘) ∈ ℤ)
167		elfz5 12334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑥) ∈ (ℤ_≥‘𝑀) ∧ (𝐺‘𝑘) ∈ ℤ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
168	163, 166, 167	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
169	30	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)))
170		nnssre 11024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℕ ⊆ ℝ
171		ressxr 10083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ⊆ ℝ^*
172	170, 171	sstri 3612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ ⊆ ℝ^*
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ℕ ⊆ ℝ^*)
174		imassrn 5477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 “ ℕ) ⊆ ran 𝐺
175	161	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝐺:ℕ⟶𝑍)
176		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺:ℕ⟶𝑍 → ran 𝐺 ⊆ 𝑍)
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ 𝑍)
178	177, 56	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ran 𝐺 ⊆ ℝ)
179	174, 178	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ)
180	179, 171	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝐺 “ ℕ) ⊆ ℝ^*)
181		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑥 ∈ ℕ)
182	151	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → 𝑘 ∈ ℕ)
183		leisorel 13244	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 Isom < , < (ℕ, (𝐺 “ ℕ)) ∧ (ℕ ⊆ ℝ^* ∧ (𝐺 “ ℕ) ⊆ ℝ^*) ∧ (𝑥 ∈ ℕ ∧ 𝑘 ∈ ℕ)) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
184	169, 173, 180, 181, 182, 183	syl122anc 1335	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → (𝑥 ≤ 𝑘 ↔ (𝐺‘𝑥) ≤ (𝐺‘𝑘)))
185	168, 184	bitr4d 271	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) ∧ 𝑥 ∈ ℕ) → ((𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)) ↔ 𝑥 ≤ 𝑘))
186	185	pm5.32da 673	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
187		elpreima 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐺 Fn ℕ → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
188	161, 26, 187	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ (𝑥 ∈ ℕ ∧ (𝐺‘𝑥) ∈ (𝑀...(𝐺‘𝑘)))))
189		fznn 12408	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℤ → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
190	143, 189	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (1...𝑘) ↔ (𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝑘)))
191	186, 188, 190	3bitr4d 300	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑥 ∈ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) ↔ 𝑥 ∈ (1...𝑘)))
192	191	eqrdv 2620	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (^◡𝐺 “ (𝑀...(𝐺‘𝑘))) = (1...𝑘))
193	192	imaeq2d 5466	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) = (𝐺 “ (1...𝑘)))
194	193	sseq1d 3632	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ↔ (𝐺 “ (1...𝑘)) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
195	36	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝐺:ℕ–1-1→𝑍)
196		elfznn 12370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℕ)
197	196	ssriv 3607	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑘) ⊆ ℕ
198		ovex 6678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑘) ∈ V
199	198	f1imaen 8018	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺:ℕ–1-1→𝑍 ∧ (1...𝑘) ⊆ ℕ) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
200	195, 197, 199	sylancl 694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ≈ (1...𝑘))
201		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (1...𝑘) ∈ Fin)
202		enfii 8177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑘) ∈ Fin ∧ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)) → (𝐺 “ (1...𝑘)) ∈ Fin)
203	201, 200, 202	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺 “ (1...𝑘)) ∈ Fin)
204		hashen 13135	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (1...𝑘) ∈ Fin) → ((#‘(𝐺 “ (1...𝑘))) = (#‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
205	203, 201, 204	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (1...𝑘))) = (#‘(1...𝑘)) ↔ (𝐺 “ (1...𝑘)) ≈ (1...𝑘)))
206	200, 205	mpbird 247	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (1...𝑘))) = (#‘(1...𝑘)))
207		nnnn0 11299	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
208		hashfz1 13134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → (#‘(1...𝑘)) = 𝑘)
209	151, 207, 208	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(1...𝑘)) = 𝑘)
210	206, 209	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (1...𝑘))) = 𝑘)
211	210	breq1d 4663	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (1...𝑘))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ 𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
212		hashdom 13168	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 “ (1...𝑘)) ∈ Fin ∧ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) ∈ Fin) → ((#‘(𝐺 “ (1...𝑘))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
213	203, 139, 212	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((#‘(𝐺 “ (1...𝑘))) ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
214	211, 213	bitr3d 270	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) ↔ (𝐺 “ (1...𝑘)) ≼ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))))
215	160, 194, 214	3imtr4d 283	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))) ⊆ (𝐺 “ (^◡𝐺 “ (𝑀...𝑗))) → 𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
216	158, 215	syl5 34	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → 𝑘 ≤ (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗))))))
217	154, 216	mtod 189	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)))
218		eluzelz 11697	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ_≥‘(𝐺‘1)) → 𝑗 ∈ ℤ)
219	218	ad2antlr 763	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → 𝑗 ∈ ℤ)
220		uztric 11709	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
221	165, 219, 220	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) ∨ (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
222	221	ord 392	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (¬ 𝑗 ∈ (ℤ_≥‘(𝐺‘𝑘)) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗)))
223	217, 222	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (𝐺‘𝑘) ∈ (ℤ_≥‘𝑗))
224		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = (𝐺‘𝑘) → (𝑀...𝑚) = (𝑀...(𝐺‘𝑘)))
225	224	imaeq2d 5466	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (𝐺‘𝑘) → (^◡𝐺 “ (𝑀...𝑚)) = (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))
226	225	imaeq2d 5466	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (𝐺‘𝑘) → (𝐺 “ (^◡𝐺 “ (𝑀...𝑚))) = (𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))
227	226	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚)))) = (#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))))
228	227	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) = (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))))
229	228	eleq1d 2686	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ))
230	228	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝐺‘𝑘) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴) = ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴))
231	230	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝐺‘𝑘) → (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)))
232	231	breq1d 4663	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝐺‘𝑘) → ((abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥))
233	229, 232	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑘) → (((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
234	233	rspcv 3305	. . . . . . . . . 10 ⊢ ((𝐺‘𝑘) ∈ (ℤ_≥‘𝑗) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
235	223, 234	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥)))
236	193	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = (#‘(𝐺 “ (1...𝑘))))
237	236, 210	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘))))) = 𝑘)
238	237	fveq2d 6195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) = (seq1( + , 𝐻)‘𝑘))
239	238	eleq1d 2686	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ↔ (seq1( + , 𝐻)‘𝑘) ∈ ℂ))
240	238	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴) = ((seq1( + , 𝐻)‘𝑘) − 𝐴))
241	240	fveq2d 6195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) = (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)))
242	241	breq1d 4663	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → ((abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥 ↔ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
243	239, 242	anbi12d 747	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...(𝐺‘𝑘)))))) − 𝐴)) < 𝑥) ↔ ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
244	235, 243	sylibd 229	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) ∧ 𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
245	244	ralrimdva 2969	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∀𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
246		fveq2 6191	. . . . . . . . 9 ⊢ (𝑛 = ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (ℤ_≥‘𝑛) = (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1)))
247	246	raleqdv 3144	. . . . . . . 8 ⊢ (𝑛 = ((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) → (∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
248	247	rspcev 3309	. . . . . . 7 ⊢ ((((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1) ∈ ℕ ∧ ∀𝑘 ∈ (ℤ_≥‘((#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑗)))) + 1))((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))
249	136, 245, 248	syl6an 568	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘(𝐺‘1))) → (∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
250	249	rexlimdva 3031	. . . . 5 ⊢ (𝜑 → (∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)))
251	125, 250	impbid 202	. . . 4 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
252	251	ralbidv 2986	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥)))
253	252	anbi2d 740	. 2 ⊢ (𝜑 → ((𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥)) ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
254		nnuz 11723	. . 3 ⊢ ℕ = (ℤ_≥‘1)
255		1zzd 11408	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
256		seqex 12803	. . . 4 ⊢ seq1( + , 𝐻) ∈ V
257	256	a1i 11	. . 3 ⊢ (𝜑 → seq1( + , 𝐻) ∈ V)
258		eqidd 2623	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐻)‘𝑘) = (seq1( + , 𝐻)‘𝑘))
259	254, 255, 257, 258	clim2 14235	. 2 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ_≥‘𝑛)((seq1( + , 𝐻)‘𝑘) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘𝑘) − 𝐴)) < 𝑥))))
260	120, 121	syl 17	. . 3 ⊢ (𝜑 → (𝐺‘1) ∈ ℤ)
261		seqex 12803	. . . 4 ⊢ seq𝑀( + , 𝐹) ∈ V
262	261	a1i 11	. . 3 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V)
263		isercoll.0	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑍 ∖ ran 𝐺)) → (𝐹‘𝑛) = 0)
264		isercoll.f	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ ℂ)
265		isercoll.h	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (𝐹‘(𝐺‘𝑘)))
266	1, 22, 4, 23, 263, 264, 265	isercolllem3 14397	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ_≥‘(𝐺‘1))) → (seq𝑀( + , 𝐹)‘𝑚) = (seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))))
267	122, 260, 262, 266	clim2 14235	. 2 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ⇝ 𝐴 ↔ (𝐴 ∈ ℂ ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑗 ∈ (ℤ_≥‘(𝐺‘1))∀𝑚 ∈ (ℤ_≥‘𝑗)((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) ∈ ℂ ∧ (abs‘((seq1( + , 𝐻)‘(#‘(𝐺 “ (^◡𝐺 “ (𝑀...𝑚))))) − 𝐴)) < 𝑥))))
268	253, 259, 267	3bitr4d 300	1 ⊢ (𝜑 → (seq1( + , 𝐻) ⇝ 𝐴 ↔ seq𝑀( + , 𝐹) ⇝ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∖ cdif 3571 ∩ cin 3573 ⊆ wss 3574 class class class wbr 4653 ^◡ccnv 5113 ran crn 5115 ↾ cres 5116 “ cima 5117 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –1-1→wf1 5885 –1-1-onto→wf1o 5887 ‘cfv 5888 Isom wiso 5889 (class class class)co 6650 ≈ cen 7952 ≼ cdom 7953 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 ...cfz 12326 seqcseq 12801 #chash 13117 abscabs 13974 ⇝ cli 14215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-seq 12802 df-hash 13118 df-clim 14219

This theorem is referenced by: isercoll2 14399

W3C validator