Theorem fprodeq0

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

	Ref	Expression
Hypotheses	fprodeq0.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	fprodeq0.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
	fprodeq0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	fprodeq0.4	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝐴 = 0 )
Assertion	fprodeq0	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 0 )

Proof

Step	Hyp	Ref	Expression
1		fprodeq0.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		fprodeq0.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3		fprodeq0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
4		fprodeq0.4	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝐴 = 0 )
5		eluzel2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
6	5	adantl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
7	6	zred	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
8	7	ltp1d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 < ( 𝑁 + 1 ) )
9		fzdisj	⊢ ( 𝑁 < ( 𝑁 + 1 ) → ( ( 𝑀 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... 𝐾 ) ) = ∅ )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑀 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... 𝐾 ) ) = ∅ )
11		eluzel2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12	11 1	eleq2s	⊢ ( 𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ )
13	2 12	syl	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℤ )
15		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝐾 ∈ ℤ )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ℤ )
17	14 16 6	3jca	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
18		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
19	18 1	eleq2s	⊢ ( 𝑁 ∈ 𝑍 → 𝑀 ≤ 𝑁 )
20	2 19	syl	⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
21		eluzle	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝐾 )
22	20 21	anim12i	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝐾 ) )
23		elfz2	⊢ ( 𝑁 ∈ ( 𝑀 ... 𝐾 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝐾 ) ) )
24	17 22 23	sylanbrc	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( 𝑀 ... 𝐾 ) )
25		fzsplit	⊢ ( 𝑁 ∈ ( 𝑀 ... 𝐾 ) → ( 𝑀 ... 𝐾 ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... 𝐾 ) ) )
26	24 25	syl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑀 ... 𝐾 ) = ( ( 𝑀 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... 𝐾 ) ) )
27		fzfid	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑀 ... 𝐾 ) ∈ Fin )
28		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝐾 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
29	28 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝐾 ) → 𝑘 ∈ 𝑍 )
30	29 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝐾 ) ) → 𝐴 ∈ ℂ )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝐾 ) ) → 𝐴 ∈ ℂ )
32	10 26 27 31	fprodsplit	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) 𝐴 ) )
33	2 1	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
34		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
35	34 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ 𝑍 )
36	35 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
37	33 36	fprodm1s	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · ⦋ 𝑁 / 𝑘 ⦌ 𝐴 ) )
38	2 4	csbied	⊢ ( 𝜑 → ⦋ 𝑁 / 𝑘 ⦌ 𝐴 = 0 )
39	38	oveq2d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · ⦋ 𝑁 / 𝑘 ⦌ 𝐴 ) = ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · 0 ) )
40		fzfid	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) ∈ Fin )
41		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
42	41 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ 𝑍 )
43	42 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
44	40 43	fprodcl	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 ∈ ℂ )
45	44	mul01d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 · 0 ) = 0 )
46	37 39 45	3eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 0 )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = 0 )
48	47	oveq1d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ∏ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) 𝐴 ) = ( 0 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) 𝐴 ) )
49		fzfid	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑁 + 1 ) ... 𝐾 ) ∈ Fin )
50	1	peano2uzs	⊢ ( 𝑁 ∈ 𝑍 → ( 𝑁 + 1 ) ∈ 𝑍 )
51	2 50	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
52		elfzuz	⊢ ( 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
53	1	uztrn2	⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
54	51 52 53	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) ) → 𝑘 ∈ 𝑍 )
55	54	adantrl	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) ) ) → 𝑘 ∈ 𝑍 )
56	55 3	syldan	⊢ ( ( 𝜑 ∧ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) ) ) → 𝐴 ∈ ℂ )
57	56	anassrs	⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) ) → 𝐴 ∈ ℂ )
58	49 57	fprodcl	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) 𝐴 ∈ ℂ )
59	58	mul02d	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 0 · ∏ 𝑘 ∈ ( ( 𝑁 + 1 ) ... 𝐾 ) 𝐴 ) = 0 )
60	32 48 59	3eqtrd	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 0 )