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 sselid φ 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