Metamath Proof Explorer

Theorem ntrivcvgfvn0

Description: Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017)

Ref Expression
Hypotheses ntrivcvgfvn0.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ntrivcvgfvn0.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
ntrivcvgfvn0.3 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
ntrivcvgfvn0.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
ntrivcvgfvn0.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion ntrivcvgfvn0 ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 ntrivcvgfvn0.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ntrivcvgfvn0.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 ntrivcvgfvn0.3 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
4 ntrivcvgfvn0.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
5 ntrivcvgfvn0.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6 fclim ⊢ ⇝ : dom ⇝ ⟶ ℂ
7 ffun ⊢ ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
8 6 7 ax-mp ⊢ Fun ⇝
9 funbrfv ⊢ ( Fun ⇝ → ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 𝑋 ) )
10 8 3 9 mpsyl ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 𝑋 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 𝑋 )
12 eqid ⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 )
13 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
14 1 13 eqsstri ⊢ 𝑍 ⊆ ℤ
15 14 2 sselid ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → 𝑁 ∈ ℤ )
17 seqex ⊢ seq 𝑀 ( · , 𝐹 ) ∈ V
18 17 a1i ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → seq 𝑀 ( · , 𝐹 ) ∈ V )
19 0cnd ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → 0 ∈ ℂ )
20 fveqeq2 ⊢ ( 𝑚 = 𝑁 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) )
21 20 imbi2d ⊢ ( 𝑚 = 𝑁 → ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ) ↔ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) ) )
22 fveqeq2 ⊢ ( 𝑚 = 𝑛 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) )
23 22 imbi2d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ) ↔ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) ) )
24 fveqeq2 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 ) )
25 24 imbi2d ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ) ↔ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 ) ) )
26 fveqeq2 ⊢ ( 𝑚 = 𝑘 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ↔ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = 0 ) )
27 26 imbi2d ⊢ ( 𝑚 = 𝑘 → ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑚 ) = 0 ) ↔ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = 0 ) ) )
28 simpr ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 )
29 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
30 uztrn ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 29 30 sylan2 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 3adant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
33 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
34 32 33 syl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
35 oveq1 ⊢ ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( 0 · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
36 35 3ad2ant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = ( 0 · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
37 peano2uz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
38 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑛 + 1 ) ∈ 𝑍 )
39 2 37 38 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑛 + 1 ) ∈ 𝑍 )
40 5 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
41 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
42 41 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
43 42 rspcv ⊢ ( ( 𝑛 + 1 ) ∈ 𝑍 → ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ ) )
44 40 43 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
45 39 44 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
46 45 ancoms ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℂ )
47 46 mul02d ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ) → ( 0 · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = 0 )
48 47 3adant3 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → ( 0 · ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) = 0 )
49 34 36 48 3eqtrd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 )
50 49 3exp ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 ) ) )
51 50 adantrd ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 ) ) )
52 51 a2d ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑛 ) = 0 ) → ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 + 1 ) ) = 0 ) ) )
53 21 23 25 27 28 52 uzind4i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = 0 ) )
54 53 impcom ⊢ ( ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑘 ) = 0 )
55 12 16 18 19 54 climconst ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → seq 𝑀 ( · , 𝐹 ) ⇝ 0 )
56 funbrfv ⊢ ( Fun ⇝ → ( seq 𝑀 ( · , 𝐹 ) ⇝ 0 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 0 ) )
57 8 55 56 mpsyl ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) = 0 )
58 11 57 eqtr3d ⊢ ( ( 𝜑 ∧ ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 ) → 𝑋 = 0 )
59 58 ex ⊢ ( 𝜑 → ( ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) = 0 → 𝑋 = 0 ) )
60 59 necon3d ⊢ ( 𝜑 → ( 𝑋 ≠ 0 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 ) )
61 4 60 mpd ⊢ ( 𝜑 → ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ≠ 0 )