Metamath Proof Explorer

Theorem sumrb

Description: Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 9-Apr-2014)

Ref Expression
Hypotheses summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
sumrb.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sumrb.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
sumrb.6 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
sumrb.7 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
Assertion sumrb ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 summo.1 ⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 0 ) )
2 summo.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 sumrb.4 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 sumrb.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5 sumrb.6 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
6 sumrb.7 ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) )
7 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
8 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
9 climres ⊢ ( ( 𝑁 ∈ ℤ ∧ seq 𝑀 ( + , 𝐹 ) ∈ V ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ) )
10 7 8 9 sylancl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ) )
11 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
13 1 11 12 sumrblem ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )
14 6 13 mpidan ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )
15 14 breq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑁 ) ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )
16 10 15 bitr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )
17 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
19 1 17 18 sumrblem ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑁 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑀 ) ) = seq 𝑀 ( + , 𝐹 ) )
20 5 19 mpidan ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑁 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑀 ) ) = seq 𝑀 ( + , 𝐹 ) )
21 20 breq1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( seq 𝑁 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐶 ↔ seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ) )
22 3 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
23 seqex ⊢ seq 𝑁 ( + , 𝐹 ) ∈ V
24 climres ⊢ ( ( 𝑀 ∈ ℤ ∧ seq 𝑁 ( + , 𝐹 ) ∈ V ) → ( ( seq 𝑁 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )
25 22 23 24 sylancl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( seq 𝑁 ( + , 𝐹 ) ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )
26 21 25 bitr3d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )
27 uztric ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
28 3 4 27 syl2anc ⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
29 16 26 28 mpjaodan ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ⇝ 𝐶 ↔ seq 𝑁 ( + , 𝐹 ) ⇝ 𝐶 ) )