This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem seqid3

Description: A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a .+ -idempotent sums (or " .+ 's") to that element. (Contributed by Mario Carneiro, 15-Dec-2014)

Ref Expression
Hypotheses seqid3.1 
|- ( ph -> ( Z .+ Z ) = Z )
seqid3.2 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqid3.3 
|- ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = Z )
Assertion seqid3 
|- ( ph -> ( seq M ( .+ , F ) ` N ) = Z )

Proof

Step Hyp Ref Expression
1 seqid3.1 
 |-  ( ph -> ( Z .+ Z ) = Z )
2 seqid3.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 seqid3.3 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) = Z )
4 fvex 
 |-  ( F ` x ) e. _V
5 4 elsn 
 |-  ( ( F ` x ) e. { Z } <-> ( F ` x ) = Z )
6 3 5 sylibr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( F ` x ) e. { Z } )
7 ovex 
 |-  ( Z .+ Z ) e. _V
8 7 elsn 
 |-  ( ( Z .+ Z ) e. { Z } <-> ( Z .+ Z ) = Z )
9 1 8 sylibr 
 |-  ( ph -> ( Z .+ Z ) e. { Z } )
10 elsni 
 |-  ( x e. { Z } -> x = Z )
11 elsni 
 |-  ( y e. { Z } -> y = Z )
12 10 11 oveqan12d 
 |-  ( ( x e. { Z } /\ y e. { Z } ) -> ( x .+ y ) = ( Z .+ Z ) )
13 12 eleq1d 
 |-  ( ( x e. { Z } /\ y e. { Z } ) -> ( ( x .+ y ) e. { Z } <-> ( Z .+ Z ) e. { Z } ) )
14 9 13 syl5ibrcom 
 |-  ( ph -> ( ( x e. { Z } /\ y e. { Z } ) -> ( x .+ y ) e. { Z } ) )
15 14 imp 
 |-  ( ( ph /\ ( x e. { Z } /\ y e. { Z } ) ) -> ( x .+ y ) e. { Z } )
16 2 6 15 seqcl 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) e. { Z } )
17 elsni 
 |-  ( ( seq M ( .+ , F ) ` N ) e. { Z } -> ( seq M ( .+ , F ) ` N ) = Z )
18 16 17 syl 
 |-  ( ph -> ( seq M ( .+ , F ) ` N ) = Z )