sumrblem

	Ref	Expression
Hypotheses	summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
	summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	sumrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
Assertion	sumrblem	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to {seq M (+ F) ↾}_{ℤ_{\geq N}} = seq N (+ F)$

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		sumrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		addid2	$⊢ n \in ℂ \to 0 + n = n$
5	4	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in ℂ) \to 0 + n = n$
6		0cnd	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to 0 \in ℂ$
7	3	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to N \in ℤ_{\geq M}$
8		iftrue	$⊢ k \in A \to if (k \in A, B, 0) = B$
9	8	adantl	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) = B$
10	9 2	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, B, 0) \in ℂ$
11	10	ex	$⊢ φ \to (k \in A \to if (k \in A, B, 0) \in ℂ)$
12		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 0) = 0$
13		0cn	$⊢ 0 \in ℂ$
14	12 13	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 0) \in ℂ$
15	11 14	pm2.61d1	$⊢ φ \to if (k \in A, B, 0) \in ℂ$
16	15	adantr	$⊢ (φ \land k \in ℤ) \to if (k \in A, B, 0) \in ℂ$
17	16 1	fmptd	$⊢ φ \to F : ℤ ⟶ ℂ$
18	17	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to F : ℤ ⟶ ℂ$
19		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
20	3 19	syl	$⊢ φ \to N \in ℤ$
21	20	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to N \in ℤ$
22	18 21	ffvelrnd	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to F (N) \in ℂ$
23		elfzelz	$⊢ n \in (M \dots N - 1) \to n \in ℤ$
24	23	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to n \in ℤ$
25		simplr	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to A \subseteq ℤ_{\geq N}$
26	20	zcnd	$⊢ φ \to N \in ℂ$
27	26	ad2antrr	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to N \in ℂ$
28		ax-1cn	$⊢ 1 \in ℂ$
29		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
30	27 28 29	sylancl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to N - 1 + 1 = N$
31	30	fveq2d	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to ℤ_{\geq (N - 1 + 1)} = ℤ_{\geq N}$
32	25 31	sseqtrrd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to A \subseteq ℤ_{\geq (N - 1 + 1)}$
33		fznuz	$⊢ n \in (M \dots N - 1) \to \neg n \in ℤ_{\geq (N - 1 + 1)}$
34	33	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to \neg n \in ℤ_{\geq (N - 1 + 1)}$
35	32 34	ssneldd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to \neg n \in A$
36	24 35	eldifd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to n \in (ℤ ∖ A)$
37		fveqeq2	$⊢ k = n \to (F (k) = 0 \leftrightarrow F (n) = 0)$
38		eldifi	$⊢ k \in (ℤ ∖ A) \to k \in ℤ$
39		eldifn	$⊢ k \in (ℤ ∖ A) \to \neg k \in A$
40	39 12	syl	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 0) = 0$
41	40 13	eqeltrdi	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 0) \in ℂ$
42	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 0) \in ℂ) \to F (k) = if (k \in A, B, 0)$
43	38 41 42	syl2anc	$⊢ k \in (ℤ ∖ A) \to F (k) = if (k \in A, B, 0)$
44	43 40	eqtrd	$⊢ k \in (ℤ ∖ A) \to F (k) = 0$
45	37 44	vtoclga	$⊢ n \in (ℤ ∖ A) \to F (n) = 0$
46	36 45	syl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to F (n) = 0$
47	5 6 7 22 46	seqid	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to {seq M (+ F) ↾}_{ℤ_{\geq N}} = seq N (+ F)$

Metamath Proof Explorer

Theorem sumrblem

Proof