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 sselid ( 𝜑𝑁 ∈ ℤ )
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 𝑁 ( · , 𝐹 ) ) ) )