This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 addlid ⊢ ( 𝑛 ∈ ℂ → ( 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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
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 𝑁 ( + , 𝐹 ) )