Metamath Proof Explorer

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 )