# 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}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
prodrb.4 ${⊢}{\phi }\to {M}\in ℤ$
prodrb.5 ${⊢}{\phi }\to {N}\in ℤ$
prodrb.6 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
prodrb.7 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {N}}$
Assertion prodrb ${⊢}{\phi }\to \left(seq{M}\left(×,{F}\right)⇝{C}↔seq{N}\left(×,{F}\right)⇝{C}\right)$

### Proof

Step Hyp Ref Expression
1 prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
2 prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 prodrb.4 ${⊢}{\phi }\to {M}\in ℤ$
4 prodrb.5 ${⊢}{\phi }\to {N}\in ℤ$
5 prodrb.6 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
6 prodrb.7 ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {N}}$
7 1 2 3 4 5 6 prodrblem2 ${⊢}\left({\phi }\wedge {N}\in {ℤ}_{\ge {M}}\right)\to \left(seq{M}\left(×,{F}\right)⇝{C}↔seq{N}\left(×,{F}\right)⇝{C}\right)$
8 1 2 4 3 6 5 prodrblem2 ${⊢}\left({\phi }\wedge {M}\in {ℤ}_{\ge {N}}\right)\to \left(seq{N}\left(×,{F}\right)⇝{C}↔seq{M}\left(×,{F}\right)⇝{C}\right)$
9 8 bicomd ${⊢}\left({\phi }\wedge {M}\in {ℤ}_{\ge {N}}\right)\to \left(seq{M}\left(×,{F}\right)⇝{C}↔seq{N}\left(×,{F}\right)⇝{C}\right)$
10 uztric ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\in {ℤ}_{\ge {M}}\vee {M}\in {ℤ}_{\ge {N}}\right)$
11 3 4 10 syl2anc ${⊢}{\phi }\to \left({N}\in {ℤ}_{\ge {M}}\vee {M}\in {ℤ}_{\ge {N}}\right)$
12 7 9 11 mpjaodan ${⊢}{\phi }\to \left(seq{M}\left(×,{F}\right)⇝{C}↔seq{N}\left(×,{F}\right)⇝{C}\right)$