Theorem sumrblem

Description: Lemma for sumrb . (Contributed by Mario Carneiro, 12-Aug-2013)

	Ref	Expression
Hypotheses	summo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
	summo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	sumrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
Assertion	sumrblem	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		summo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2		summo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		sumrb.3	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4		addid2	⊢ ( 𝑛 ∈ ℂ → ( 0 + 𝑛 ) = 𝑛 )
5	4	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ℂ ) → ( 0 + 𝑛 ) = 𝑛 )
6		0cnd	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 0 ∈ ℂ )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
8		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 𝐵 )
10	9 2	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
11	10	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) )
12		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
13		0cn	⊢ 0 ∈ ℂ
14	12 13	eqeltrdi	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
15	11 14	pm2.61d1	⊢ ( 𝜑 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
17	16 1	fmptd	⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ℂ )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 𝐹 : ℤ ⟶ ℂ )
19		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
20	3 19	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
22	18 21	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
23		elfzelz	⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℤ )
24	23	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ℤ )
25		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
26	20	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
27	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
28		ax-1cn	⊢ 1 ∈ ℂ
29		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
30	27 28 29	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
31	30	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝑁 ) )
32	25 31	sseqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ⊆ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
33		fznuz	⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → ¬ 𝑛 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
34	33	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
35	32 34	ssneldd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ¬ 𝑛 ∈ 𝐴 )
36	24 35	eldifd	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑛 ∈ ( ℤ ∖ 𝐴 ) )
37		fveqeq2	⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) = 0 ↔ ( 𝐹 ‘ 𝑛 ) = 0 ) )
38		eldifi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → 𝑘 ∈ ℤ )
39		eldifn	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ¬ 𝑘 ∈ 𝐴 )
40	39 12	syl	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) = 0 )
41	40 13	eqeltrdi	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ )
42	1	fvmpt2	⊢ ( ( 𝑘 ∈ ℤ ∧ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
43	38 41 42	syl2anc	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
44	43 40	eqtrd	⊢ ( 𝑘 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 0 )
45	37 44	vtoclga	⊢ ( 𝑛 ∈ ( ℤ ∖ 𝐴 ) → ( 𝐹 ‘ 𝑛 ) = 0 )
46	36 45	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) = 0 )
47	5 6 7 22 46	seqid	⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )