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 ) )