Theorem 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	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
	seqsplit.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
	seqsplit.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
	seq1p.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	seq1p.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
Assertion	seq1p	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		seqsplit.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
2		seqsplit.2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
3		seqsplit.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
4		seq1p.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		seq1p.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑆 )
6		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7	4 6	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8	1 2 3 7 5	seqsplit	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )
9		seq1	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
10	4 9	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
11	10	oveq1d	⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( 𝐹 ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )
12	8 11	eqtrd	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( 𝐹 ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )