prodrblem

	Ref	Expression
Hypotheses	prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
	prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	prodrb.3	$⊢ φ \to N \in ℤ_{\geq M}$
Assertion	prodrblem	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to {seq M (\times F) ↾}_{ℤ_{\geq N}} = seq N (\times F)$

Proof

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.3	$⊢ φ \to N \in ℤ_{\geq M}$
4		mulid2	$⊢ n \in ℂ \to 1 n = n$
5	4	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in ℂ) \to 1 n = n$
6		1cnd	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to 1 \in ℂ$
7	3	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to N \in ℤ_{\geq M}$
8		iftrue	$⊢ k \in A \to if (k \in A, B, 1) = B$
9	8	adantl	$⊢ ((φ \land k \in ℤ) \land k \in A) \to if (k \in A, B, 1) = B$
10	2	adantlr	$⊢ ((φ \land k \in ℤ) \land k \in A) \to B \in ℂ$
11	9 10	eqeltrd	$⊢ ((φ \land k \in ℤ) \land k \in A) \to if (k \in A, B, 1) \in ℂ$
12	11	ex	$⊢ (φ \land k \in ℤ) \to (k \in A \to if (k \in A, B, 1) \in ℂ)$
13		iffalse	$⊢ \neg k \in A \to if (k \in A, B, 1) = 1$
14		ax-1cn	$⊢ 1 \in ℂ$
15	13 14	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, B, 1) \in ℂ$
16	12 15	pm2.61d1	$⊢ (φ \land k \in ℤ) \to if (k \in A, B, 1) \in ℂ$
17	16 1	fmptd	$⊢ φ \to F : ℤ ⟶ ℂ$
18		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
19	18 3	sselid	$⊢ φ \to N \in ℤ$
20	17 19	ffvelrnd	$⊢ φ \to F (N) \in ℂ$
21	20	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to F (N) \in ℂ$
22		elfzelz	$⊢ n \in (M \dots N - 1) \to n \in ℤ$
23	22	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to n \in ℤ$
24		simplr	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to A \subseteq ℤ_{\geq N}$
25	19	zcnd	$⊢ φ \to N \in ℂ$
26	25	adantr	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to N \in ℂ$
27	26	adantr	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to N \in ℂ$
28		1cnd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to 1 \in ℂ$
29	27 28	npcand	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to N - 1 + 1 = N$
30	29	fveq2d	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to ℤ_{\geq (N - 1 + 1)} = ℤ_{\geq N}$
31	24 30	sseqtrrd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to A \subseteq ℤ_{\geq (N - 1 + 1)}$
32		fznuz	$⊢ n \in (M \dots N - 1) \to \neg n \in ℤ_{\geq (N - 1 + 1)}$
33	32	adantl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to \neg n \in ℤ_{\geq (N - 1 + 1)}$
34	31 33	ssneldd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to \neg n \in A$
35	23 34	eldifd	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to n \in (ℤ ∖ A)$
36		fveqeq2	$⊢ k = n \to (F (k) = 1 \leftrightarrow F (n) = 1)$
37		eldifi	$⊢ k \in (ℤ ∖ A) \to k \in ℤ$
38		eldifn	$⊢ k \in (ℤ ∖ A) \to \neg k \in A$
39	38 13	syl	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 1) = 1$
40	39 14	eqeltrdi	$⊢ k \in (ℤ ∖ A) \to if (k \in A, B, 1) \in ℂ$
41	1	fvmpt2	$⊢ (k \in ℤ \land if (k \in A, B, 1) \in ℂ) \to F (k) = if (k \in A, B, 1)$
42	37 40 41	syl2anc	$⊢ k \in (ℤ ∖ A) \to F (k) = if (k \in A, B, 1)$
43	42 39	eqtrd	$⊢ k \in (ℤ ∖ A) \to F (k) = 1$
44	36 43	vtoclga	$⊢ n \in (ℤ ∖ A) \to F (n) = 1$
45	35 44	syl	$⊢ ((φ \land A \subseteq ℤ_{\geq N}) \land n \in (M \dots N - 1)) \to F (n) = 1$
46	5 6 7 21 45	seqid	$⊢ (φ \land A \subseteq ℤ_{\geq N}) \to {seq M (\times F) ↾}_{ℤ_{\geq N}} = seq N (\times F)$

Metamath Proof Explorer

Theorem prodrblem

Proof