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	$$⊢\phi \to Z\underset{\dot{}}{+}Z=Z$$
	seqid3.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	seqid3.3	$$⊢\left(\phi \wedge x\in \left(M\dots N\right)\right)\to F\left(x\right)=Z$$
Assertion	seqid3	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=Z$$

Proof

Step	Hyp	Ref	Expression
1		seqid3.1	$$⊢\phi \to Z\underset{\dot{}}{+}Z=Z$$
2		seqid3.2	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
3		seqid3.3	$$⊢\left(\phi \wedge x\in \left(M\dots N\right)\right)\to F\left(x\right)=Z$$
4		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
5	4	elsn	$$⊢F\left(x\right)\in \left\{Z\right\}\leftrightarrow F\left(x\right)=Z$$
6	3 5	sylibr	$$⊢\left(\phi \wedge x\in \left(M\dots N\right)\right)\to F\left(x\right)\in \left\{Z\right\}$$
7		ovex	$$⊢Z\underset{\dot{}}{+}Z\in \mathrm{V}$$
8	7	elsn	$$⊢Z\underset{\dot{}}{+}Z\in \left\{Z\right\}\leftrightarrow Z\underset{\dot{}}{+}Z=Z$$
9	1 8	sylibr	$$⊢\phi \to Z\underset{\dot{}}{+}Z\in \left\{Z\right\}$$
10		elsni	$$⊢x\in \left\{Z\right\}\to x=Z$$
11		elsni	$$⊢y\in \left\{Z\right\}\to y=Z$$
12	10 11	oveqan12d	$$⊢\left(x\in \left\{Z\right\}\wedge y\in \left\{Z\right\}\right)\to x\underset{\dot{}}{+}y=Z\underset{\dot{}}{+}Z$$
13	12	eleq1d	$$⊢\left(x\in \left\{Z\right\}\wedge y\in \left\{Z\right\}\right)\to \left(x\underset{\dot{}}{+}y\in \left\{Z\right\}\leftrightarrow Z\underset{\dot{}}{+}Z\in \left\{Z\right\}\right)$$
14	9 13	syl5ibrcom	$$⊢\phi \to \left(\left(x\in \left\{Z\right\}\wedge y\in \left\{Z\right\}\right)\to x\underset{\dot{}}{+}y\in \left\{Z\right\}\right)$$
15	14	imp	$$⊢\left(\phi \wedge \left(x\in \left\{Z\right\}\wedge y\in \left\{Z\right\}\right)\right)\to x\underset{\dot{}}{+}y\in \left\{Z\right\}$$
16	2 6 15	seqcl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\in \left\{Z\right\}$$
17		elsni	$$⊢seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)\in \left\{Z\right\}\to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=Z$$
18	16 17	syl	$$⊢\phi \to seqM\left(\underset{\dot{}}{+},F\right)\left(N\right)=Z$$