Theorem prodfn0

Description: No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018)

	Ref	Expression
Hypotheses	prodfn0.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	prodfn0.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
	prodfn0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
Assertion	prodfn0	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		prodfn0.1	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		prodfn0.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
3		prodfn0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
4		eluzfz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
5	1 4	syl	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
6		fveq2	⊢ ( 𝑚 = 𝑀 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) )
7	6	neeq1d	⊢ ( 𝑚 = 𝑀 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ) )
8	7	imbi2d	⊢ ( 𝑚 = 𝑀 → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ) ) )
9		fveq2	⊢ ( 𝑚 = 𝑛 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) )
10	9	neeq1d	⊢ ( 𝑚 = 𝑛 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) )
11	10	imbi2d	⊢ ( 𝑚 = 𝑛 → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) ) )
12		fveq2	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) )
13	12	neeq1d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 ) )
14	13	imbi2d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 ) ) )
15		fveq2	⊢ ( 𝑚 = 𝑁 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) )
16	15	neeq1d	⊢ ( 𝑚 = 𝑁 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 ) )
17	16	imbi2d	⊢ ( 𝑚 = 𝑁 → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) ≠ 0 ) ↔ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 ) ) )
18		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
19		elfzelz	⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ∈ ℤ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
21		seq1	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
23		fveq2	⊢ ( 𝑘 = 𝑀 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑀 ) )
24	23	neeq1d	⊢ ( 𝑘 = 𝑀 → ( ( 𝐹 ‘ 𝑘 ) ≠ 0 ↔ ( 𝐹 ‘ 𝑀 ) ≠ 0 ) )
25	24	imbi2d	⊢ ( 𝑘 = 𝑀 → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≠ 0 ) ) )
26	3	expcom	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
27	25 26	vtoclga	⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ≠ 0 ) )
28	27	impcom	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑀 ) ≠ 0 )
29	22 28	eqnetrd	⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 )
30	29	expcom	⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ) )
31	18 30	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ) )
32		elfzouz	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
33	32	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
34		seqp1	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
35	33 34	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
36		elfzofz	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
37		elfzuz	⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
39		elfzuz3	⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) )
40		fzss2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
41	39 40	syl	⊢ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ... 𝑛 ) ⊆ ( 𝑀 ... 𝑁 ) )
42	41	sselda	⊢ ( ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
43	42 2	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
44	43	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
45		mulcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
46	45	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
47	38 44 46	seqcl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
48	36 47	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
49	48	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ∈ ℂ )
50		fzofzp1	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
51		fveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
52	51	eleq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
53	52	imbi2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) ) )
54	2	expcom	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
55	53 54	vtoclga	⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
56	50 55	syl	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
57	56	impcom	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
58	57	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
59		simp3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 )
60	51	neeq1d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 0 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 ) )
61	60	imbi2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝐹 ‘ 𝑘 ) ≠ 0 ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 ) ) )
62	61 26	vtoclga	⊢ ( ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 ) )
63	62	impcom	⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 )
64	50 63	sylan2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 )
65	64	3adant3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≠ 0 )
66	49 58 59 65	mulne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ≠ 0 )
67	35 66	eqnetrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 )
68	67	3exp	⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 ) ) )
69	68	com12	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 ) ) )
70	69	a2d	⊢ ( 𝑛 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) ≠ 0 ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) ≠ 0 ) ) )
71	8 11 14 17 31 70	fzind2	⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 ) )
72	5 71	mpcom	⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )