prodrb

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

	Ref	Expression
Hypotheses	prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
	prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	prodrb.4	$⊢ φ \to M \in ℤ$
	prodrb.5	$⊢ φ \to N \in ℤ$
	prodrb.6	$⊢ φ \to A \subseteq ℤ_{\geq M}$
	prodrb.7	$⊢ φ \to A \subseteq ℤ_{\geq N}$
Assertion	prodrb	$⊢ φ \to (seq M (\times F) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$

Step	Hyp	Ref	Expression
1		prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
2		prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodrb.4	$⊢ φ \to M \in ℤ$
4		prodrb.5	$⊢ φ \to N \in ℤ$
5		prodrb.6	$⊢ φ \to A \subseteq ℤ_{\geq M}$
6		prodrb.7	$⊢ φ \to A \subseteq ℤ_{\geq N}$
7	1 2 3 4 5 6	prodrblem2	$⊢ (φ \land N \in ℤ_{\geq M}) \to (seq M (\times F) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$
8	1 2 4 3 6 5	prodrblem2	$⊢ (φ \land M \in ℤ_{\geq N}) \to (seq N (\times F) ⇝ C \leftrightarrow seq M (\times F) ⇝ C)$
9	8	bicomd	$⊢ (φ \land M \in ℤ_{\geq N}) \to (seq M (\times F) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$
10		uztric	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$
11	3 4 10	syl2anc	$⊢ φ \to (N \in ℤ_{\geq M} \lor M \in ℤ_{\geq N})$
12	7 9 11	mpjaodan	$⊢ φ \to (seq M (\times F) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$

Metamath Proof Explorer