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	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝑁 − 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 𝑁 ( · , 𝐹 ) ) ) )