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	⊢ ( 𝜑 → ( 𝑍 + 𝑍 ) = 𝑍 )
	seqid3.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	seqid3.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
Assertion	seqid3	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		seqid3.1	⊢ ( 𝜑 → ( 𝑍 + 𝑍 ) = 𝑍 )
2		seqid3.2	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3		seqid3.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑍 )
4		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
5	4	elsn	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
6	3 5	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } )
7		ovex	⊢ ( 𝑍 + 𝑍 ) ∈ V
8	7	elsn	⊢ ( ( 𝑍 + 𝑍 ) ∈ { 𝑍 } ↔ ( 𝑍 + 𝑍 ) = 𝑍 )
9	1 8	sylibr	⊢ ( 𝜑 → ( 𝑍 + 𝑍 ) ∈ { 𝑍 } )
10		elsni	⊢ ( 𝑥 ∈ { 𝑍 } → 𝑥 = 𝑍 )
11		elsni	⊢ ( 𝑦 ∈ { 𝑍 } → 𝑦 = 𝑍 )
12	10 11	oveqan12d	⊢ ( ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ { 𝑍 } ) → ( 𝑥 + 𝑦 ) = ( 𝑍 + 𝑍 ) )
13	12	eleq1d	⊢ ( ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ { 𝑍 } ) → ( ( 𝑥 + 𝑦 ) ∈ { 𝑍 } ↔ ( 𝑍 + 𝑍 ) ∈ { 𝑍 } ) )
14	9 13	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ { 𝑍 } ) → ( 𝑥 + 𝑦 ) ∈ { 𝑍 } ) )
15	14	imp	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝑍 } ∧ 𝑦 ∈ { 𝑍 } ) ) → ( 𝑥 + 𝑦 ) ∈ { 𝑍 } )
16	2 6 15	seqcl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑍 } )
17		elsni	⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑍 } → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )
18	16 17	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )