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 ⊢ ( 𝜑 → ( 𝑍 + 𝑍 ) = 𝑍 )
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 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = 𝑍 )