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 = ℤ_{\geq M}$
	ntrivcvgtail.2	$⊢ φ \to N \in Z$
	ntrivcvgtail.3	$⊢ φ \to seq M (\times F) ⇝ X$
	ntrivcvgtail.4	$⊢ φ \to X \neq 0$
	ntrivcvgtail.5	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
Assertion	ntrivcvgtail	$⊢ φ \to (⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F)))$

Proof

Step	Hyp	Ref	Expression
1		ntrivcvgtail.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvgtail.2	$⊢ φ \to N \in Z$
3		ntrivcvgtail.3	$⊢ φ \to seq M (\times F) ⇝ X$
4		ntrivcvgtail.4	$⊢ φ \to X \neq 0$
5		ntrivcvgtail.5	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
6		fclim	$⊢ ⇝ : dom ⇝ ⟶ ℂ$
7		ffun	$⊢ ⇝ : dom ⇝ ⟶ ℂ \to Fun ⇝$
8	6 7	ax-mp	$⊢ Fun ⇝$
9		funbrfv	$⊢ Fun ⇝ \to (seq M (\times F) ⇝ X \to ⇝ (seq M (\times F)) = X)$
10	8 3 9	mpsyl	$⊢ φ \to ⇝ (seq M (\times F)) = X$
11	10 4	eqnetrd	$⊢ φ \to ⇝ (seq M (\times F)) \neq 0$
12	3 10	breqtrrd	$⊢ φ \to seq M (\times F) ⇝ ⇝ (seq M (\times F))$
13	11 12	jca	$⊢ φ \to (⇝ (seq M (\times F)) \neq 0 \land seq M (\times F) ⇝ ⇝ (seq M (\times F)))$
14	13	adantr	$⊢ (φ \land N = M) \to (⇝ (seq M (\times F)) \neq 0 \land seq M (\times F) ⇝ ⇝ (seq M (\times F)))$
15		seqeq1	$⊢ N = M \to seq N (\times F) = seq M (\times F)$
16	15	fveq2d	$⊢ N = M \to ⇝ (seq N (\times F)) = ⇝ (seq M (\times F))$
17	16	neeq1d	$⊢ N = M \to (⇝ (seq N (\times F)) \neq 0 \leftrightarrow ⇝ (seq M (\times F)) \neq 0)$
18	15 16	breq12d	$⊢ N = M \to (seq N (\times F) ⇝ ⇝ (seq N (\times F)) \leftrightarrow seq M (\times F) ⇝ ⇝ (seq M (\times F)))$
19	17 18	anbi12d	$⊢ N = M \to ((⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F))) \leftrightarrow (⇝ (seq M (\times F)) \neq 0 \land seq M (\times F) ⇝ ⇝ (seq M (\times F))))$
20	19	adantl	$⊢ (φ \land N = M) \to ((⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F))) \leftrightarrow (⇝ (seq M (\times F)) \neq 0 \land seq M (\times F) ⇝ ⇝ (seq M (\times F))))$
21	14 20	mpbird	$⊢ (φ \land N = M) \to (⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F)))$
22		simpr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in ℤ_{\geq M}$
23	22 1	eleqtrrdi	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 \in Z$
24	5	adantlr	$⊢ ((φ \land N - 1 \in ℤ_{\geq M}) \land k \in Z) \to F (k) \in ℂ$
25	3	adantr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq M (\times F) ⇝ X$
26	4	adantr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to X \neq 0$
27	1 23 25 26 24	ntrivcvgfvn0	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq M (\times F) (N - 1) \neq 0$
28	1 23 24 25 27	clim2div	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq (N - 1 + 1) (\times F) ⇝ (\frac{X}{seq M (\times F) (N - 1)})$
29		funbrfv	$⊢ Fun ⇝ \to (seq (N - 1 + 1) (\times F) ⇝ (\frac{X}{seq M (\times F) (N - 1)}) \to ⇝ (seq (N - 1 + 1) (\times F)) = \frac{X}{seq M (\times F) (N - 1)})$
30	8 28 29	mpsyl	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to ⇝ (seq (N - 1 + 1) (\times F)) = \frac{X}{seq M (\times F) (N - 1)}$
31		climcl	$⊢ seq M (\times F) ⇝ X \to X \in ℂ$
32	3 31	syl	$⊢ φ \to X \in ℂ$
33	32	adantr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to X \in ℂ$
34		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
35	34 1	eleq2s	$⊢ N \in Z \to M \in ℤ$
36	2 35	syl	$⊢ φ \to M \in ℤ$
37	1 36 5	prodf	$⊢ φ \to seq M (\times F) : Z ⟶ ℂ$
38	1	feq2i	$⊢ seq M (\times F) : Z ⟶ ℂ \leftrightarrow seq M (\times F) : ℤ_{\geq M} ⟶ ℂ$
39	37 38	sylib	$⊢ φ \to seq M (\times F) : ℤ_{\geq M} ⟶ ℂ$
40	39	ffvelcdmda	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq M (\times F) (N - 1) \in ℂ$
41	33 40 26 27	divne0d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to \frac{X}{seq M (\times F) (N - 1)} \neq 0$
42	30 41	eqnetrd	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to ⇝ (seq (N - 1 + 1) (\times F)) \neq 0$
43	28 30	breqtrrd	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq (N - 1 + 1) (\times F) ⇝ ⇝ (seq (N - 1 + 1) (\times F))$
44		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
45	1 44	eqsstri	$⊢ Z \subseteq ℤ$
46	45 2	sselid	$⊢ φ \to N \in ℤ$
47	46	zcnd	$⊢ φ \to N \in ℂ$
48	47	adantr	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N \in ℂ$
49		1cnd	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to 1 \in ℂ$
50	48 49	npcand	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to N - 1 + 1 = N$
51	50	seqeq1d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to seq (N - 1 + 1) (\times F) = seq N (\times F)$
52	51	fveq2d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to ⇝ (seq (N - 1 + 1) (\times F)) = ⇝ (seq N (\times F))$
53	52	neeq1d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to (⇝ (seq (N - 1 + 1) (\times F)) \neq 0 \leftrightarrow ⇝ (seq N (\times F)) \neq 0)$
54	51 52	breq12d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to (seq (N - 1 + 1) (\times F) ⇝ ⇝ (seq (N - 1 + 1) (\times F)) \leftrightarrow seq N (\times F) ⇝ ⇝ (seq N (\times F)))$
55	53 54	anbi12d	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to ((⇝ (seq (N - 1 + 1) (\times F)) \neq 0 \land seq (N - 1 + 1) (\times F) ⇝ ⇝ (seq (N - 1 + 1) (\times F))) \leftrightarrow (⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F))))$
56	42 43 55	mpbi2and	$⊢ (φ \land N - 1 \in ℤ_{\geq M}) \to (⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F)))$
57	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
58		uzm1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N - 1 \in ℤ_{\geq M})$
59	57 58	syl	$⊢ φ \to (N = M \lor N - 1 \in ℤ_{\geq M})$
60	21 56 59	mpjaodan	$⊢ φ \to (⇝ (seq N (\times F)) \neq 0 \land seq N (\times F) ⇝ ⇝ (seq N (\times F)))$

Metamath Proof Explorer

Theorem ntrivcvgtail

Proof