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