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	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
	seqsplit.2	$⊢ (φ \land (x \in S \land y \in S \land z \in S)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
	seqsplit.3	$⊢ φ \to N \in ℤ_{\geq (M + 1)}$
	seqsplit.4	$⊢ φ \to M \in ℤ_{\geq K}$
	seqsplit.5	$⊢ (φ \land x \in (K \dots N)) \to F (x) \in S$
Assertion	seqsplit	$⊢ φ \to seq K (\underset{˙}{+}, F) (N) = seq K (\underset{˙}{+}, F) (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N)$

Proof

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

Metamath Proof Explorer

Theorem seqsplit

Proof