prodrblem2

	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	prodrblem2	$⊢ (φ \land N \in ℤ_{\geq M}) \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	4	adantr	$⊢ (φ \land N \in ℤ_{\geq M}) \to N \in ℤ$
8		seqex	$⊢ seq M (\times F) \in V$
9		climres	$⊢ (N \in ℤ \land seq M (\times F) \in V) \to (({seq M (\times F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq M (\times F) ⇝ C)$
10	7 8 9	sylancl	$⊢ (φ \land N \in ℤ_{\geq M}) \to (({seq M (\times F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq M (\times F) ⇝ C)$
11	2	adantlr	$⊢ ((φ \land N \in ℤ_{\geq M}) \land k \in A) \to B \in ℂ$
12		simpr	$⊢ (φ \land N \in ℤ_{\geq M}) \to N \in ℤ_{\geq M}$
13	1 11 12	prodrblem	$⊢ ((φ \land N \in ℤ_{\geq M}) \land A \subseteq ℤ_{\geq N}) \to {seq M (\times F) ↾}_{ℤ_{\geq N}} = seq N (\times F)$
14	6 13	mpidan	$⊢ (φ \land N \in ℤ_{\geq M}) \to {seq M (\times F) ↾}_{ℤ_{\geq N}} = seq N (\times F)$
15	14	breq1d	$⊢ (φ \land N \in ℤ_{\geq M}) \to (({seq M (\times F) ↾}_{ℤ_{\geq N}}) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$
16	10 15	bitr3d	$⊢ (φ \land N \in ℤ_{\geq M}) \to (seq M (\times F) ⇝ C \leftrightarrow seq N (\times F) ⇝ C)$

Metamath Proof Explorer