fprodeq0

Description: Anything finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017)

	Ref	Expression
Hypotheses	fprodeq0.1	$⊢ Z = ℤ_{\geq M}$
	fprodeq0.2	$⊢ φ \to N \in Z$
	fprodeq0.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
	fprodeq0.4	$⊢ (φ \land k = N) \to A = 0$
Assertion	fprodeq0	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = M}^{K} A = 0$

Proof

Step	Hyp	Ref	Expression
1		fprodeq0.1	$⊢ Z = ℤ_{\geq M}$
2		fprodeq0.2	$⊢ φ \to N \in Z$
3		fprodeq0.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
4		fprodeq0.4	$⊢ (φ \land k = N) \to A = 0$
5		eluzel2	$⊢ K \in ℤ_{\geq N} \to N \in ℤ$
6	5	adantl	$⊢ (φ \land K \in ℤ_{\geq N}) \to N \in ℤ$
7	6	zred	$⊢ (φ \land K \in ℤ_{\geq N}) \to N \in ℝ$
8	7	ltp1d	$⊢ (φ \land K \in ℤ_{\geq N}) \to N < N + 1$
9		fzdisj	$⊢ N < N + 1 \to (M \dots N) \cap (N + 1 \dots K) = \emptyset$
10	8 9	syl	$⊢ (φ \land K \in ℤ_{\geq N}) \to (M \dots N) \cap (N + 1 \dots K) = \emptyset$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	11 1	eleq2s	$⊢ N \in Z \to M \in ℤ$
13	2 12	syl	$⊢ φ \to M \in ℤ$
14	13	adantr	$⊢ (φ \land K \in ℤ_{\geq N}) \to M \in ℤ$
15		eluzelz	$⊢ K \in ℤ_{\geq N} \to K \in ℤ$
16	15	adantl	$⊢ (φ \land K \in ℤ_{\geq N}) \to K \in ℤ$
17	14 16 6	3jca	$⊢ (φ \land K \in ℤ_{\geq N}) \to (M \in ℤ \land K \in ℤ \land N \in ℤ)$
18		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
19	18 1	eleq2s	$⊢ N \in Z \to M \leq N$
20	2 19	syl	$⊢ φ \to M \leq N$
21		eluzle	$⊢ K \in ℤ_{\geq N} \to N \leq K$
22	20 21	anim12i	$⊢ (φ \land K \in ℤ_{\geq N}) \to (M \leq N \land N \leq K)$
23		elfz2	$⊢ N \in (M \dots K) \leftrightarrow ((M \in ℤ \land K \in ℤ \land N \in ℤ) \land (M \leq N \land N \leq K))$
24	17 22 23	sylanbrc	$⊢ (φ \land K \in ℤ_{\geq N}) \to N \in (M \dots K)$
25		fzsplit	$⊢ N \in (M \dots K) \to (M \dots K) = (M \dots N) \cup (N + 1 \dots K)$
26	24 25	syl	$⊢ (φ \land K \in ℤ_{\geq N}) \to (M \dots K) = (M \dots N) \cup (N + 1 \dots K)$
27		fzfid	$⊢ (φ \land K \in ℤ_{\geq N}) \to (M \dots K) \in Fin$
28		elfzuz	$⊢ k \in (M \dots K) \to k \in ℤ_{\geq M}$
29	28 1	eleqtrrdi	$⊢ k \in (M \dots K) \to k \in Z$
30	29 3	sylan2	$⊢ (φ \land k \in (M \dots K)) \to A \in ℂ$
31	30	adantlr	$⊢ ((φ \land K \in ℤ_{\geq N}) \land k \in (M \dots K)) \to A \in ℂ$
32	10 26 27 31	fprodsplit	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = M}^{K} A = \prod_{k = M}^{N} A \prod_{k = N + 1}^{K} A$
33	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
34		elfzuz	$⊢ k \in (M \dots N) \to k \in ℤ_{\geq M}$
35	34 1	eleqtrrdi	$⊢ k \in (M \dots N) \to k \in Z$
36	35 3	sylan2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
37	33 36	fprodm1s	$⊢ φ \to \prod_{k = M}^{N} A = \prod_{k = M}^{N - 1} A ⦋ N / k ⦌ A$
38	2 4	csbied	$⊢ φ \to ⦋ N / k ⦌ A = 0$
39	38	oveq2d	$⊢ φ \to \prod_{k = M}^{N - 1} A ⦋ N / k ⦌ A = \prod_{k = M}^{N - 1} A \cdot 0$
40		fzfid	$⊢ φ \to (M \dots N - 1) \in Fin$
41		elfzuz	$⊢ k \in (M \dots N - 1) \to k \in ℤ_{\geq M}$
42	41 1	eleqtrrdi	$⊢ k \in (M \dots N - 1) \to k \in Z$
43	42 3	sylan2	$⊢ (φ \land k \in (M \dots N - 1)) \to A \in ℂ$
44	40 43	fprodcl	$⊢ φ \to \prod_{k = M}^{N - 1} A \in ℂ$
45	44	mul01d	$⊢ φ \to \prod_{k = M}^{N - 1} A \cdot 0 = 0$
46	37 39 45	3eqtrd	$⊢ φ \to \prod_{k = M}^{N} A = 0$
47	46	adantr	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = M}^{N} A = 0$
48	47	oveq1d	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = M}^{N} A \prod_{k = N + 1}^{K} A = 0 \cdot \prod_{k = N + 1}^{K} A$
49		fzfid	$⊢ (φ \land K \in ℤ_{\geq N}) \to (N + 1 \dots K) \in Fin$
50	1	peano2uzs	$⊢ N \in Z \to N + 1 \in Z$
51	2 50	syl	$⊢ φ \to N + 1 \in Z$
52		elfzuz	$⊢ k \in (N + 1 \dots K) \to k \in ℤ_{\geq (N + 1)}$
53	1	uztrn2	$⊢ (N + 1 \in Z \land k \in ℤ_{\geq (N + 1)}) \to k \in Z$
54	51 52 53	syl2an	$⊢ (φ \land k \in (N + 1 \dots K)) \to k \in Z$
55	54	adantrl	$⊢ (φ \land (K \in ℤ_{\geq N} \land k \in (N + 1 \dots K))) \to k \in Z$
56	55 3	syldan	$⊢ (φ \land (K \in ℤ_{\geq N} \land k \in (N + 1 \dots K))) \to A \in ℂ$
57	56	anassrs	$⊢ ((φ \land K \in ℤ_{\geq N}) \land k \in (N + 1 \dots K)) \to A \in ℂ$
58	49 57	fprodcl	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = N + 1}^{K} A \in ℂ$
59	58	mul02d	$⊢ (φ \land K \in ℤ_{\geq N}) \to 0 \cdot \prod_{k = N + 1}^{K} A = 0$
60	32 48 59	3eqtrd	$⊢ (φ \land K \in ℤ_{\geq N}) \to \prod_{k = M}^{K} A = 0$

Metamath Proof Explorer

Theorem fprodeq0

Proof