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 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )