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 ∈ ℤ ⟼ if k ∈ A B 1
prodmo.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
prodrb.4 ⊢ φ → M ∈ ℤ
prodrb.5 ⊢ φ → N ∈ ℤ
prodrb.6 ⊢ φ → A ⊆ ℤ ≥ M
prodrb.7 ⊢ φ → A ⊆ ℤ ≥ N
Assertion prodrb ⊢ φ → seq M × F ⇝ C ↔ seq N × F ⇝ C

Proof

Step Hyp Ref Expression
1 prodmo.1 ⊢ F = k ∈ ℤ ⟼ if k ∈ A B 1
2 prodmo.2 ⊢ φ ∧ k ∈ A → B ∈ ℂ
3 prodrb.4 ⊢ φ → M ∈ ℤ
4 prodrb.5 ⊢ φ → N ∈ ℤ
5 prodrb.6 ⊢ φ → A ⊆ ℤ ≥ M
6 prodrb.7 ⊢ φ → A ⊆ ℤ ≥ N
7 1 2 3 4 5 6 prodrblem2 ⊢ φ ∧ N ∈ ℤ ≥ M → seq M × F ⇝ C ↔ seq N × F ⇝ C
8 1 2 4 3 6 5 prodrblem2 ⊢ φ ∧ M ∈ ℤ ≥ N → seq N × F ⇝ C ↔ seq M × F ⇝ C
9 8 bicomd ⊢ φ ∧ M ∈ ℤ ≥ N → seq M × F ⇝ C ↔ seq N × F ⇝ C
10 uztric ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ M ∨ M ∈ ℤ ≥ N
11 3 4 10 syl2anc ⊢ φ → N ∈ ℤ ≥ M ∨ M ∈ ℤ ≥ N
12 7 9 11 mpjaodan ⊢ φ → seq M × F ⇝ C ↔ seq N × F ⇝ C