isercoll

Description: Rearrange an infinite series by spacing out the terms using an order isomorphism. (Contributed by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypotheses	isercoll.z	$⊢ Z = ℤ_{\geq M}$
	isercoll.m	$⊢ φ \to M \in ℤ$
	isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
	isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
	isercoll.0	$⊢ (φ \land n \in (Z ∖ ran G)) \to F (n) = 0$
	isercoll.f	$⊢ (φ \land n \in Z) \to F (n) \in ℂ$
	isercoll.h	$⊢ (φ \land k \in ℕ) \to H (k) = F (G (k))$
Assertion	isercoll	$⊢ φ \to (seq 1 (+ H) ⇝ A \leftrightarrow seq M (+ F) ⇝ A)$

Proof

Step	Hyp	Ref	Expression
1		isercoll.z	$⊢ Z = ℤ_{\geq M}$
2		isercoll.m	$⊢ φ \to M \in ℤ$
3		isercoll.g	$⊢ φ \to G : ℕ ⟶ Z$
4		isercoll.i	$⊢ (φ \land k \in ℕ) \to G (k) < G (k + 1)$
5		isercoll.0	$⊢ (φ \land n \in (Z ∖ ran G)) \to F (n) = 0$
6		isercoll.f	$⊢ (φ \land n \in Z) \to F (n) \in ℂ$
7		isercoll.h	$⊢ (φ \land k \in ℕ) \to H (k) = F (G (k))$
8		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
9	1 8	eqsstri	$⊢ Z \subseteq ℤ$
10	3	ffvelrnda	$⊢ (φ \land n \in ℕ) \to G (n) \in Z$
11	9 10	sseldi	$⊢ (φ \land n \in ℕ) \to G (n) \in ℤ$
12		nnz	$⊢ n \in ℕ \to n \in ℤ$
13	12	ad2antlr	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to n \in ℤ$
14		fzfid	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (M \dots m) \in Fin$
15		ffun	$⊢ G : ℕ ⟶ Z \to Fun G$
16		funimacnv	$⊢ Fun G \to G [G^{-1} [(M \dots m)]] = (M \dots m) \cap ran G$
17	3 15 16	3syl	$⊢ φ \to G [G^{-1} [(M \dots m)]] = (M \dots m) \cap ran G$
18		inss1	$⊢ (M \dots m) \cap ran G \subseteq (M \dots m)$
19	17 18	eqsstrdi	$⊢ φ \to G [G^{-1} [(M \dots m)]] \subseteq (M \dots m)$
20	19	ad2antrr	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [G^{-1} [(M \dots m)]] \subseteq (M \dots m)$
21	14 20	ssfid	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [G^{-1} [(M \dots m)]] \in Fin$
22		hashcl	$⊢ G [G^{-1} [(M \dots m)]] \in Fin \to \|G [G^{-1} [(M \dots m)]]\| \in ℕ_{0}$
23		nn0z	$⊢ \|G [G^{-1} [(M \dots m)]]\| \in ℕ_{0} \to \|G [G^{-1} [(M \dots m)]]\| \in ℤ$
24	21 22 23	3syl	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|G [G^{-1} [(M \dots m)]]\| \in ℤ$
25		ssid	$⊢ ℕ \subseteq ℕ$
26	1 2 3 4	isercolllem1	$⊢ (φ \land ℕ \subseteq ℕ) \to ({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ])$
27	25 26	mpan2	$⊢ φ \to ({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ])$
28		ffn	$⊢ G : ℕ ⟶ Z \to G Fn ℕ$
29		fnresdm	$⊢ G Fn ℕ \to {G ↾}_{ℕ} = G$
30		isoeq1	$⊢ {G ↾}_{ℕ} = G \to (({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ]) \leftrightarrow G {Isom}_{<, <} (ℕ, G [ℕ]))$
31	3 28 29 30	4syl	$⊢ φ \to (({G ↾}_{ℕ}) {Isom}_{<, <} (ℕ, G [ℕ]) \leftrightarrow G {Isom}_{<, <} (ℕ, G [ℕ]))$
32	27 31	mpbid	$⊢ φ \to G {Isom}_{<, <} (ℕ, G [ℕ])$
33		isof1o	$⊢ G {Isom}_{<, <} (ℕ, G [ℕ]) \to G : ℕ \underset{1-1 onto}{⟶} G [ℕ]$
34		f1ocnv	$⊢ G : ℕ \underset{1-1 onto}{⟶} G [ℕ] \to G^{-1} : G [ℕ] \underset{1-1 onto}{⟶} ℕ$
35		f1ofun	$⊢ G^{-1} : G [ℕ] \underset{1-1 onto}{⟶} ℕ \to Fun G^{-1}$
36	32 33 34 35	4syl	$⊢ φ \to Fun G^{-1}$
37		df-f1	$⊢ G : ℕ \underset{1-1}{⟶} Z \leftrightarrow (G : ℕ ⟶ Z \land Fun G^{-1})$
38	3 36 37	sylanbrc	$⊢ φ \to G : ℕ \underset{1-1}{⟶} Z$
39	38	ad2antrr	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G : ℕ \underset{1-1}{⟶} Z$
40		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
41		ovex	$⊢ (1 \dots n) \in V$
42	41	f1imaen	$⊢ (G : ℕ \underset{1-1}{⟶} Z \land (1 \dots n) \subseteq ℕ) \to G [(1 \dots n)] \approx (1 \dots n)$
43	39 40 42	sylancl	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [(1 \dots n)] \approx (1 \dots n)$
44		fzfid	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (1 \dots n) \in Fin$
45		enfii	$⊢ ((1 \dots n) \in Fin \land G [(1 \dots n)] \approx (1 \dots n)) \to G [(1 \dots n)] \in Fin$
46	44 43 45	syl2anc	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [(1 \dots n)] \in Fin$
47		hashen	$⊢ (G [(1 \dots n)] \in Fin \land (1 \dots n) \in Fin) \to (\|G [(1 \dots n)]\| = \|(1 \dots n)\| \leftrightarrow G [(1 \dots n)] \approx (1 \dots n))$
48	46 44 47	syl2anc	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (\|G [(1 \dots n)]\| = \|(1 \dots n)\| \leftrightarrow G [(1 \dots n)] \approx (1 \dots n))$
49	43 48	mpbird	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|G [(1 \dots n)]\| = \|(1 \dots n)\|$
50		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
51	50	ad2antlr	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to n \in ℕ_{0}$
52		hashfz1	$⊢ n \in ℕ_{0} \to \|(1 \dots n)\| = n$
53	51 52	syl	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|(1 \dots n)\| = n$
54	49 53	eqtrd	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|G [(1 \dots n)]\| = n$
55		elfznn	$⊢ y \in (1 \dots n) \to y \in ℕ$
56	55	adantl	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to y \in ℕ$
57		zssre	$⊢ ℤ \subseteq ℝ$
58	9 57	sstri	$⊢ Z \subseteq ℝ$
59	3	ad2antrr	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G : ℕ ⟶ Z$
60		ffvelrn	$⊢ (G : ℕ ⟶ Z \land y \in ℕ) \to G (y) \in Z$
61	59 55 60	syl2an	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \in Z$
62	58 61	sseldi	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \in ℝ$
63	10	ad2antrr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (n) \in Z$
64	58 63	sseldi	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (n) \in ℝ$
65		eluzelz	$⊢ m \in ℤ_{\geq G (n)} \to m \in ℤ$
66	65	ad2antlr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to m \in ℤ$
67	66	zred	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to m \in ℝ$
68		elfzle2	$⊢ y \in (1 \dots n) \to y \leq n$
69	68	adantl	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to y \leq n$
70	32	ad3antrrr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G {Isom}_{<, <} (ℕ, G [ℕ])$
71		simpllr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to n \in ℕ$
72		isorel	$⊢ (G {Isom}_{<, <} (ℕ, G [ℕ]) \land (n \in ℕ \land y \in ℕ)) \to (n < y \leftrightarrow G (n) < G (y))$
73	70 71 56 72	syl12anc	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (n < y \leftrightarrow G (n) < G (y))$
74	73	notbid	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (\neg n < y \leftrightarrow \neg G (n) < G (y))$
75	56	nnred	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to y \in ℝ$
76	71	nnred	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to n \in ℝ$
77	75 76	lenltd	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (y \leq n \leftrightarrow \neg n < y)$
78	62 64	lenltd	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (G (y) \leq G (n) \leftrightarrow \neg G (n) < G (y))$
79	74 77 78	3bitr4d	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (y \leq n \leftrightarrow G (y) \leq G (n))$
80	69 79	mpbid	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \leq G (n)$
81		eluzle	$⊢ m \in ℤ_{\geq G (n)} \to G (n) \leq m$
82	81	ad2antlr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (n) \leq m$
83	62 64 67 80 82	letrd	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \leq m$
84	61 1	eleqtrdi	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \in ℤ_{\geq M}$
85		elfz5	$⊢ (G (y) \in ℤ_{\geq M} \land m \in ℤ) \to (G (y) \in (M \dots m) \leftrightarrow G (y) \leq m)$
86	84 66 85	syl2anc	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (G (y) \in (M \dots m) \leftrightarrow G (y) \leq m)$
87	83 86	mpbird	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G (y) \in (M \dots m)$
88	59	ffnd	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G Fn ℕ$
89	88	adantr	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to G Fn ℕ$
90		elpreima	$⊢ G Fn ℕ \to (y \in G^{-1} [(M \dots m)] \leftrightarrow (y \in ℕ \land G (y) \in (M \dots m)))$
91	89 90	syl	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to (y \in G^{-1} [(M \dots m)] \leftrightarrow (y \in ℕ \land G (y) \in (M \dots m)))$
92	56 87 91	mpbir2and	$⊢ (((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \land y \in (1 \dots n)) \to y \in G^{-1} [(M \dots m)]$
93	92	ex	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (y \in (1 \dots n) \to y \in G^{-1} [(M \dots m)])$
94	93	ssrdv	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (1 \dots n) \subseteq G^{-1} [(M \dots m)]$
95		imass2	$⊢ (1 \dots n) \subseteq G^{-1} [(M \dots m)] \to G [(1 \dots n)] \subseteq G [G^{-1} [(M \dots m)]]$
96	94 95	syl	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [(1 \dots n)] \subseteq G [G^{-1} [(M \dots m)]]$
97		ssdomg	$⊢ G [G^{-1} [(M \dots m)]] \in Fin \to (G [(1 \dots n)] \subseteq G [G^{-1} [(M \dots m)]] \to G [(1 \dots n)] ≼ G [G^{-1} [(M \dots m)]])$
98	21 96 97	sylc	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to G [(1 \dots n)] ≼ G [G^{-1} [(M \dots m)]]$
99		hashdom	$⊢ (G [(1 \dots n)] \in Fin \land G [G^{-1} [(M \dots m)]] \in Fin) \to (\|G [(1 \dots n)]\| \leq \|G [G^{-1} [(M \dots m)]]\| \leftrightarrow G [(1 \dots n)] ≼ G [G^{-1} [(M \dots m)]])$
100	46 21 99	syl2anc	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (\|G [(1 \dots n)]\| \leq \|G [G^{-1} [(M \dots m)]]\| \leftrightarrow G [(1 \dots n)] ≼ G [G^{-1} [(M \dots m)]])$
101	98 100	mpbird	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|G [(1 \dots n)]\| \leq \|G [G^{-1} [(M \dots m)]]\|$
102	54 101	eqbrtrrd	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to n \leq \|G [G^{-1} [(M \dots m)]]\|$
103		eluz2	$⊢ \|G [G^{-1} [(M \dots m)]]\| \in ℤ_{\geq n} \leftrightarrow (n \in ℤ \land \|G [G^{-1} [(M \dots m)]]\| \in ℤ \land n \leq \|G [G^{-1} [(M \dots m)]]\|)$
104	13 24 102 103	syl3anbrc	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to \|G [G^{-1} [(M \dots m)]]\| \in ℤ_{\geq n}$
105		fveq2	$⊢ k = \|G [G^{-1} [(M \dots m)]]\| \to seq 1 (+ H) (k) = seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|)$
106	105	eleq1d	$⊢ k = \|G [G^{-1} [(M \dots m)]]\| \to (seq 1 (+ H) (k) \in ℂ \leftrightarrow seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ)$
107	105	fvoveq1d	$⊢ k = \|G [G^{-1} [(M \dots m)]]\| \to \|seq 1 (+ H) (k) - A\| = \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\|$
108	107	breq1d	$⊢ k = \|G [G^{-1} [(M \dots m)]]\| \to (\|seq 1 (+ H) (k) - A\| < x \leftrightarrow \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x)$
109	106 108	anbi12d	$⊢ k = \|G [G^{-1} [(M \dots m)]]\| \to ((seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \leftrightarrow (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
110	109	rspcv	$⊢ \|G [G^{-1} [(M \dots m)]]\| \in ℤ_{\geq n} \to (\forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
111	104 110	syl	$⊢ ((φ \land n \in ℕ) \land m \in ℤ_{\geq G (n)}) \to (\forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
112	111	ralrimdva	$⊢ (φ \land n \in ℕ) \to (\forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to \forall m \in ℤ_{\geq G (n)} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
113		fveq2	$⊢ j = G (n) \to ℤ_{\geq j} = ℤ_{\geq G (n)}$
114	113	raleqdv	$⊢ j = G (n) \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \leftrightarrow \forall m \in ℤ_{\geq G (n)} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
115	114	rspcev	$⊢ (G (n) \in ℤ \land \forall m \in ℤ_{\geq G (n)} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x)) \to \exists j \in ℤ \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x)$
116	11 112 115	syl6an	$⊢ (φ \land n \in ℕ) \to (\forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to \exists j \in ℤ \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
117	116	rexlimdva	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to \exists j \in ℤ \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
118		1nn	$⊢ 1 \in ℕ$
119		ffvelrn	$⊢ (G : ℕ ⟶ Z \land 1 \in ℕ) \to G (1) \in Z$
120	3 118 119	sylancl	$⊢ φ \to G (1) \in Z$
121	120 1	eleqtrdi	$⊢ φ \to G (1) \in ℤ_{\geq M}$
122		eluzelz	$⊢ G (1) \in ℤ_{\geq M} \to G (1) \in ℤ$
123		eqid	$⊢ ℤ_{\geq G (1)} = ℤ_{\geq G (1)}$
124	123	rexuz3	$⊢ G (1) \in ℤ \to (\exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \leftrightarrow \exists j \in ℤ \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
125	121 122 124	3syl	$⊢ φ \to (\exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \leftrightarrow \exists j \in ℤ \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
126	117 125	sylibrd	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \to \exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
127		fzfid	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to (M \dots j) \in Fin$
128		funimacnv	$⊢ Fun G \to G [G^{-1} [(M \dots j)]] = (M \dots j) \cap ran G$
129	3 15 128	3syl	$⊢ φ \to G [G^{-1} [(M \dots j)]] = (M \dots j) \cap ran G$
130		inss1	$⊢ (M \dots j) \cap ran G \subseteq (M \dots j)$
131	129 130	eqsstrdi	$⊢ φ \to G [G^{-1} [(M \dots j)]] \subseteq (M \dots j)$
132	131	adantr	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots j)]] \subseteq (M \dots j)$
133	127 132	ssfid	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to G [G^{-1} [(M \dots j)]] \in Fin$
134		hashcl	$⊢ G [G^{-1} [(M \dots j)]] \in Fin \to \|G [G^{-1} [(M \dots j)]]\| \in ℕ_{0}$
135		nn0p1nn	$⊢ \|G [G^{-1} [(M \dots j)]]\| \in ℕ_{0} \to \|G [G^{-1} [(M \dots j)]]\| + 1 \in ℕ$
136	133 134 135	3syl	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to \|G [G^{-1} [(M \dots j)]]\| + 1 \in ℕ$
137		eluzle	$⊢ k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)} \to \|G [G^{-1} [(M \dots j)]]\| + 1 \leq k$
138	137	adantl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots j)]]\| + 1 \leq k$
139	133	adantr	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G [G^{-1} [(M \dots j)]] \in Fin$
140		nn0z	$⊢ \|G [G^{-1} [(M \dots j)]]\| \in ℕ_{0} \to \|G [G^{-1} [(M \dots j)]]\| \in ℤ$
141	139 134 140	3syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots j)]]\| \in ℤ$
142		eluzelz	$⊢ k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)} \to k \in ℤ$
143	142	adantl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to k \in ℤ$
144		zltp1le	$⊢ (\|G [G^{-1} [(M \dots j)]]\| \in ℤ \land k \in ℤ) \to (\|G [G^{-1} [(M \dots j)]]\| < k \leftrightarrow \|G [G^{-1} [(M \dots j)]]\| + 1 \leq k)$
145	141 143 144	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|G [G^{-1} [(M \dots j)]]\| < k \leftrightarrow \|G [G^{-1} [(M \dots j)]]\| + 1 \leq k)$
146	138 145	mpbird	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots j)]]\| < k$
147		nn0re	$⊢ \|G [G^{-1} [(M \dots j)]]\| \in ℕ_{0} \to \|G [G^{-1} [(M \dots j)]]\| \in ℝ$
148	133 134 147	3syl	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to \|G [G^{-1} [(M \dots j)]]\| \in ℝ$
149	148	adantr	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots j)]]\| \in ℝ$
150		eluznn	$⊢ (\|G [G^{-1} [(M \dots j)]]\| + 1 \in ℕ \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to k \in ℕ$
151	136 150	sylan	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to k \in ℕ$
152	151	nnred	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to k \in ℝ$
153	149 152	ltnled	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|G [G^{-1} [(M \dots j)]]\| < k \leftrightarrow \neg k \leq \|G [G^{-1} [(M \dots j)]]\|)$
154	146 153	mpbid	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \neg k \leq \|G [G^{-1} [(M \dots j)]]\|$
155		fzss2	$⊢ j \in ℤ_{\geq G (k)} \to (M \dots G (k)) \subseteq (M \dots j)$
156		imass2	$⊢ (M \dots G (k)) \subseteq (M \dots j) \to G^{-1} [(M \dots G (k))] \subseteq G^{-1} [(M \dots j)]$
157		imass2	$⊢ G^{-1} [(M \dots G (k))] \subseteq G^{-1} [(M \dots j)] \to G [G^{-1} [(M \dots G (k))]] \subseteq G [G^{-1} [(M \dots j)]]$
158	155 156 157	3syl	$⊢ j \in ℤ_{\geq G (k)} \to G [G^{-1} [(M \dots G (k))]] \subseteq G [G^{-1} [(M \dots j)]]$
159		ssdomg	$⊢ G [G^{-1} [(M \dots j)]] \in Fin \to (G [(1 \dots k)] \subseteq G [G^{-1} [(M \dots j)]] \to G [(1 \dots k)] ≼ G [G^{-1} [(M \dots j)]])$
160	139 159	syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (G [(1 \dots k)] \subseteq G [G^{-1} [(M \dots j)]] \to G [(1 \dots k)] ≼ G [G^{-1} [(M \dots j)]])$
161	3	ad2antrr	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G : ℕ ⟶ Z$
162	161	ffvelrnda	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G (x) \in Z$
163	162 1	eleqtrdi	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G (x) \in ℤ_{\geq M}$
164	161 151	ffvelrnd	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G (k) \in Z$
165	9 164	sseldi	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G (k) \in ℤ$
166	165	adantr	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G (k) \in ℤ$
167		elfz5	$⊢ (G (x) \in ℤ_{\geq M} \land G (k) \in ℤ) \to (G (x) \in (M \dots G (k)) \leftrightarrow G (x) \leq G (k))$
168	163 166 167	syl2anc	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to (G (x) \in (M \dots G (k)) \leftrightarrow G (x) \leq G (k))$
169	32	ad3antrrr	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G {Isom}_{<, <} (ℕ, G [ℕ])$
170		nnssre	$⊢ ℕ \subseteq ℝ$
171		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
172	170 171	sstri	$⊢ ℕ \subseteq ℝ^{*}$
173	172	a1i	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to ℕ \subseteq ℝ^{*}$
174		imassrn	$⊢ G [ℕ] \subseteq ran G$
175	161	adantr	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G : ℕ ⟶ Z$
176	175	frnd	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to ran G \subseteq Z$
177	176 58	sstrdi	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to ran G \subseteq ℝ$
178	174 177	sstrid	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G [ℕ] \subseteq ℝ$
179	178 171	sstrdi	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to G [ℕ] \subseteq ℝ^{*}$
180		simpr	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to x \in ℕ$
181	151	adantr	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to k \in ℕ$
182		leisorel	$⊢ (G {Isom}_{<, <} (ℕ, G [ℕ]) \land (ℕ \subseteq ℝ^{} \land G [ℕ] \subseteq ℝ^{}) \land (x \in ℕ \land k \in ℕ)) \to (x \leq k \leftrightarrow G (x) \leq G (k))$
183	169 173 179 180 181 182	syl122anc	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to (x \leq k \leftrightarrow G (x) \leq G (k))$
184	168 183	bitr4d	$⊢ (((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \land x \in ℕ) \to (G (x) \in (M \dots G (k)) \leftrightarrow x \leq k)$
185	184	pm5.32da	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to ((x \in ℕ \land G (x) \in (M \dots G (k))) \leftrightarrow (x \in ℕ \land x \leq k))$
186		elpreima	$⊢ G Fn ℕ \to (x \in G^{-1} [(M \dots G (k))] \leftrightarrow (x \in ℕ \land G (x) \in (M \dots G (k))))$
187	161 28 186	3syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (x \in G^{-1} [(M \dots G (k))] \leftrightarrow (x \in ℕ \land G (x) \in (M \dots G (k))))$
188		fznn	$⊢ k \in ℤ \to (x \in (1 \dots k) \leftrightarrow (x \in ℕ \land x \leq k))$
189	143 188	syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (x \in (1 \dots k) \leftrightarrow (x \in ℕ \land x \leq k))$
190	185 187 189	3bitr4d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (x \in G^{-1} [(M \dots G (k))] \leftrightarrow x \in (1 \dots k))$
191	190	eqrdv	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G^{-1} [(M \dots G (k))] = (1 \dots k)$
192	191	imaeq2d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G [G^{-1} [(M \dots G (k))]] = G [(1 \dots k)]$
193	192	sseq1d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (G [G^{-1} [(M \dots G (k))]] \subseteq G [G^{-1} [(M \dots j)]] \leftrightarrow G [(1 \dots k)] \subseteq G [G^{-1} [(M \dots j)]])$
194	38	ad2antrr	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G : ℕ \underset{1-1}{⟶} Z$
195		fz1ssnn	$⊢ (1 \dots k) \subseteq ℕ$
196		ovex	$⊢ (1 \dots k) \in V$
197	196	f1imaen	$⊢ (G : ℕ \underset{1-1}{⟶} Z \land (1 \dots k) \subseteq ℕ) \to G [(1 \dots k)] \approx (1 \dots k)$
198	194 195 197	sylancl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G [(1 \dots k)] \approx (1 \dots k)$
199		fzfid	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (1 \dots k) \in Fin$
200		enfii	$⊢ ((1 \dots k) \in Fin \land G [(1 \dots k)] \approx (1 \dots k)) \to G [(1 \dots k)] \in Fin$
201	199 198 200	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G [(1 \dots k)] \in Fin$
202		hashen	$⊢ (G [(1 \dots k)] \in Fin \land (1 \dots k) \in Fin) \to (\|G [(1 \dots k)]\| = \|(1 \dots k)\| \leftrightarrow G [(1 \dots k)] \approx (1 \dots k))$
203	201 199 202	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|G [(1 \dots k)]\| = \|(1 \dots k)\| \leftrightarrow G [(1 \dots k)] \approx (1 \dots k))$
204	198 203	mpbird	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [(1 \dots k)]\| = \|(1 \dots k)\|$
205		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
206		hashfz1	$⊢ k \in ℕ_{0} \to \|(1 \dots k)\| = k$
207	151 205 206	3syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|(1 \dots k)\| = k$
208	204 207	eqtrd	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [(1 \dots k)]\| = k$
209	208	breq1d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|G [(1 \dots k)]\| \leq \|G [G^{-1} [(M \dots j)]]\| \leftrightarrow k \leq \|G [G^{-1} [(M \dots j)]]\|)$
210		hashdom	$⊢ (G [(1 \dots k)] \in Fin \land G [G^{-1} [(M \dots j)]] \in Fin) \to (\|G [(1 \dots k)]\| \leq \|G [G^{-1} [(M \dots j)]]\| \leftrightarrow G [(1 \dots k)] ≼ G [G^{-1} [(M \dots j)]])$
211	201 139 210	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|G [(1 \dots k)]\| \leq \|G [G^{-1} [(M \dots j)]]\| \leftrightarrow G [(1 \dots k)] ≼ G [G^{-1} [(M \dots j)]])$
212	209 211	bitr3d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (k \leq \|G [G^{-1} [(M \dots j)]]\| \leftrightarrow G [(1 \dots k)] ≼ G [G^{-1} [(M \dots j)]])$
213	160 193 212	3imtr4d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (G [G^{-1} [(M \dots G (k))]] \subseteq G [G^{-1} [(M \dots j)]] \to k \leq \|G [G^{-1} [(M \dots j)]]\|)$
214	158 213	syl5	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (j \in ℤ_{\geq G (k)} \to k \leq \|G [G^{-1} [(M \dots j)]]\|)$
215	154 214	mtod	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \neg j \in ℤ_{\geq G (k)}$
216		eluzelz	$⊢ j \in ℤ_{\geq G (1)} \to j \in ℤ$
217	216	ad2antlr	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to j \in ℤ$
218		uztric	$⊢ (G (k) \in ℤ \land j \in ℤ) \to (j \in ℤ_{\geq G (k)} \lor G (k) \in ℤ_{\geq j})$
219	165 217 218	syl2anc	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (j \in ℤ_{\geq G (k)} \lor G (k) \in ℤ_{\geq j})$
220	219	ord	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\neg j \in ℤ_{\geq G (k)} \to G (k) \in ℤ_{\geq j})$
221	215 220	mpd	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to G (k) \in ℤ_{\geq j}$
222		oveq2	$⊢ m = G (k) \to (M \dots m) = (M \dots G (k))$
223	222	imaeq2d	$⊢ m = G (k) \to G^{-1} [(M \dots m)] = G^{-1} [(M \dots G (k))]$
224	223	imaeq2d	$⊢ m = G (k) \to G [G^{-1} [(M \dots m)]] = G [G^{-1} [(M \dots G (k))]]$
225	224	fveq2d	$⊢ m = G (k) \to \|G [G^{-1} [(M \dots m)]]\| = \|G [G^{-1} [(M \dots G (k))]]\|$
226	225	fveq2d	$⊢ m = G (k) \to seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) = seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|)$
227	226	eleq1d	$⊢ m = G (k) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \leftrightarrow seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ)$
228	226	fvoveq1d	$⊢ m = G (k) \to \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| = \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\|$
229	228	breq1d	$⊢ m = G (k) \to (\|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x \leftrightarrow \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x)$
230	227 229	anbi12d	$⊢ m = G (k) \to ((seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \leftrightarrow (seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x))$
231	230	rspcv	$⊢ G (k) \in ℤ_{\geq j} \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x))$
232	221 231	syl	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x))$
233	192	fveq2d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots G (k))]]\| = \|G [(1 \dots k)]\|$
234	233 208	eqtrd	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|G [G^{-1} [(M \dots G (k))]]\| = k$
235	234	fveq2d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) = seq 1 (+ H) (k)$
236	235	eleq1d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ \leftrightarrow seq 1 (+ H) (k) \in ℂ)$
237	235	fvoveq1d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| = \|seq 1 (+ H) (k) - A\|$
238	237	breq1d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x \leftrightarrow \|seq 1 (+ H) (k) - A\| < x)$
239	236 238	anbi12d	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to ((seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots G (k))]]\|) - A\| < x) \leftrightarrow (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
240	232 239	sylibd	$⊢ ((φ \land j \in ℤ_{\geq G (1)}) \land k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}) \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
241	240	ralrimdva	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to \forall k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
242		fveq2	$⊢ n = \|G [G^{-1} [(M \dots j)]]\| + 1 \to ℤ_{\geq n} = ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)}$
243	242	raleqdv	$⊢ n = \|G [G^{-1} [(M \dots j)]]\| + 1 \to (\forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \leftrightarrow \forall k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
244	243	rspcev	$⊢ (\|G [G^{-1} [(M \dots j)]]\| + 1 \in ℕ \land \forall k \in ℤ_{\geq (\|G [G^{-1} [(M \dots j)]]\| + 1)} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x)) \to \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x)$
245	136 241 244	syl6an	$⊢ (φ \land j \in ℤ_{\geq G (1)}) \to (\forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
246	245	rexlimdva	$⊢ φ \to (\exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x) \to \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x))$
247	126 246	impbid	$⊢ φ \to (\exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \leftrightarrow \exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
248	247	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x))$
249	248	anbi2d	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x)))$
250		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
251		1zzd	$⊢ φ \to 1 \in ℤ$
252		seqex	$⊢ seq 1 (+ H) \in V$
253	252	a1i	$⊢ φ \to seq 1 (+ H) \in V$
254		eqidd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) = seq 1 (+ H) (k)$
255	250 251 253 254	clim2	$⊢ φ \to (seq 1 (+ H) ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists n \in ℕ \forall k \in ℤ_{\geq n} (seq 1 (+ H) (k) \in ℂ \land \|seq 1 (+ H) (k) - A\| < x)))$
256	121 122	syl	$⊢ φ \to G (1) \in ℤ$
257		seqex	$⊢ seq M (+ F) \in V$
258	257	a1i	$⊢ φ \to seq M (+ F) \in V$
259	1 2 3 4 5 6 7	isercolllem3	$⊢ (φ \land m \in ℤ_{\geq G (1)}) \to seq M (+ F) (m) = seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|)$
260	123 256 258 259	clim2	$⊢ φ \to (seq M (+ F) ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq G (1)} \forall m \in ℤ_{\geq j} (seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) \in ℂ \land \|seq 1 (+ H) (\|G [G^{-1} [(M \dots m)]]\|) - A\| < x)))$
261	249 255 260	3bitr4d	$⊢ φ \to (seq 1 (+ H) ⇝ A \leftrightarrow seq M (+ F) ⇝ A)$

Metamath Proof Explorer

Theorem isercoll

Proof