Metamath Proof Explorer

Theorem seqfeq3

Description: Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 25-Apr-2016)

		Ref	Expression
	Hypotheses	seqfeq3.m	$⊢ φ \to M \in ℤ$
		seqfeq3.f	$⊢ (φ \land x \in ℤ_{\geq M}) \to F (x) \in S$
		seqfeq3.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
		seqfeq3.id	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x Q y$
	Assertion	seqfeq3	$⊢ φ \to seq M (\underset{˙}{+}, F) = seq M (Q, F)$

Proof

Step	Hyp	Ref	Expression
1		seqfeq3.m	$⊢ φ \to M \in ℤ$
2		seqfeq3.f	$⊢ (φ \land x \in ℤ_{\geq M}) \to F (x) \in S$
3		seqfeq3.cl	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
4		seqfeq3.id	$⊢ (φ \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x Q y$
5		seqfn	$⊢ M \in ℤ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
6	1 5	syl	$⊢ φ \to seq M (\underset{˙}{+}, F) Fn ℤ_{\geq M}$
7		seqfn	$⊢ M \in ℤ \to seq M (Q, F) Fn ℤ_{\geq M}$
8	1 7	syl	$⊢ φ \to seq M (Q, F) Fn ℤ_{\geq M}$
9		simpr	$⊢ (φ \land a \in ℤ_{\geq M}) \to a \in ℤ_{\geq M}$
10		simpll	$⊢ ((φ \land a \in ℤ_{\geq M}) \land x \in (M \dots a)) \to φ$
11		elfzuz	$⊢ x \in (M \dots a) \to x \in ℤ_{\geq M}$
12	11	adantl	$⊢ ((φ \land a \in ℤ_{\geq M}) \land x \in (M \dots a)) \to x \in ℤ_{\geq M}$
13	10 12 2	syl2anc	$⊢ ((φ \land a \in ℤ_{\geq M}) \land x \in (M \dots a)) \to F (x) \in S$
14	3	adantlr	$⊢ ((φ \land a \in ℤ_{\geq M}) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
15	4	adantlr	$⊢ ((φ \land a \in ℤ_{\geq M}) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x Q y$
16	9 13 14 15	seqfeq4	$⊢ (φ \land a \in ℤ_{\geq M}) \to seq M (\underset{˙}{+}, F) (a) = seq M (Q, F) (a)$
17	6 8 16	eqfnfvd	$⊢ φ \to seq M (\underset{˙}{+}, F) = seq M (Q, F)$