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 ⊢ Z = ℤ ≥ M
ntrivcvgtail.2 ⊢ φ → N ∈ Z
ntrivcvgtail.3 ⊢ φ → seq M × F ⇝ X
ntrivcvgtail.4 ⊢ φ → X ≠ 0
ntrivcvgtail.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
Assertion ntrivcvgtail ⊢ φ → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F

Proof

Step Hyp Ref Expression
1 ntrivcvgtail.1 ⊢ Z = ℤ ≥ M
2 ntrivcvgtail.2 ⊢ φ → N ∈ Z
3 ntrivcvgtail.3 ⊢ φ → seq M × F ⇝ X
4 ntrivcvgtail.4 ⊢ φ → X ≠ 0
5 ntrivcvgtail.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
6 fclim ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ
7 ffun ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ → Fun ⁡ ⇝
8 6 7 ax-mp ⊢ Fun ⁡ ⇝
9 funbrfv ⊢ Fun ⁡ ⇝ → seq M × F ⇝ X → ⇝ ⁡ seq M × F = X
10 8 3 9 mpsyl ⊢ φ → ⇝ ⁡ seq M × F = X
11 10 4 eqnetrd ⊢ φ → ⇝ ⁡ seq M × F ≠ 0
12 3 10 breqtrrd ⊢ φ → seq M × F ⇝ ⇝ ⁡ seq M × F
13 11 12 jca ⊢ φ → ⇝ ⁡ seq M × F ≠ 0 ∧ seq M × F ⇝ ⇝ ⁡ seq M × F
14 13 adantr ⊢ φ ∧ N = M → ⇝ ⁡ seq M × F ≠ 0 ∧ seq M × F ⇝ ⇝ ⁡ seq M × F
15 seqeq1 ⊢ N = M → seq N × F = seq M × F
16 15 fveq2d ⊢ N = M → ⇝ ⁡ seq N × F = ⇝ ⁡ seq M × F
17 16 neeq1d ⊢ N = M → ⇝ ⁡ seq N × F ≠ 0 ↔ ⇝ ⁡ seq M × F ≠ 0
18 15 16 breq12d ⊢ N = M → seq N × F ⇝ ⇝ ⁡ seq N × F ↔ seq M × F ⇝ ⇝ ⁡ seq M × F
19 17 18 anbi12d ⊢ N = M → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F ↔ ⇝ ⁡ seq M × F ≠ 0 ∧ seq M × F ⇝ ⇝ ⁡ seq M × F
20 19 adantl ⊢ φ ∧ N = M → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F ↔ ⇝ ⁡ seq M × F ≠ 0 ∧ seq M × F ⇝ ⇝ ⁡ seq M × F
21 14 20 mpbird ⊢ φ ∧ N = M → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F
22 simpr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → N − 1 ∈ ℤ ≥ M
23 22 1 eleqtrrdi ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → N − 1 ∈ Z
24 5 adantlr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M ∧ k ∈ Z → F ⁡ k ∈ ℂ
25 3 adantr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq M × F ⇝ X
26 4 adantr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → X ≠ 0
27 1 23 25 26 24 ntrivcvgfvn0 ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq M × F ⁡ N − 1 ≠ 0
28 1 23 24 25 27 clim2div ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq N - 1 + 1 × F ⇝ X seq M × F ⁡ N − 1
29 funbrfv ⊢ Fun ⁡ ⇝ → seq N - 1 + 1 × F ⇝ X seq M × F ⁡ N − 1 → ⇝ ⁡ seq N - 1 + 1 × F = X seq M × F ⁡ N − 1
30 8 28 29 mpsyl ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N - 1 + 1 × F = X seq M × F ⁡ N − 1
31 climcl ⊢ seq M × F ⇝ X → X ∈ ℂ
32 3 31 syl ⊢ φ → X ∈ ℂ
33 32 adantr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → X ∈ ℂ
34 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
35 34 1 eleq2s ⊢ N ∈ Z → M ∈ ℤ
36 2 35 syl ⊢ φ → M ∈ ℤ
37 1 36 5 prodf ⊢ φ → seq M × F : Z ⟶ ℂ
38 1 feq2i ⊢ seq M × F : Z ⟶ ℂ ↔ seq M × F : ℤ ≥ M ⟶ ℂ
39 37 38 sylib ⊢ φ → seq M × F : ℤ ≥ M ⟶ ℂ
40 39 ffvelrnda ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq M × F ⁡ N − 1 ∈ ℂ
41 33 40 26 27 divne0d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → X seq M × F ⁡ N − 1 ≠ 0
42 30 41 eqnetrd ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N - 1 + 1 × F ≠ 0
43 28 30 breqtrrd ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq N - 1 + 1 × F ⇝ ⇝ ⁡ seq N - 1 + 1 × F
44 uzssz ⊢ ℤ ≥ M ⊆ ℤ
45 1 44 eqsstri ⊢ Z ⊆ ℤ
46 45 2 sseldi ⊢ φ → N ∈ ℤ
47 46 zcnd ⊢ φ → N ∈ ℂ
48 47 adantr ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → N ∈ ℂ
49 1cnd ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → 1 ∈ ℂ
50 48 49 npcand ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → N - 1 + 1 = N
51 50 seqeq1d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq N - 1 + 1 × F = seq N × F
52 51 fveq2d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N - 1 + 1 × F = ⇝ ⁡ seq N × F
53 52 neeq1d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N - 1 + 1 × F ≠ 0 ↔ ⇝ ⁡ seq N × F ≠ 0
54 51 52 breq12d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → seq N - 1 + 1 × F ⇝ ⇝ ⁡ seq N - 1 + 1 × F ↔ seq N × F ⇝ ⇝ ⁡ seq N × F
55 53 54 anbi12d ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N - 1 + 1 × F ≠ 0 ∧ seq N - 1 + 1 × F ⇝ ⇝ ⁡ seq N - 1 + 1 × F ↔ ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F
56 42 43 55 mpbi2and ⊢ φ ∧ N − 1 ∈ ℤ ≥ M → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F
57 2 1 eleqtrdi ⊢ φ → N ∈ ℤ ≥ M
58 uzm1 ⊢ N ∈ ℤ ≥ M → N = M ∨ N − 1 ∈ ℤ ≥ M
59 57 58 syl ⊢ φ → N = M ∨ N − 1 ∈ ℤ ≥ M
60 21 56 59 mpjaodan ⊢ φ → ⇝ ⁡ seq N × F ≠ 0 ∧ seq N × F ⇝ ⇝ ⁡ seq N × F