Theorem seqsplit

Description: Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	seqsplit.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
	seqsplit.2	$$⊢\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)$$
	seqsplit.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left(M+1\right)}$$
	seqsplit.4	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge K}$$
	seqsplit.5	$$⊢\left(\phi \wedge x\in \left(K\dots N\right)\right)\to F\left(x\right)\in S$$
Assertion	seqsplit	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		seqsplit.1	$$⊢\left(\phi \wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
2		seqsplit.2	$$⊢\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)$$
3		seqsplit.3	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left(M+1\right)}$$
4		seqsplit.4	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge K}$$
5		seqsplit.5	$$⊢\left(\phi \wedge x\in \left(K\dots N\right)\right)\to F\left(x\right)\in S$$
6		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to N\in \left(M+1\dots N\right)$$
7	3 6	syl	$$⊢\phi \to N\in \left(M+1\dots N\right)$$
8		eleq1	$$⊢x=M+1\to \left(x\in \left(M+1\dots N\right)\leftrightarrow M+1\in \left(M+1\dots N\right)\right)$$
9		fveq2	$$⊢x=M+1\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)$$
10		fveq2	$$⊢x=M+1\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)$$
11	10	oveq2d	$$⊢x=M+1\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)$$
12	9 11	eqeq12d	$$⊢x=M+1\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\leftrightarrow seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)\right)$$
13	8 12	imbi12d	$$⊢x=M+1\to \left(\left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\leftrightarrow \left(M+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)\right)\right)$$
14	13	imbi2d	$$⊢x=M+1\to \left(\left(\phi \to \left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\right)\leftrightarrow \left(\phi \to \left(M+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)\right)\right)\right)$$
15		eleq1	$$⊢x=n\to \left(x\in \left(M+1\dots N\right)\leftrightarrow n\in \left(M+1\dots N\right)\right)$$
16		fveq2	$$⊢x=n\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)$$
17		fveq2	$$⊢x=n\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)$$
18	17	oveq2d	$$⊢x=n\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)$$
19	16 18	eqeq12d	$$⊢x=n\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\leftrightarrow seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)$$
20	15 19	imbi12d	$$⊢x=n\to \left(\left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\leftrightarrow \left(n\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right)$$
21	20	imbi2d	$$⊢x=n\to \left(\left(\phi \to \left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\right)\leftrightarrow \left(\phi \to \left(n\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right)\right)$$
22		eleq1	$$⊢x=n+1\to \left(x\in \left(M+1\dots N\right)\leftrightarrow n+1\in \left(M+1\dots N\right)\right)$$
23		fveq2	$$⊢x=n+1\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)$$
24		fveq2	$$⊢x=n+1\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)$$
25	24	oveq2d	$$⊢x=n+1\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)$$
26	23 25	eqeq12d	$$⊢x=n+1\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\leftrightarrow seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\right)$$
27	22 26	imbi12d	$$⊢x=n+1\to \left(\left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\leftrightarrow \left(n+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\right)\right)$$
28	27	imbi2d	$$⊢x=n+1\to \left(\left(\phi \to \left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\right)\leftrightarrow \left(\phi \to \left(n+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\right)\right)\right)$$
29		eleq1	$$⊢x=N\to \left(x\in \left(M+1\dots N\right)\leftrightarrow N\in \left(M+1\dots N\right)\right)$$
30		fveq2	$$⊢x=N\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)$$
31		fveq2	$$⊢x=N\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)$$
32	31	oveq2d	$$⊢x=N\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)$$
33	30 32	eqeq12d	$$⊢x=N\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\leftrightarrow seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)\right)$$
34	29 33	imbi12d	$$⊢x=N\to \left(\left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\leftrightarrow \left(N\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)\right)\right)$$
35	34	imbi2d	$$⊢x=N\to \left(\left(\phi \to \left(x\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(x\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(x\right)\right)\right)\leftrightarrow \left(\phi \to \left(N\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)\right)\right)\right)$$
36		seqp1	$$⊢M\in {\mathbb{Z}}_{\ge K}\to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)$$
37	4 36	syl	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)$$
38		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to M+1\in \mathbb{Z}$$
39		seq1	$$⊢M+1\in \mathbb{Z}\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=F\left(M+1\right)$$
40	3 38 39	3syl	$$⊢\phi \to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=F\left(M+1\right)$$
41	40	oveq2d	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}F\left(M+1\right)$$
42	37 41	eqtr4d	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)$$
43	42	a1i13	$$⊢M+1\in \mathbb{Z}\to \left(\phi \to \left(M+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(M+1\right)\right)\right)$$
44		peano2fzr	$$⊢\left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\to n\in \left(M+1\dots N\right)$$
45	44	adantl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to n\in \left(M+1\dots N\right)$$
46	45	expr	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to \left(n+1\in \left(M+1\dots N\right)\to n\in \left(M+1\dots N\right)\right)$$
47	46	imim1d	$$⊢\left(\phi \wedge n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to \left(\left(n\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\to \left(n+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right)$$
48		oveq1	$$⊢seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)=\left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\underset{\dot{}}{+}F\left(n+1\right)$$
49		simprl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to n\in {\mathbb{Z}}_{\ge \left(M+1\right)}$$
50		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge K}\to M+1\in {\mathbb{Z}}_{\ge K}$$
51	4 50	syl	$$⊢\phi \to M+1\in {\mathbb{Z}}_{\ge K}$$
52	51	adantr	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to M+1\in {\mathbb{Z}}_{\ge K}$$
53		uztrn	$$⊢\left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge M+1\in {\mathbb{Z}}_{\ge K}\right)\to n\in {\mathbb{Z}}_{\ge K}$$
54	49 52 53	syl2anc	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to n\in {\mathbb{Z}}_{\ge K}$$
55		seqp1	$$⊢n\in {\mathbb{Z}}_{\ge K}\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)$$
56	54 55	syl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)$$
57		seqp1	$$⊢n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)$$
58	49 57	syl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)$$
59	58	oveq2d	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}\left(seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)\right)$$
60		simpl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \phi$$
61		eluzelz	$$⊢M\in {\mathbb{Z}}_{\ge K}\to M\in \mathbb{Z}$$
62	4 61	syl	$$⊢\phi \to M\in \mathbb{Z}$$
63		peano2uzr	$$⊢\left(M\in \mathbb{Z}\wedge N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to N\in {\mathbb{Z}}_{\ge M}$$
64	62 3 63	syl2anc	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
65		fzss2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(K\dots M\right)\subseteq \left(K\dots N\right)$$
66	64 65	syl	$$⊢\phi \to \left(K\dots M\right)\subseteq \left(K\dots N\right)$$
67	66	sselda	$$⊢\left(\phi \wedge x\in \left(K\dots M\right)\right)\to x\in \left(K\dots N\right)$$
68	67 5	syldan	$$⊢\left(\phi \wedge x\in \left(K\dots M\right)\right)\to F\left(x\right)\in S$$
69	4 68 1	seqcl	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\in S$$
70	69	adantr	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\in S$$
71		elfzuz3	$$⊢n\in \left(M+1\dots N\right)\to N\in {\mathbb{Z}}_{\ge n}$$
72		fzss2	$$⊢N\in {\mathbb{Z}}_{\ge n}\to \left(M+1\dots n\right)\subseteq \left(M+1\dots N\right)$$
73	45 71 72	3syl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(M+1\dots n\right)\subseteq \left(M+1\dots N\right)$$
74		fzss1	$$⊢M+1\in {\mathbb{Z}}_{\ge K}\to \left(M+1\dots N\right)\subseteq \left(K\dots N\right)$$
75	4 50 74	3syl	$$⊢\phi \to \left(M+1\dots N\right)\subseteq \left(K\dots N\right)$$
76	75	adantr	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(M+1\dots N\right)\subseteq \left(K\dots N\right)$$
77	73 76	sstrd	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(M+1\dots n\right)\subseteq \left(K\dots N\right)$$
78	77	sselda	$$⊢\left(\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\wedge x\in \left(M+1\dots n\right)\right)\to x\in \left(K\dots N\right)$$
79	5	adantlr	$$⊢\left(\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\wedge x\in \left(K\dots N\right)\right)\to F\left(x\right)\in S$$
80	78 79	syldan	$$⊢\left(\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\wedge x\in \left(M+1\dots n\right)\right)\to F\left(x\right)\in S$$
81	1	adantlr	$$⊢\left(\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to x\underset{\dot{}}{+}y\in S$$
82	49 80 81	seqcl	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\in S$$
83		fveq2	$$⊢x=n+1\to F\left(x\right)=F\left(n+1\right)$$
84	83	eleq1d	$$⊢x=n+1\to \left(F\left(x\right)\in S\leftrightarrow F\left(n+1\right)\in S\right)$$
85	5	ralrimiva	$$⊢\phi \to \forall x\in \left(K\dots N\right)F\left(x\right)\in S$$
86	85	adantr	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \forall x\in \left(K\dots N\right)F\left(x\right)\in S$$
87		simpr	$$⊢\left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\to n+1\in \left(M+1\dots N\right)$$
88		ssel2	$$⊢\left(\left(M+1\dots N\right)\subseteq \left(K\dots N\right)\wedge n+1\in \left(M+1\dots N\right)\right)\to n+1\in \left(K\dots N\right)$$
89	75 87 88	syl2an	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to n+1\in \left(K\dots N\right)$$
90	84 86 89	rspcdva	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to F\left(n+1\right)\in S$$
91	2	caovassg	$$⊢\left(\phi \wedge \left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\in S\wedge seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\in S\wedge F\left(n+1\right)\in S\right)\right)\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\underset{\dot{}}{+}F\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}\left(seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)\right)$$
92	60 70 82 90 91	syl13anc	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\underset{\dot{}}{+}F\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}\left(seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)\right)$$
93	59 92	eqtr4d	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=\left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\underset{\dot{}}{+}F\left(n+1\right)$$
94	56 93	eqeq12d	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\leftrightarrow seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)\underset{\dot{}}{+}F\left(n+1\right)=\left(seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\underset{\dot{}}{+}F\left(n+1\right)\right)$$
95	48 94	imbitrrid	$$⊢\left(\phi \wedge \left(n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\wedge n+1\in \left(M+1\dots N\right)\right)\right)\to \left(seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\right)$$
96	47 95	animpimp2impd	$$⊢n\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to \left(\left(\phi \to \left(n\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n\right)\right)\right)\to \left(\phi \to \left(n+1\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(n+1\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(n+1\right)\right)\right)\right)$$
97	14 21 28 35 43 96	uzind4	$$⊢N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\to \left(\phi \to \left(N\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)\right)\right)$$
98	3 97	mpcom	$$⊢\phi \to \left(N\in \left(M+1\dots N\right)\to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)\right)$$
99	7 98	mpd	$$⊢\phi \to seqK\left(\underset{\dot{}}{+},F\right)\left(N\right)=seqK\left(\underset{\dot{}}{+},F\right)\left(M\right)\underset{\dot{}}{+}seq\left(M+1\right)\left(\underset{\dot{}}{+},F\right)\left(N\right)$$