Metamath Proof Explorer

Theorem ntrivcvgtail

Description: A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 ntrivcvgtail.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ntrivcvgtail.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 ntrivcvgtail.3 ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
4 ntrivcvgtail.4 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
5 ntrivcvgtail.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 4 eqnetrd ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 )
12 3 10 breqtrrd ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
13 11 12 jca ⊢ ( 𝜑 → ( ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ) )
15 seqeq1 ⊢ ( 𝑁 = 𝑀 → seq 𝑁 ( · , 𝐹 ) = seq 𝑀 ( · , 𝐹 ) )
16 15 fveq2d ⊢ ( 𝑁 = 𝑀 → ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) = ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) )
17 16 neeq1d ⊢ ( 𝑁 = 𝑀 → ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ↔ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 ) )
18 15 16 breq12d ⊢ ( 𝑁 = 𝑀 → ( seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ↔ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ) )
19 17 18 anbi12d ⊢ ( 𝑁 = 𝑀 → ( ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) ↔ ( ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ) ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) ↔ ( ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑀 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( · , 𝐹 ) ) ) ) )
21 14 20 mpbird ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) )
22 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
23 22 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 − 1 ) ∈ 𝑍 )
24 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 )
26 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑋 ≠ 0 )
27 1 23 25 26 24 ntrivcvgfvn0 ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ≠ 0 )
28 1 23 24 25 27 clim2div ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ ( 𝑋 / ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
29 funbrfv ⊢ ( Fun ⇝ → ( seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ ( 𝑋 / ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) → ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) = ( 𝑋 / ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) ) )
30 8 28 29 mpsyl ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) = ( 𝑋 / ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) )
31 climcl ⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝑋 → 𝑋 ∈ ℂ )
32 3 31 syl ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
33 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑋 ∈ ℂ )
34 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
35 34 1 eleq2s ⊢ ( 𝑁 ∈ 𝑍 → 𝑀 ∈ ℤ )
36 2 35 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37 1 36 5 prodf ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ )
38 1 feq2i ⊢ ( seq 𝑀 ( · , 𝐹 ) : 𝑍 ⟶ ℂ ↔ seq 𝑀 ( · , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ ℂ )
39 37 38 sylib ⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) : ( ℤ≥ ‘ 𝑀 ) ⟶ ℂ )
40 39 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ∈ ℂ )
41 33 40 26 27 divne0d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑋 / ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑁 − 1 ) ) ) ≠ 0 )
42 30 41 eqnetrd ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) ≠ 0 )
43 28 30 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) )
44 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
45 1 44 eqsstri ⊢ 𝑍 ⊆ ℤ
46 45 2 sseldi ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
47 46 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℂ )
49 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ∈ ℂ )
50 48 49 npcand ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
51 50 seqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) = seq 𝑁 ( · , 𝐹 ) )
52 51 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) = ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) )
53 52 neeq1d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) ≠ 0 ↔ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ) )
54 51 52 breq12d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) ↔ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) )
55 53 54 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) ≠ 0 ∧ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq ( ( 𝑁 − 1 ) + 1 ) ( · , 𝐹 ) ) ) ↔ ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) ) )
56 42 43 55 mpbi2and ⊢ ( ( 𝜑 ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) )
57 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
58 uzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
59 57 58 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
60 21 56 59 mpjaodan ⊢ ( 𝜑 → ( ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ≠ 0 ∧ seq 𝑁 ( · , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑁 ( · , 𝐹 ) ) ) )