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

Metamath Proof Explorer

Theorem seqm1

Description: Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Assertion seqm1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
2 seqp1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) )
3 1 2 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) )
4 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → 𝑁 ∈ ℂ )
5 ax-1cn ⊢ 1 ∈ ℂ
6 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7 4 5 6 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
8 7 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
9 8 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
10 8 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐹 ‘ 𝑁 ) )
11 10 oveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ ( ( 𝑁 − 1 ) + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ 𝑁 ) ) )
12 3 9 11 3eqtr3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹 ‘ 𝑁 ) ) )