This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ( + , 𝐹 ) ‘ 𝑁 ) ) )