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

Metamath Proof Explorer

Theorem prodrb

Description: Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
prodmo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
prodrb.4 
|- ( ph -> M e. ZZ )
prodrb.5 
|- ( ph -> N e. ZZ )
prodrb.6 
|- ( ph -> A C_ ( ZZ>= ` M ) )
prodrb.7 
|- ( ph -> A C_ ( ZZ>= ` N ) )
Assertion prodrb 
|- ( ph -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2 prodmo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodrb.4 
 |-  ( ph -> M e. ZZ )
4 prodrb.5 
 |-  ( ph -> N e. ZZ )
5 prodrb.6 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
6 prodrb.7 
 |-  ( ph -> A C_ ( ZZ>= ` N ) )
7 1 2 3 4 5 6 prodrblem2 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
8 1 2 4 3 6 5 prodrblem2 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( seq N ( x. , F ) ~~> C <-> seq M ( x. , F ) ~~> C ) )
9 8 bicomd 
 |-  ( ( ph /\ M e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )
10 uztric 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
11 3 4 10 syl2anc 
 |-  ( ph -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
12 7 9 11 mpjaodan 
 |-  ( ph -> ( seq M ( x. , F ) ~~> C <-> seq N ( x. , F ) ~~> C ) )