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
⊢ Z = ℤ ≥ M
seqp1iOLD.2
⊢ N ∈ Z
seqp1iOLD.3
⊢ K = N + 1
seqp1iOLD.4
⊢ φ → seq M + ˙ F ⁡ N = A
seqp1iOLD.5
⊢ φ → F ⁡ K = B
Assertion
seqp1iOLD
⊢ φ → seq M + ˙ F ⁡ K = A + ˙ B
Proof
Step
Hyp
Ref
Expression
1
seqp1iOLD.1
⊢ Z = ℤ ≥ M
2
seqp1iOLD.2
⊢ N ∈ Z
3
seqp1iOLD.3
⊢ K = N + 1
4
seqp1iOLD.4
⊢ φ → seq M + ˙ F ⁡ N = A
5
seqp1iOLD.5
⊢ φ → F ⁡ K = B
6
2
a1i
⊢ φ → N ∈ Z
7
1 6 3 4 5
seqp1d
⊢ φ → seq M + ˙ F ⁡ K = A + ˙ B