Metamath Proof Explorer

Theorem seqfeq3

Description: Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 25-Apr-2016)

Ref Expression
Hypotheses seqfeq3.m 
|- ( ph -> M e. ZZ )
seqfeq3.f 
|- ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )
seqfeq3.cl 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqfeq3.id 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )
Assertion seqfeq3 
|- ( ph -> seq M ( .+ , F ) = seq M ( Q , F ) )

Proof

Step Hyp Ref Expression
1 seqfeq3.m 
 |-  ( ph -> M e. ZZ )
2 seqfeq3.f 
 |-  ( ( ph /\ x e. ( ZZ>= ` M ) ) -> ( F ` x ) e. S )
3 seqfeq3.cl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
4 seqfeq3.id 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )
5 seqfn 
 |-  ( M e. ZZ -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
6 1 5 syl 
 |-  ( ph -> seq M ( .+ , F ) Fn ( ZZ>= ` M ) )
7 seqfn 
 |-  ( M e. ZZ -> seq M ( Q , F ) Fn ( ZZ>= ` M ) )
8 1 7 syl 
 |-  ( ph -> seq M ( Q , F ) Fn ( ZZ>= ` M ) )
9 simpr 
 |-  ( ( ph /\ a e. ( ZZ>= ` M ) ) -> a e. ( ZZ>= ` M ) )
10 simpll 
 |-  ( ( ( ph /\ a e. ( ZZ>= ` M ) ) /\ x e. ( M ... a ) ) -> ph )
11 elfzuz 
 |-  ( x e. ( M ... a ) -> x e. ( ZZ>= ` M ) )
12 11 adantl 
 |-  ( ( ( ph /\ a e. ( ZZ>= ` M ) ) /\ x e. ( M ... a ) ) -> x e. ( ZZ>= ` M ) )
13 10 12 2 syl2anc 
 |-  ( ( ( ph /\ a e. ( ZZ>= ` M ) ) /\ x e. ( M ... a ) ) -> ( F ` x ) e. S )
14 3 adantlr 
 |-  ( ( ( ph /\ a e. ( ZZ>= ` M ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
15 4 adantlr 
 |-  ( ( ( ph /\ a e. ( ZZ>= ` M ) ) /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) = ( x Q y ) )
16 9 13 14 15 seqfeq4 
 |-  ( ( ph /\ a e. ( ZZ>= ` M ) ) -> ( seq M ( .+ , F ) ` a ) = ( seq M ( Q , F ) ` a ) )
17 6 8 16 eqfnfvd 
 |-  ( ph -> seq M ( .+ , F ) = seq M ( Q , F ) )