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 )