Theorem seqf1olem2a

Description: Lemma for seqf1o . (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	seqf1o.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
	seqf1o.2	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
	seqf1o.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
	seqf1o.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	seqf1o.5	$$⊢\phi \to C\subseteq S$$
	seqf1olem2a.1	$$⊢\phi \to G:A⟶C$$
	seqf1olem2a.3	$$⊢\phi \to K\in A$$
	seqf1olem2a.4	$$⊢\phi \to \left(M\dots N\right)\subseteq A$$
Assertion	seqf1olem2a	$$⊢\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)$$

Proof

Step	Hyp	Ref	Expression
1		seqf1o.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
2		seqf1o.2	$$⊢\left(\phi \wedge \left(x\in C\wedge y\in C\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
3		seqf1o.3	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
4		seqf1o.4	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
5		seqf1o.5	$$⊢\phi \to C\subseteq S$$
6		seqf1olem2a.1	$$⊢\phi \to G:A⟶C$$
7		seqf1olem2a.3	$$⊢\phi \to K\in A$$
8		seqf1olem2a.4	$$⊢\phi \to \left(M\dots N\right)\subseteq A$$
9		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
10	4 9	syl	$$⊢\phi \to N\in \left(M\dots N\right)$$
11		fveq2	$$⊢m=M\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)$$
12	11	oveq2d	$$⊢m=M\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)$$
13	11	oveq1d	$$⊢m=M\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\underset{\dot{}}{+}G\left(K\right)$$
14	12 13	eqeq12d	$$⊢m=M\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\leftrightarrow G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
15	14	imbi2d	$$⊢m=M\to \left(\left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\right)\leftrightarrow \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
16		fveq2	$$⊢m=n\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)$$
17	16	oveq2d	$$⊢m=n\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)$$
18	16	oveq1d	$$⊢m=n\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)$$
19	17 18	eqeq12d	$$⊢m=n\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\leftrightarrow G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
20	19	imbi2d	$$⊢m=n\to \left(\left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\right)\leftrightarrow \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
21		fveq2	$$⊢m=n+1\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)$$
22	21	oveq2d	$$⊢m=n+1\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)$$
23	21	oveq1d	$$⊢m=n+1\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)$$
24	22 23	eqeq12d	$$⊢m=n+1\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\leftrightarrow G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
25	24	imbi2d	$$⊢m=n+1\to \left(\left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\right)\leftrightarrow \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
26		fveq2	$$⊢m=N\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)$$
27	26	oveq2d	$$⊢m=N\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)$$
28	26	oveq1d	$$⊢m=N\to seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)$$
29	27 28	eqeq12d	$$⊢m=N\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\leftrightarrow G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
30	29	imbi2d	$$⊢m=N\to \left(\left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(m\right)\underset{\dot{}}{+}G\left(K\right)\right)\leftrightarrow \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
31	6 7	ffvelrnd	$$⊢\phi \to G\left(K\right)\in C$$
32		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
33		seq1	$$⊢M\in \mathbb{Z}\to seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=G\left(M\right)$$
34	4 32 33	3syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=G\left(M\right)$$
35		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
36	4 35	syl	$$⊢\phi \to M\in \left(M\dots N\right)$$
37	8 36	sseldd	$$⊢\phi \to M\in A$$
38	6 37	ffvelrnd	$$⊢\phi \to G\left(M\right)\in C$$
39	34 38	eqeltrd	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\in C$$
40	2 31 39	caovcomd	$$⊢\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\underset{\dot{}}{+}G\left(K\right)$$
41	40	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(M\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
42		oveq1	$$⊢G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\right)\underset{\dot{}}{+}G\left(n+1\right)=\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\underset{\dot{}}{+}G\left(n+1\right)$$
43		elfzouz	$$⊢n\in \left(M..^N\right)\to n\in {\mathbb{Z}}_{\ge M}$$
44	43	adantl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to n\in {\mathbb{Z}}_{\ge M}$$
45		seqp1	$$⊢n\in {\mathbb{Z}}_{\ge M}\to seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)$$
46	44 45	syl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)$$
47	46	oveq2d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=G\left(K\right)\underset{\dot{}}{+}\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)\right)$$
48	3	adantlr	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge \left(x\in S\wedge y\in S\wedge z\in S\right)\right)\to \left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)$$
49	5 31	sseldd	$$⊢\phi \to G\left(K\right)\in S$$
50	49	adantr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(K\right)\in S$$
51	5	adantr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to C\subseteq S$$
52	51	adantr	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge x\in \left(M\dots n\right)\right)\to C\subseteq S$$
53	6	adantr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G:A⟶C$$
54	53	adantr	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge x\in \left(M\dots n\right)\right)\to G:A⟶C$$
55		elfzouz2	$$⊢n\in \left(M..^N\right)\to N\in {\mathbb{Z}}_{\ge n}$$
56	55	adantl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to N\in {\mathbb{Z}}_{\ge n}$$
57		fzss2	$$⊢N\in {\mathbb{Z}}_{\ge n}\to \left(M\dots n\right)\subseteq \left(M\dots N\right)$$
58	56 57	syl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(M\dots n\right)\subseteq \left(M\dots N\right)$$
59	8	adantr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(M\dots N\right)\subseteq A$$
60	58 59	sstrd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(M\dots n\right)\subseteq A$$
61	60	sselda	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge x\in \left(M\dots n\right)\right)\to x\in A$$
62	54 61	ffvelrnd	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge x\in \left(M\dots n\right)\right)\to G\left(x\right)\in C$$
63	52 62	sseldd	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge x\in \left(M\dots n\right)\right)\to G\left(x\right)\in S$$
64	1	adantlr	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
65	44 63 64	seqcl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\in S$$
66		fzofzp1	$$⊢n\in \left(M..^N\right)\to n+1\in \left(M\dots N\right)$$
67	66	adantl	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to n+1\in \left(M\dots N\right)$$
68	59 67	sseldd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to n+1\in A$$
69	53 68	ffvelrnd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(n+1\right)\in C$$
70	51 69	sseldd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(n+1\right)\in S$$
71	48 50 65 70	caovassd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\right)\underset{\dot{}}{+}G\left(n+1\right)=G\left(K\right)\underset{\dot{}}{+}\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)\right)$$
72	47 71	eqtr4d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=\left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\right)\underset{\dot{}}{+}G\left(n+1\right)$$
73	48 65 70 50	caovassd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)\right)\underset{\dot{}}{+}G\left(K\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}\left(G\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
74	46	oveq1d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)=\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(n+1\right)\right)\underset{\dot{}}{+}G\left(K\right)$$
75	48 65 50 70	caovassd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\underset{\dot{}}{+}G\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}\left(G\left(K\right)\underset{\dot{}}{+}G\left(n+1\right)\right)$$
76	2	adantlr	$$⊢\left(\left(\phi \wedge n\in \left(M..^N\right)\right)\wedge \left(x\in C\wedge y\in C\right)\right)\to x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
77	31	adantr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(K\right)\in C$$
78	76 69 77	caovcomd	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to G\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)=G\left(K\right)\underset{\dot{}}{+}G\left(n+1\right)$$
79	78	oveq2d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}\left(G\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}\left(G\left(K\right)\underset{\dot{}}{+}G\left(n+1\right)\right)$$
80	75 79	eqtr4d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\underset{\dot{}}{+}G\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}\left(G\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
81	73 74 80	3eqtr4d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)=\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\underset{\dot{}}{+}G\left(n+1\right)$$
82	72 81	eqeq12d	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\leftrightarrow \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\right)\underset{\dot{}}{+}G\left(n+1\right)=\left(seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\underset{\dot{}}{+}G\left(n+1\right)\right)$$
83	42 82	syl5ibr	$$⊢\left(\phi \wedge n\in \left(M..^N\right)\right)\to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
84	83	expcom	$$⊢n\in \left(M..^N\right)\to \left(\phi \to \left(G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
85	84	a2d	$$⊢n\in \left(M..^N\right)\to \left(\left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n\right)\underset{\dot{}}{+}G\left(K\right)\right)\to \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(n+1\right)\underset{\dot{}}{+}G\left(K\right)\right)\right)$$
86	15 20 25 30 41 85	fzind2	$$⊢N\in \left(M\dots N\right)\to \left(\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)\right)$$
87	10 86	mpcom	$$⊢\phi \to G\left(K\right)\underset{\dot{}}{+}seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)=seqM\left(\underset{\dot{}}{+},G\right)\left(N\right)\underset{\dot{}}{+}G\left(K\right)$$