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 
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
sumrb.4 
|- ( ph -> M e. ZZ )
sumrb.5 
|- ( ph -> N e. ZZ )
sumrb.6 
|- ( ph -> A C_ ( ZZ>= ` M ) )
sumrb.7 
|- ( ph -> A C_ ( ZZ>= ` N ) )
Assertion sumrb 
|- ( ph -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )

Proof

Step Hyp Ref Expression
1 summo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2 summo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 sumrb.4 
 |-  ( ph -> M e. ZZ )
4 sumrb.5 
 |-  ( ph -> N e. ZZ )
5 sumrb.6 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
6 sumrb.7 
 |-  ( ph -> A C_ ( ZZ>= ` N ) )
7 4 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. ZZ )
8 seqex 
 |-  seq M ( + , F ) e. _V
9 climres 
 |-  ( ( N e. ZZ /\ seq M ( + , F ) e. _V ) -> ( ( seq M ( + , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq M ( + , F ) ~~> C ) )
10 7 8 9 sylancl 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( seq M ( + , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq M ( + , F ) ~~> C ) )
11 2 adantlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` M ) ) /\ k e. A ) -> B e. CC )
12 simpr 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. ( ZZ>= ` M ) )
13 1 11 12 sumrblem 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` M ) ) /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )
14 6 13 mpidan 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )
15 14 breq1d 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( seq M ( + , F ) |` ( ZZ>= ` N ) ) ~~> C <-> seq N ( + , F ) ~~> C ) )
16 10 15 bitr3d 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )
17 2 adantlr 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` N ) ) /\ k e. A ) -> B e. CC )
18 simpr 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> M e. ( ZZ>= ` N ) )
19 1 17 18 sumrblem 
 |-  ( ( ( ph /\ M e. ( ZZ>= ` N ) ) /\ A C_ ( ZZ>= ` M ) ) -> ( seq N ( + , F ) |` ( ZZ>= ` M ) ) = seq M ( + , F ) )
20 5 19 mpidan 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( seq N ( + , F ) |` ( ZZ>= ` M ) ) = seq M ( + , F ) )
21 20 breq1d 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( ( seq N ( + , F ) |` ( ZZ>= ` M ) ) ~~> C <-> seq M ( + , F ) ~~> C ) )
22 3 adantr 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> M e. ZZ )
23 seqex 
 |-  seq N ( + , F ) e. _V
24 climres 
 |-  ( ( M e. ZZ /\ seq N ( + , F ) e. _V ) -> ( ( seq N ( + , F ) |` ( ZZ>= ` M ) ) ~~> C <-> seq N ( + , F ) ~~> C ) )
25 22 23 24 sylancl 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( ( seq N ( + , F ) |` ( ZZ>= ` M ) ) ~~> C <-> seq N ( + , F ) ~~> C ) )
26 21 25 bitr3d 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )
27 uztric 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
28 3 4 27 syl2anc 
 |-  ( ph -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
29 16 26 28 mpjaodan 
 |-  ( ph -> ( seq M ( + , F ) ~~> C <-> seq N ( + , F ) ~~> C ) )