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

Metamath Proof Explorer

Theorem seqp1d

Description: Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by AV, 3-May-2024)

Ref Expression
Hypotheses seqp1d.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
seqp1d.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
seqp1d.3 ⊢ 𝐾 = ( 𝑁 + 1 )
seqp1d.4 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
seqp1d.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
Assertion seqp1d ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 seqp1d.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 seqp1d.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 seqp1d.3 ⊢ 𝐾 = ( 𝑁 + 1 )
4 seqp1d.4 ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
5 seqp1d.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
6 3 fveq2i ⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) )
7 6 a1i ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
8 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
11 3 fveq2i ⊢ ( 𝐹 ‘ 𝐾 ) = ( 𝐹 ‘ ( 𝑁 + 1 ) )
12 11 5 eqtr3id ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = 𝐵 )
13 4 12 oveq12d ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐴 + 𝐵 ) )
14 7 10 13 3eqtrd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )