Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The infinite sequence builder "seq" - extension
seqp1iOLD
Metamath Proof Explorer
Description: Obsolete version of seqp1d as of 3-May-2024. Value of the sequence
builder function at a successor. (Contributed by Mario Carneiro , 30-Apr-2014) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
seqp1iOLD.1
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
seqp1iOLD.2
⊢ 𝑁 ∈ 𝑍
seqp1iOLD.3
⊢ 𝐾 = ( 𝑁 + 1 )
seqp1iOLD.4
⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
seqp1iOLD.5
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
Assertion
seqp1iOLD
⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
seqp1iOLD.1
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2
seqp1iOLD.2
⊢ 𝑁 ∈ 𝑍
3
seqp1iOLD.3
⊢ 𝐾 = ( 𝑁 + 1 )
4
seqp1iOLD.4
⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝐴 )
5
seqp1iOLD.5
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐾 ) = 𝐵 )
6
2
a1i
⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
7
1 6 3 4 5
seqp1d
⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝐾 ) = ( 𝐴 + 𝐵 ) )