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 ⊢ φ → Z + ˙ Z = Z
seqid3.2 ⊢ φ → N ∈ ℤ ≥ M
seqid3.3 ⊢ φ ∧ x ∈ M … N → F ⁡ x = Z
Assertion seqid3 ⊢ φ → seq M + ˙ F ⁡ N = Z

Proof

Step Hyp Ref Expression
1 seqid3.1 ⊢ φ → Z + ˙ Z = Z
2 seqid3.2 ⊢ φ → N ∈ ℤ ≥ M
3 seqid3.3 ⊢ φ ∧ x ∈ M … N → F ⁡ x = Z
4 fvex ⊢ F ⁡ x ∈ V
5 4 elsn ⊢ F ⁡ x ∈ Z ↔ F ⁡ x = Z
6 3 5 sylibr ⊢ φ ∧ x ∈ M … N → F ⁡ x ∈ Z
7 ovex ⊢ Z + ˙ Z ∈ V
8 7 elsn ⊢ Z + ˙ Z ∈ Z ↔ Z + ˙ Z = Z
9 1 8 sylibr ⊢ φ → Z + ˙ Z ∈ Z
10 elsni ⊢ x ∈ Z → x = Z
11 elsni ⊢ y ∈ Z → y = Z
12 10 11 oveqan12d ⊢ x ∈ Z ∧ y ∈ Z → x + ˙ y = Z + ˙ Z
13 12 eleq1d ⊢ x ∈ Z ∧ y ∈ Z → x + ˙ y ∈ Z ↔ Z + ˙ Z ∈ Z
14 9 13 syl5ibrcom ⊢ φ → x ∈ Z ∧ y ∈ Z → x + ˙ y ∈ Z
15 14 imp ⊢ φ ∧ x ∈ Z ∧ y ∈ Z → x + ˙ y ∈ Z
16 2 6 15 seqcl ⊢ φ → seq M + ˙ F ⁡ N ∈ Z
17 elsni ⊢ seq M + ˙ F ⁡ N ∈ Z → seq M + ˙ F ⁡ N = Z
18 16 17 syl ⊢ φ → seq M + ˙ F ⁡ N = Z