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 = ( ZZ>= ` M ) |
|
seqp1iOLD.2 | |- N e. Z |
||
seqp1iOLD.3 | |- K = ( N + 1 ) |
||
seqp1iOLD.4 | |- ( ph -> ( seq M ( .+ , F ) ` N ) = A ) |
||
seqp1iOLD.5 | |- ( ph -> ( F ` K ) = B ) |
||
Assertion | seqp1iOLD | |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( A .+ B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | seqp1iOLD.1 | |- Z = ( ZZ>= ` M ) |
|
2 | seqp1iOLD.2 | |- N e. Z |
|
3 | seqp1iOLD.3 | |- K = ( N + 1 ) |
|
4 | seqp1iOLD.4 | |- ( ph -> ( seq M ( .+ , F ) ` N ) = A ) |
|
5 | seqp1iOLD.5 | |- ( ph -> ( F ` K ) = B ) |
|
6 | 2 | a1i | |- ( ph -> N e. Z ) |
7 | 1 6 3 4 5 | seqp1d | |- ( ph -> ( seq M ( .+ , F ) ` K ) = ( A .+ B ) ) |