seq1p

Description: Removing the first term from a sequence. (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)}$
	seq1p.4	$⊢ φ \to M \in ℤ$
	seq1p.5	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
Assertion	seq1p	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = F (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N)$

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		seq1p.4	$⊢ φ \to M \in ℤ$
5		seq1p.5	$⊢ (φ \land x \in (M \dots N)) \to F (x) \in S$
6		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
7	4 6	syl	$⊢ φ \to M \in ℤ_{\geq M}$
8	1 2 3 7 5	seqsplit	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = seq M (\underset{˙}{+}, F) (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N)$
9		seq1	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
10	4 9	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) = F (M)$
11	10	oveq1d	$⊢ φ \to seq M (\underset{˙}{+}, F) (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N) = F (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N)$
12	8 11	eqtrd	$⊢ φ \to seq M (\underset{˙}{+}, F) (N) = F (M) \underset{˙}{+} seq (M + 1) (\underset{˙}{+}, F) (N)$

Metamath Proof Explorer