seqcoll

Description: The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F . (Contributed by Mario Carneiro, 2-Apr-2014)

	Ref	Expression
Hypotheses	seqcoll.1	$⊢ (φ \land k \in S) \to Z \underset{˙}{+} k = k$
	seqcoll.1b	$⊢ (φ \land k \in S) \to k \underset{˙}{+} Z = k$
	seqcoll.c	$⊢ (φ \land (k \in S \land n \in S)) \to k \underset{˙}{+} n \in S$
	seqcoll.a	$⊢ φ \to Z \in S$
	seqcoll.2	$⊢ φ \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
	seqcoll.3	$⊢ φ \to N \in (1 \dots \|A\|)$
	seqcoll.4	$⊢ φ \to A \subseteq ℤ_{\geq M}$
	seqcoll.5	$⊢ (φ \land k \in (M \dots G (\|A\|))) \to F (k) \in S$
	seqcoll.6	$⊢ (φ \land k \in ((M \dots G (\|A\|)) ∖ A)) \to F (k) = Z$
	seqcoll.7	$⊢ (φ \land n \in (1 \dots \|A\|)) \to H (n) = F (G (n))$
Assertion	seqcoll	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N)$

Proof

Step	Hyp	Ref	Expression
1		seqcoll.1	$⊢ (φ \land k \in S) \to Z \underset{˙}{+} k = k$
2		seqcoll.1b	$⊢ (φ \land k \in S) \to k \underset{˙}{+} Z = k$
3		seqcoll.c	$⊢ (φ \land (k \in S \land n \in S)) \to k \underset{˙}{+} n \in S$
4		seqcoll.a	$⊢ φ \to Z \in S$
5		seqcoll.2	$⊢ φ \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
6		seqcoll.3	$⊢ φ \to N \in (1 \dots \|A\|)$
7		seqcoll.4	$⊢ φ \to A \subseteq ℤ_{\geq M}$
8		seqcoll.5	$⊢ (φ \land k \in (M \dots G (\|A\|))) \to F (k) \in S$
9		seqcoll.6	$⊢ (φ \land k \in ((M \dots G (\|A\|)) ∖ A)) \to F (k) = Z$
10		seqcoll.7	$⊢ (φ \land n \in (1 \dots \|A\|)) \to H (n) = F (G (n))$
11		elfznn	$⊢ N \in (1 \dots \|A\|) \to N \in ℕ$
12	6 11	syl	$⊢ φ \to N \in ℕ$
13		eleq1	$⊢ y = 1 \to (y \in (1 \dots \|A\|) \leftrightarrow 1 \in (1 \dots \|A\|))$
14		2fveq3	$⊢ y = 1 \to seq M (\underset{˙}{+}, F) (G (y)) = seq M (\underset{˙}{+}, F) (G (1))$
15		fveq2	$⊢ y = 1 \to seq 1 (\underset{˙}{+}, H) (y) = seq 1 (\underset{˙}{+}, H) (1)$
16	14 15	eqeq12d	$⊢ y = 1 \to (seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y) \leftrightarrow seq M (\underset{˙}{+}, F) (G (1)) = seq 1 (\underset{˙}{+}, H) (1))$
17	13 16	imbi12d	$⊢ y = 1 \to ((y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y)) \leftrightarrow (1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (1)) = seq 1 (\underset{˙}{+}, H) (1)))$
18	17	imbi2d	$⊢ y = 1 \to ((φ \to (y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y))) \leftrightarrow (φ \to (1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (1)) = seq 1 (\underset{˙}{+}, H) (1))))$
19		eleq1	$⊢ y = m \to (y \in (1 \dots \|A\|) \leftrightarrow m \in (1 \dots \|A\|))$
20		2fveq3	$⊢ y = m \to seq M (\underset{˙}{+}, F) (G (y)) = seq M (\underset{˙}{+}, F) (G (m))$
21		fveq2	$⊢ y = m \to seq 1 (\underset{˙}{+}, H) (y) = seq 1 (\underset{˙}{+}, H) (m)$
22	20 21	eqeq12d	$⊢ y = m \to (seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y) \leftrightarrow seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m))$
23	19 22	imbi12d	$⊢ y = m \to ((y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y)) \leftrightarrow (m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)))$
24	23	imbi2d	$⊢ y = m \to ((φ \to (y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y))) \leftrightarrow (φ \to (m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m))))$
25		eleq1	$⊢ y = m + 1 \to (y \in (1 \dots \|A\|) \leftrightarrow m + 1 \in (1 \dots \|A\|))$
26		2fveq3	$⊢ y = m + 1 \to seq M (\underset{˙}{+}, F) (G (y)) = seq M (\underset{˙}{+}, F) (G (m + 1))$
27		fveq2	$⊢ y = m + 1 \to seq 1 (\underset{˙}{+}, H) (y) = seq 1 (\underset{˙}{+}, H) (m + 1)$
28	26 27	eqeq12d	$⊢ y = m + 1 \to (seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y) \leftrightarrow seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1))$
29	25 28	imbi12d	$⊢ y = m + 1 \to ((y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y)) \leftrightarrow (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1)))$
30	29	imbi2d	$⊢ y = m + 1 \to ((φ \to (y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y))) \leftrightarrow (φ \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1))))$
31		eleq1	$⊢ y = N \to (y \in (1 \dots \|A\|) \leftrightarrow N \in (1 \dots \|A\|))$
32		2fveq3	$⊢ y = N \to seq M (\underset{˙}{+}, F) (G (y)) = seq M (\underset{˙}{+}, F) (G (N))$
33		fveq2	$⊢ y = N \to seq 1 (\underset{˙}{+}, H) (y) = seq 1 (\underset{˙}{+}, H) (N)$
34	32 33	eqeq12d	$⊢ y = N \to (seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y) \leftrightarrow seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N))$
35	31 34	imbi12d	$⊢ y = N \to ((y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y)) \leftrightarrow (N \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N)))$
36	35	imbi2d	$⊢ y = N \to ((φ \to (y \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (y)) = seq 1 (\underset{˙}{+}, H) (y))) \leftrightarrow (φ \to (N \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N))))$
37		isof1o	$⊢ G {Isom}_{<, <} ((1 \dots \|A\|), A) \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
38	5 37	syl	$⊢ φ \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
39		f1of	$⊢ G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to G : (1 \dots \|A\|) ⟶ A$
40	38 39	syl	$⊢ φ \to G : (1 \dots \|A\|) ⟶ A$
41		elfzuz2	$⊢ N \in (1 \dots \|A\|) \to \|A\| \in ℤ_{\geq 1}$
42	6 41	syl	$⊢ φ \to \|A\| \in ℤ_{\geq 1}$
43		eluzfz1	$⊢ \|A\| \in ℤ_{\geq 1} \to 1 \in (1 \dots \|A\|)$
44	42 43	syl	$⊢ φ \to 1 \in (1 \dots \|A\|)$
45	40 44	ffvelrnd	$⊢ φ \to G (1) \in A$
46	7 45	sseldd	$⊢ φ \to G (1) \in ℤ_{\geq M}$
47		eluzle	$⊢ \|A\| \in ℤ_{\geq 1} \to 1 \leq \|A\|$
48	42 47	syl	$⊢ φ \to 1 \leq \|A\|$
49		fzssz	$⊢ (1 \dots \|A\|) \subseteq ℤ$
50		zssre	$⊢ ℤ \subseteq ℝ$
51	49 50	sstri	$⊢ (1 \dots \|A\|) \subseteq ℝ$
52	51	a1i	$⊢ φ \to (1 \dots \|A\|) \subseteq ℝ$
53		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
54	52 53	sstrdi	$⊢ φ \to (1 \dots \|A\|) \subseteq ℝ^{*}$
55		eluzelre	$⊢ k \in ℤ_{\geq M} \to k \in ℝ$
56	55	ssriv	$⊢ ℤ_{\geq M} \subseteq ℝ$
57	7 56	sstrdi	$⊢ φ \to A \subseteq ℝ$
58	57 53	sstrdi	$⊢ φ \to A \subseteq ℝ^{*}$
59		eluzfz2	$⊢ \|A\| \in ℤ_{\geq 1} \to \|A\| \in (1 \dots \|A\|)$
60	42 59	syl	$⊢ φ \to \|A\| \in (1 \dots \|A\|)$
61		leisorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land ((1 \dots \|A\|) \subseteq ℝ^{} \land A \subseteq ℝ^{}) \land (1 \in (1 \dots \|A\|) \land \|A\| \in (1 \dots \|A\|))) \to (1 \leq \|A\| \leftrightarrow G (1) \leq G (\|A\|))$
62	5 54 58 44 60 61	syl122anc	$⊢ φ \to (1 \leq \|A\| \leftrightarrow G (1) \leq G (\|A\|))$
63	48 62	mpbid	$⊢ φ \to G (1) \leq G (\|A\|)$
64	40 60	ffvelrnd	$⊢ φ \to G (\|A\|) \in A$
65	7 64	sseldd	$⊢ φ \to G (\|A\|) \in ℤ_{\geq M}$
66		eluzelz	$⊢ G (\|A\|) \in ℤ_{\geq M} \to G (\|A\|) \in ℤ$
67	65 66	syl	$⊢ φ \to G (\|A\|) \in ℤ$
68		elfz5	$⊢ (G (1) \in ℤ_{\geq M} \land G (\|A\|) \in ℤ) \to (G (1) \in (M \dots G (\|A\|)) \leftrightarrow G (1) \leq G (\|A\|))$
69	46 67 68	syl2anc	$⊢ φ \to (G (1) \in (M \dots G (\|A\|)) \leftrightarrow G (1) \leq G (\|A\|))$
70	63 69	mpbird	$⊢ φ \to G (1) \in (M \dots G (\|A\|))$
71		fveq2	$⊢ k = G (1) \to F (k) = F (G (1))$
72	71	eleq1d	$⊢ k = G (1) \to (F (k) \in S \leftrightarrow F (G (1)) \in S)$
73	72	imbi2d	$⊢ k = G (1) \to ((φ \to F (k) \in S) \leftrightarrow (φ \to F (G (1)) \in S))$
74	8	expcom	$⊢ k \in (M \dots G (\|A\|)) \to (φ \to F (k) \in S)$
75	73 74	vtoclga	$⊢ G (1) \in (M \dots G (\|A\|)) \to (φ \to F (G (1)) \in S)$
76	70 75	mpcom	$⊢ φ \to F (G (1)) \in S$
77		eluzelz	$⊢ G (1) \in ℤ_{\geq M} \to G (1) \in ℤ$
78	46 77	syl	$⊢ φ \to G (1) \in ℤ$
79		peano2zm	$⊢ G (1) \in ℤ \to G (1) - 1 \in ℤ$
80	78 79	syl	$⊢ φ \to G (1) - 1 \in ℤ$
81	80	zred	$⊢ φ \to G (1) - 1 \in ℝ$
82	78	zred	$⊢ φ \to G (1) \in ℝ$
83	67	zred	$⊢ φ \to G (\|A\|) \in ℝ$
84	82	lem1d	$⊢ φ \to G (1) - 1 \leq G (1)$
85	81 82 83 84 63	letrd	$⊢ φ \to G (1) - 1 \leq G (\|A\|)$
86		eluz	$⊢ (G (1) - 1 \in ℤ \land G (\|A\|) \in ℤ) \to (G (\|A\|) \in ℤ_{\geq (G (1) - 1)} \leftrightarrow G (1) - 1 \leq G (\|A\|))$
87	80 67 86	syl2anc	$⊢ φ \to (G (\|A\|) \in ℤ_{\geq (G (1) - 1)} \leftrightarrow G (1) - 1 \leq G (\|A\|))$
88	85 87	mpbird	$⊢ φ \to G (\|A\|) \in ℤ_{\geq (G (1) - 1)}$
89		fzss2	$⊢ G (\|A\|) \in ℤ_{\geq (G (1) - 1)} \to (M \dots G (1) - 1) \subseteq (M \dots G (\|A\|))$
90	88 89	syl	$⊢ φ \to (M \dots G (1) - 1) \subseteq (M \dots G (\|A\|))$
91	90	sselda	$⊢ (φ \land k \in (M \dots G (1) - 1)) \to k \in (M \dots G (\|A\|))$
92		eluzel2	$⊢ G (1) \in ℤ_{\geq M} \to M \in ℤ$
93	46 92	syl	$⊢ φ \to M \in ℤ$
94		elfzm11	$⊢ (M \in ℤ \land G (1) \in ℤ) \to (k \in (M \dots G (1) - 1) \leftrightarrow (k \in ℤ \land M \leq k \land k < G (1)))$
95	93 78 94	syl2anc	$⊢ φ \to (k \in (M \dots G (1) - 1) \leftrightarrow (k \in ℤ \land M \leq k \land k < G (1)))$
96		simp3	$⊢ (k \in ℤ \land M \leq k \land k < G (1)) \to k < G (1)$
97	82	adantr	$⊢ (φ \land k \in A) \to G (1) \in ℝ$
98	57	sselda	$⊢ (φ \land k \in A) \to k \in ℝ$
99		f1ocnv	$⊢ G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|)$
100	38 99	syl	$⊢ φ \to G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|)$
101		f1of	$⊢ G^{-1} : A \underset{1-1 onto}{⟶} (1 \dots \|A\|) \to G^{-1} : A ⟶ (1 \dots \|A\|)$
102	100 101	syl	$⊢ φ \to G^{-1} : A ⟶ (1 \dots \|A\|)$
103	102	ffvelrnda	$⊢ (φ \land k \in A) \to G^{-1} (k) \in (1 \dots \|A\|)$
104		elfznn	$⊢ G^{-1} (k) \in (1 \dots \|A\|) \to G^{-1} (k) \in ℕ$
105	103 104	syl	$⊢ (φ \land k \in A) \to G^{-1} (k) \in ℕ$
106	105	nnge1d	$⊢ (φ \land k \in A) \to 1 \leq G^{-1} (k)$
107	5	adantr	$⊢ (φ \land k \in A) \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
108	54	adantr	$⊢ (φ \land k \in A) \to (1 \dots \|A\|) \subseteq ℝ^{*}$
109	58	adantr	$⊢ (φ \land k \in A) \to A \subseteq ℝ^{*}$
110	44	adantr	$⊢ (φ \land k \in A) \to 1 \in (1 \dots \|A\|)$
111		leisorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land ((1 \dots \|A\|) \subseteq ℝ^{} \land A \subseteq ℝ^{}) \land (1 \in (1 \dots \|A\|) \land G^{-1} (k) \in (1 \dots \|A\|))) \to (1 \leq G^{-1} (k) \leftrightarrow G (1) \leq G (G^{-1} (k)))$
112	107 108 109 110 103 111	syl122anc	$⊢ (φ \land k \in A) \to (1 \leq G^{-1} (k) \leftrightarrow G (1) \leq G (G^{-1} (k)))$
113	106 112	mpbid	$⊢ (φ \land k \in A) \to G (1) \leq G (G^{-1} (k))$
114		f1ocnvfv2	$⊢ (G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land k \in A) \to G (G^{-1} (k)) = k$
115	38 114	sylan	$⊢ (φ \land k \in A) \to G (G^{-1} (k)) = k$
116	113 115	breqtrd	$⊢ (φ \land k \in A) \to G (1) \leq k$
117	97 98 116	lensymd	$⊢ (φ \land k \in A) \to \neg k < G (1)$
118	117	ex	$⊢ φ \to (k \in A \to \neg k < G (1))$
119	118	con2d	$⊢ φ \to (k < G (1) \to \neg k \in A)$
120	96 119	syl5	$⊢ φ \to ((k \in ℤ \land M \leq k \land k < G (1)) \to \neg k \in A)$
121	95 120	sylbid	$⊢ φ \to (k \in (M \dots G (1) - 1) \to \neg k \in A)$
122	121	imp	$⊢ (φ \land k \in (M \dots G (1) - 1)) \to \neg k \in A$
123	91 122	eldifd	$⊢ (φ \land k \in (M \dots G (1) - 1)) \to k \in ((M \dots G (\|A\|)) ∖ A)$
124	123 9	syldan	$⊢ (φ \land k \in (M \dots G (1) - 1)) \to F (k) = Z$
125	1 4 46 76 124	seqid	$⊢ φ \to {seq M (\underset{˙}{+}, F) ↾}_{ℤ_{\geq G (1)}} = seq G (1) (\underset{˙}{+}, F)$
126	125	fveq1d	$⊢ φ \to ({seq M (\underset{˙}{+}, F) ↾}_{ℤ_{\geq G (1)}}) (G (1)) = seq G (1) (\underset{˙}{+}, F) (G (1))$
127		uzid	$⊢ G (1) \in ℤ \to G (1) \in ℤ_{\geq G (1)}$
128	78 127	syl	$⊢ φ \to G (1) \in ℤ_{\geq G (1)}$
129	128	fvresd	$⊢ φ \to ({seq M (\underset{˙}{+}, F) ↾}_{ℤ_{\geq G (1)}}) (G (1)) = seq M (\underset{˙}{+}, F) (G (1))$
130		seq1	$⊢ G (1) \in ℤ \to seq G (1) (\underset{˙}{+}, F) (G (1)) = F (G (1))$
131	78 130	syl	$⊢ φ \to seq G (1) (\underset{˙}{+}, F) (G (1)) = F (G (1))$
132		fveq2	$⊢ n = 1 \to H (n) = H (1)$
133		2fveq3	$⊢ n = 1 \to F (G (n)) = F (G (1))$
134	132 133	eqeq12d	$⊢ n = 1 \to (H (n) = F (G (n)) \leftrightarrow H (1) = F (G (1)))$
135	134	imbi2d	$⊢ n = 1 \to ((φ \to H (n) = F (G (n))) \leftrightarrow (φ \to H (1) = F (G (1))))$
136	10	expcom	$⊢ n \in (1 \dots \|A\|) \to (φ \to H (n) = F (G (n)))$
137	135 136	vtoclga	$⊢ 1 \in (1 \dots \|A\|) \to (φ \to H (1) = F (G (1)))$
138	44 137	mpcom	$⊢ φ \to H (1) = F (G (1))$
139	131 138	eqtr4d	$⊢ φ \to seq G (1) (\underset{˙}{+}, F) (G (1)) = H (1)$
140	126 129 139	3eqtr3d	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (1)) = H (1)$
141		1z	$⊢ 1 \in ℤ$
142		seq1	$⊢ 1 \in ℤ \to seq 1 (\underset{˙}{+}, H) (1) = H (1)$
143	141 142	ax-mp	$⊢ seq 1 (\underset{˙}{+}, H) (1) = H (1)$
144	140 143	eqtr4di	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (1)) = seq 1 (\underset{˙}{+}, H) (1)$
145	144	a1d	$⊢ φ \to (1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (1)) = seq 1 (\underset{˙}{+}, H) (1))$
146		simplr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m \in ℕ$
147		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
148	146 147	eleqtrdi	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m \in ℤ_{\geq 1}$
149		nnz	$⊢ m \in ℕ \to m \in ℤ$
150	149	ad2antlr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m \in ℤ$
151		elfzuz3	$⊢ m + 1 \in (1 \dots \|A\|) \to \|A\| \in ℤ_{\geq (m + 1)}$
152	151	adantl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to \|A\| \in ℤ_{\geq (m + 1)}$
153		peano2uzr	$⊢ (m \in ℤ \land \|A\| \in ℤ_{\geq (m + 1)}) \to \|A\| \in ℤ_{\geq m}$
154	150 152 153	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to \|A\| \in ℤ_{\geq m}$
155		elfzuzb	$⊢ m \in (1 \dots \|A\|) \leftrightarrow (m \in ℤ_{\geq 1} \land \|A\| \in ℤ_{\geq m})$
156	148 154 155	sylanbrc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m \in (1 \dots \|A\|)$
157	156	ex	$⊢ (φ \land m \in ℕ) \to (m + 1 \in (1 \dots \|A\|) \to m \in (1 \dots \|A\|))$
158	157	imim1d	$⊢ (φ \land m \in ℕ) \to ((m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)) \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)))$
159		oveq1	$⊢ seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m) \to seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} H (m + 1) = seq 1 (\underset{˙}{+}, H) (m) \underset{˙}{+} H (m + 1)$
160	2	ad4ant14	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in S) \to k \underset{˙}{+} Z = k$
161	7	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to A \subseteq ℤ_{\geq M}$
162	40	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G : (1 \dots \|A\|) ⟶ A$
163	162 156	ffvelrnd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) \in A$
164	161 163	sseldd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) \in ℤ_{\geq M}$
165		nnre	$⊢ m \in ℕ \to m \in ℝ$
166	165	ad2antlr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m \in ℝ$
167	166	ltp1d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m < m + 1$
168	5	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
169		simpr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m + 1 \in (1 \dots \|A\|)$
170		isorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land (m \in (1 \dots \|A\|) \land m + 1 \in (1 \dots \|A\|))) \to (m < m + 1 \leftrightarrow G (m) < G (m + 1))$
171	168 156 169 170	syl12anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (m < m + 1 \leftrightarrow G (m) < G (m + 1))$
172	167 171	mpbid	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) < G (m + 1)$
173		eluzelz	$⊢ G (m) \in ℤ_{\geq M} \to G (m) \in ℤ$
174	164 173	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) \in ℤ$
175	162 169	ffvelrnd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in A$
176	161 175	sseldd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in ℤ_{\geq M}$
177		eluzelz	$⊢ G (m + 1) \in ℤ_{\geq M} \to G (m + 1) \in ℤ$
178	176 177	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in ℤ$
179		zltlem1	$⊢ (G (m) \in ℤ \land G (m + 1) \in ℤ) \to (G (m) < G (m + 1) \leftrightarrow G (m) \leq G (m + 1) - 1)$
180	174 178 179	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (G (m) < G (m + 1) \leftrightarrow G (m) \leq G (m + 1) - 1)$
181	172 180	mpbid	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) \leq G (m + 1) - 1$
182		peano2zm	$⊢ G (m + 1) \in ℤ \to G (m + 1) - 1 \in ℤ$
183	178 182	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \in ℤ$
184		eluz	$⊢ (G (m) \in ℤ \land G (m + 1) - 1 \in ℤ) \to (G (m + 1) - 1 \in ℤ_{\geq G (m)} \leftrightarrow G (m) \leq G (m + 1) - 1)$
185	174 183 184	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (G (m + 1) - 1 \in ℤ_{\geq G (m)} \leftrightarrow G (m) \leq G (m + 1) - 1)$
186	181 185	mpbird	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \in ℤ_{\geq G (m)}$
187	183	zred	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \in ℝ$
188	178	zred	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in ℝ$
189	83	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (\|A\|) \in ℝ$
190	188	lem1d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \leq G (m + 1)$
191		elfzle2	$⊢ m + 1 \in (1 \dots \|A\|) \to m + 1 \leq \|A\|$
192	191	adantl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to m + 1 \leq \|A\|$
193	54	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (1 \dots \|A\|) \subseteq ℝ^{*}$
194	58	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to A \subseteq ℝ^{*}$
195	60	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to \|A\| \in (1 \dots \|A\|)$
196		leisorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land ((1 \dots \|A\|) \subseteq ℝ^{} \land A \subseteq ℝ^{}) \land (m + 1 \in (1 \dots \|A\|) \land \|A\| \in (1 \dots \|A\|))) \to (m + 1 \leq \|A\| \leftrightarrow G (m + 1) \leq G (\|A\|))$
197	168 193 194 169 195 196	syl122anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (m + 1 \leq \|A\| \leftrightarrow G (m + 1) \leq G (\|A\|))$
198	192 197	mpbid	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \leq G (\|A\|)$
199	187 188 189 190 198	letrd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \leq G (\|A\|)$
200	67	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (\|A\|) \in ℤ$
201		eluz	$⊢ (G (m + 1) - 1 \in ℤ \land G (\|A\|) \in ℤ) \to (G (\|A\|) \in ℤ_{\geq (G (m + 1) - 1)} \leftrightarrow G (m + 1) - 1 \leq G (\|A\|))$
202	183 200 201	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (G (\|A\|) \in ℤ_{\geq (G (m + 1) - 1)} \leftrightarrow G (m + 1) - 1 \leq G (\|A\|))$
203	199 202	mpbird	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (\|A\|) \in ℤ_{\geq (G (m + 1) - 1)}$
204		uztrn	$⊢ (G (\|A\|) \in ℤ_{\geq (G (m + 1) - 1)} \land G (m + 1) - 1 \in ℤ_{\geq G (m)}) \to G (\|A\|) \in ℤ_{\geq G (m)}$
205	203 186 204	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (\|A\|) \in ℤ_{\geq G (m)}$
206		fzss2	$⊢ G (\|A\|) \in ℤ_{\geq G (m)} \to (M \dots G (m)) \subseteq (M \dots G (\|A\|))$
207	205 206	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (M \dots G (m)) \subseteq (M \dots G (\|A\|))$
208	207	sselda	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (M \dots G (m))) \to k \in (M \dots G (\|A\|))$
209	8	ad4ant14	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (M \dots G (\|A\|))) \to F (k) \in S$
210	208 209	syldan	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (M \dots G (m))) \to F (k) \in S$
211	3	ad4ant14	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land (k \in S \land n \in S)) \to k \underset{˙}{+} n \in S$
212	164 210 211	seqcl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m)) \in S$
213		simplll	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to φ$
214		elfzuz	$⊢ k \in (G (m) + 1 \dots G (m + 1) - 1) \to k \in ℤ_{\geq (G (m) + 1)}$
215		peano2uz	$⊢ G (m) \in ℤ_{\geq M} \to G (m) + 1 \in ℤ_{\geq M}$
216	164 215	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m) + 1 \in ℤ_{\geq M}$
217		uztrn	$⊢ (k \in ℤ_{\geq (G (m) + 1)} \land G (m) + 1 \in ℤ_{\geq M}) \to k \in ℤ_{\geq M}$
218	214 216 217	syl2anr	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to k \in ℤ_{\geq M}$
219		elfzuz3	$⊢ k \in (G (m) + 1 \dots G (m + 1) - 1) \to G (m + 1) - 1 \in ℤ_{\geq k}$
220		uztrn	$⊢ (G (\|A\|) \in ℤ_{\geq (G (m + 1) - 1)} \land G (m + 1) - 1 \in ℤ_{\geq k}) \to G (\|A\|) \in ℤ_{\geq k}$
221	203 219 220	syl2an	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to G (\|A\|) \in ℤ_{\geq k}$
222		elfzuzb	$⊢ k \in (M \dots G (\|A\|)) \leftrightarrow (k \in ℤ_{\geq M} \land G (\|A\|) \in ℤ_{\geq k})$
223	218 221 222	sylanbrc	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to k \in (M \dots G (\|A\|))$
224	149	ad2antlr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to m \in ℤ$
225	102	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G^{-1} : A ⟶ (1 \dots \|A\|)$
226		simprr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to k \in A$
227	225 226	ffvelrnd	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G^{-1} (k) \in (1 \dots \|A\|)$
228	227	elfzelzd	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G^{-1} (k) \in ℤ$
229		btwnnz	$⊢ (m \in ℤ \land m < G^{-1} (k) \land G^{-1} (k) < m + 1) \to \neg G^{-1} (k) \in ℤ$
230	229	3expib	$⊢ m \in ℤ \to ((m < G^{-1} (k) \land G^{-1} (k) < m + 1) \to \neg G^{-1} (k) \in ℤ)$
231	230	con2d	$⊢ m \in ℤ \to (G^{-1} (k) \in ℤ \to \neg (m < G^{-1} (k) \land G^{-1} (k) < m + 1))$
232	224 228 231	sylc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to \neg (m < G^{-1} (k) \land G^{-1} (k) < m + 1)$
233	5	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G {Isom}_{<, <} ((1 \dots \|A\|), A)$
234	156	adantrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to m \in (1 \dots \|A\|)$
235		isorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land (m \in (1 \dots \|A\|) \land G^{-1} (k) \in (1 \dots \|A\|))) \to (m < G^{-1} (k) \leftrightarrow G (m) < G (G^{-1} (k)))$
236	233 234 227 235	syl12anc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (m < G^{-1} (k) \leftrightarrow G (m) < G (G^{-1} (k)))$
237	38	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
238	237 226 114	syl2anc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G (G^{-1} (k)) = k$
239	238	breq2d	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (G (m) < G (G^{-1} (k)) \leftrightarrow G (m) < k)$
240	174	adantrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G (m) \in ℤ$
241	7	ad2antrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to A \subseteq ℤ_{\geq M}$
242	241 226	sseldd	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to k \in ℤ_{\geq M}$
243		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
244	242 243	syl	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to k \in ℤ$
245		zltp1le	$⊢ (G (m) \in ℤ \land k \in ℤ) \to (G (m) < k \leftrightarrow G (m) + 1 \leq k)$
246	240 244 245	syl2anc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (G (m) < k \leftrightarrow G (m) + 1 \leq k)$
247	236 239 246	3bitrd	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (m < G^{-1} (k) \leftrightarrow G (m) + 1 \leq k)$
248	169	adantrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to m + 1 \in (1 \dots \|A\|)$
249		isorel	$⊢ (G {Isom}_{<, <} ((1 \dots \|A\|), A) \land (G^{-1} (k) \in (1 \dots \|A\|) \land m + 1 \in (1 \dots \|A\|))) \to (G^{-1} (k) < m + 1 \leftrightarrow G (G^{-1} (k)) < G (m + 1))$
250	233 227 248 249	syl12anc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (G^{-1} (k) < m + 1 \leftrightarrow G (G^{-1} (k)) < G (m + 1))$
251	238	breq1d	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (G (G^{-1} (k)) < G (m + 1) \leftrightarrow k < G (m + 1))$
252	178	adantrr	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to G (m + 1) \in ℤ$
253		zltlem1	$⊢ (k \in ℤ \land G (m + 1) \in ℤ) \to (k < G (m + 1) \leftrightarrow k \leq G (m + 1) - 1)$
254	244 252 253	syl2anc	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (k < G (m + 1) \leftrightarrow k \leq G (m + 1) - 1)$
255	250 251 254	3bitrd	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to (G^{-1} (k) < m + 1 \leftrightarrow k \leq G (m + 1) - 1)$
256	247 255	anbi12d	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to ((m < G^{-1} (k) \land G^{-1} (k) < m + 1) \leftrightarrow (G (m) + 1 \leq k \land k \leq G (m + 1) - 1))$
257	232 256	mtbid	$⊢ ((φ \land m \in ℕ) \land (m + 1 \in (1 \dots \|A\|) \land k \in A)) \to \neg (G (m) + 1 \leq k \land k \leq G (m + 1) - 1)$
258	257	expr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (k \in A \to \neg (G (m) + 1 \leq k \land k \leq G (m + 1) - 1))$
259	258	con2d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to ((G (m) + 1 \leq k \land k \leq G (m + 1) - 1) \to \neg k \in A)$
260		elfzle1	$⊢ k \in (G (m) + 1 \dots G (m + 1) - 1) \to G (m) + 1 \leq k$
261		elfzle2	$⊢ k \in (G (m) + 1 \dots G (m + 1) - 1) \to k \leq G (m + 1) - 1$
262	260 261	jca	$⊢ k \in (G (m) + 1 \dots G (m + 1) - 1) \to (G (m) + 1 \leq k \land k \leq G (m + 1) - 1)$
263	259 262	impel	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to \neg k \in A$
264	223 263	eldifd	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to k \in ((M \dots G (\|A\|)) ∖ A)$
265	213 264 9	syl2anc	$⊢ (((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \land k \in (G (m) + 1 \dots G (m + 1) - 1)) \to F (k) = Z$
266	160 164 186 212 265	seqid2	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m)) = seq M (\underset{˙}{+}, F) (G (m + 1) - 1)$
267	266	oveq1d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} F (G (m + 1)) = seq M (\underset{˙}{+}, F) (G (m + 1) - 1) \underset{˙}{+} F (G (m + 1))$
268		fveq2	$⊢ n = m + 1 \to H (n) = H (m + 1)$
269		2fveq3	$⊢ n = m + 1 \to F (G (n)) = F (G (m + 1))$
270	268 269	eqeq12d	$⊢ n = m + 1 \to (H (n) = F (G (n)) \leftrightarrow H (m + 1) = F (G (m + 1)))$
271	270	imbi2d	$⊢ n = m + 1 \to ((φ \to H (n) = F (G (n))) \leftrightarrow (φ \to H (m + 1) = F (G (m + 1))))$
272	271 136	vtoclga	$⊢ m + 1 \in (1 \dots \|A\|) \to (φ \to H (m + 1) = F (G (m + 1)))$
273	272	impcom	$⊢ (φ \land m + 1 \in (1 \dots \|A\|)) \to H (m + 1) = F (G (m + 1))$
274	273	adantlr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to H (m + 1) = F (G (m + 1))$
275	274	oveq2d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} H (m + 1) = seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} F (G (m + 1))$
276	93	ad2antrr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to M \in ℤ$
277	178	zcnd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in ℂ$
278		ax-1cn	$⊢ 1 \in ℂ$
279		npcan	$⊢ (G (m + 1) \in ℂ \land 1 \in ℂ) \to G (m + 1) - 1 + 1 = G (m + 1)$
280	277 278 279	sylancl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 + 1 = G (m + 1)$
281		uztrn	$⊢ (G (m + 1) - 1 \in ℤ_{\geq G (m)} \land G (m) \in ℤ_{\geq M}) \to G (m + 1) - 1 \in ℤ_{\geq M}$
282	186 164 281	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 \in ℤ_{\geq M}$
283		eluzp1p1	$⊢ G (m + 1) - 1 \in ℤ_{\geq M} \to G (m + 1) - 1 + 1 \in ℤ_{\geq (M + 1)}$
284	282 283	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) - 1 + 1 \in ℤ_{\geq (M + 1)}$
285	280 284	eqeltrrd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to G (m + 1) \in ℤ_{\geq (M + 1)}$
286		seqm1	$⊢ (M \in ℤ \land G (m + 1) \in ℤ_{\geq (M + 1)}) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq M (\underset{˙}{+}, F) (G (m + 1) - 1) \underset{˙}{+} F (G (m + 1))$
287	276 285 286	syl2anc	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq M (\underset{˙}{+}, F) (G (m + 1) - 1) \underset{˙}{+} F (G (m + 1))$
288	267 275 287	3eqtr4rd	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} H (m + 1)$
289		seqp1	$⊢ m \in ℤ_{\geq 1} \to seq 1 (\underset{˙}{+}, H) (m + 1) = seq 1 (\underset{˙}{+}, H) (m) \underset{˙}{+} H (m + 1)$
290	148 289	syl	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to seq 1 (\underset{˙}{+}, H) (m + 1) = seq 1 (\underset{˙}{+}, H) (m) \underset{˙}{+} H (m + 1)$
291	288 290	eqeq12d	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1) \leftrightarrow seq M (\underset{˙}{+}, F) (G (m)) \underset{˙}{+} H (m + 1) = seq 1 (\underset{˙}{+}, H) (m) \underset{˙}{+} H (m + 1))$
292	159 291	syl5ibr	$⊢ ((φ \land m \in ℕ) \land m + 1 \in (1 \dots \|A\|)) \to (seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1))$
293	292	ex	$⊢ (φ \land m \in ℕ) \to (m + 1 \in (1 \dots \|A\|) \to (seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1)))$
294	293	a2d	$⊢ (φ \land m \in ℕ) \to ((m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)) \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1)))$
295	158 294	syld	$⊢ (φ \land m \in ℕ) \to ((m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)) \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1)))$
296	295	expcom	$⊢ m \in ℕ \to (φ \to ((m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m)) \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1))))$
297	296	a2d	$⊢ m \in ℕ \to ((φ \to (m \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m)) = seq 1 (\underset{˙}{+}, H) (m))) \to (φ \to (m + 1 \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (m + 1)) = seq 1 (\underset{˙}{+}, H) (m + 1))))$
298	18 24 30 36 145 297	nnind	$⊢ N \in ℕ \to (φ \to (N \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N)))$
299	12 298	mpcom	$⊢ φ \to (N \in (1 \dots \|A\|) \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N))$
300	6 299	mpd	$⊢ φ \to seq M (\underset{˙}{+}, F) (G (N)) = seq 1 (\underset{˙}{+}, H) (N)$

Metamath Proof Explorer

Theorem seqcoll

Proof