ntrivcvgfvn0

Description: Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017)

	Ref	Expression
Hypotheses	ntrivcvgfvn0.1	$⊢ Z = ℤ_{\geq M}$
	ntrivcvgfvn0.2	$⊢ φ \to N \in Z$
	ntrivcvgfvn0.3	$⊢ φ \to seq M (\times F) ⇝ X$
	ntrivcvgfvn0.4	$⊢ φ \to X \neq 0$
	ntrivcvgfvn0.5	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
Assertion	ntrivcvgfvn0	$⊢ φ \to seq M (\times F) (N) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		ntrivcvgfvn0.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvgfvn0.2	$⊢ φ \to N \in Z$
3		ntrivcvgfvn0.3	$⊢ φ \to seq M (\times F) ⇝ X$
4		ntrivcvgfvn0.4	$⊢ φ \to X \neq 0$
5		ntrivcvgfvn0.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	adantr	$⊢ (φ \land seq M (\times F) (N) = 0) \to ⇝ (seq M (\times F)) = X$
12		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
13		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
14	1 13	eqsstri	$⊢ Z \subseteq ℤ$
15	14 2	sseldi	$⊢ φ \to N \in ℤ$
16	15	adantr	$⊢ (φ \land seq M (\times F) (N) = 0) \to N \in ℤ$
17		seqex	$⊢ seq M (\times F) \in V$
18	17	a1i	$⊢ (φ \land seq M (\times F) (N) = 0) \to seq M (\times F) \in V$
19		0cnd	$⊢ (φ \land seq M (\times F) (N) = 0) \to 0 \in ℂ$
20		fveqeq2	$⊢ m = N \to (seq M (\times F) (m) = 0 \leftrightarrow seq M (\times F) (N) = 0)$
21	20	imbi2d	$⊢ m = N \to (((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (m) = 0) \leftrightarrow ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (N) = 0))$
22		fveqeq2	$⊢ m = n \to (seq M (\times F) (m) = 0 \leftrightarrow seq M (\times F) (n) = 0)$
23	22	imbi2d	$⊢ m = n \to (((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (m) = 0) \leftrightarrow ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (n) = 0))$
24		fveqeq2	$⊢ m = n + 1 \to (seq M (\times F) (m) = 0 \leftrightarrow seq M (\times F) (n + 1) = 0)$
25	24	imbi2d	$⊢ m = n + 1 \to (((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (m) = 0) \leftrightarrow ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (n + 1) = 0))$
26		fveqeq2	$⊢ m = k \to (seq M (\times F) (m) = 0 \leftrightarrow seq M (\times F) (k) = 0)$
27	26	imbi2d	$⊢ m = k \to (((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (m) = 0) \leftrightarrow ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (k) = 0))$
28		simpr	$⊢ (φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (N) = 0$
29	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
30		uztrn	$⊢ (n \in ℤ_{\geq N} \land N \in ℤ_{\geq M}) \to n \in ℤ_{\geq M}$
31	29 30	sylan2	$⊢ (n \in ℤ_{\geq N} \land φ) \to n \in ℤ_{\geq M}$
32	31	3adant3	$⊢ (n \in ℤ_{\geq N} \land φ \land seq M (\times F) (n) = 0) \to n \in ℤ_{\geq M}$
33		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
34	32 33	syl	$⊢ (n \in ℤ_{\geq N} \land φ \land seq M (\times F) (n) = 0) \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
35		oveq1	$⊢ seq M (\times F) (n) = 0 \to seq M (\times F) (n) F (n + 1) = 0 \cdot F (n + 1)$
36	35	3ad2ant3	$⊢ (n \in ℤ_{\geq N} \land φ \land seq M (\times F) (n) = 0) \to seq M (\times F) (n) F (n + 1) = 0 \cdot F (n + 1)$
37		peano2uz	$⊢ n \in ℤ_{\geq N} \to n + 1 \in ℤ_{\geq N}$
38	1	uztrn2	$⊢ (N \in Z \land n + 1 \in ℤ_{\geq N}) \to n + 1 \in Z$
39	2 37 38	syl2an	$⊢ (φ \land n \in ℤ_{\geq N}) \to n + 1 \in Z$
40	5	ralrimiva	$⊢ φ \to \forall k \in Z F (k) \in ℂ$
41		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
42	41	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℂ \leftrightarrow F (n + 1) \in ℂ)$
43	42	rspcv	$⊢ n + 1 \in Z \to (\forall k \in Z F (k) \in ℂ \to F (n + 1) \in ℂ)$
44	40 43	mpan9	$⊢ (φ \land n + 1 \in Z) \to F (n + 1) \in ℂ$
45	39 44	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to F (n + 1) \in ℂ$
46	45	ancoms	$⊢ (n \in ℤ_{\geq N} \land φ) \to F (n + 1) \in ℂ$
47	46	mul02d	$⊢ (n \in ℤ_{\geq N} \land φ) \to 0 \cdot F (n + 1) = 0$
48	47	3adant3	$⊢ (n \in ℤ_{\geq N} \land φ \land seq M (\times F) (n) = 0) \to 0 \cdot F (n + 1) = 0$
49	34 36 48	3eqtrd	$⊢ (n \in ℤ_{\geq N} \land φ \land seq M (\times F) (n) = 0) \to seq M (\times F) (n + 1) = 0$
50	49	3exp	$⊢ n \in ℤ_{\geq N} \to (φ \to (seq M (\times F) (n) = 0 \to seq M (\times F) (n + 1) = 0))$
51	50	adantrd	$⊢ n \in ℤ_{\geq N} \to ((φ \land seq M (\times F) (N) = 0) \to (seq M (\times F) (n) = 0 \to seq M (\times F) (n + 1) = 0))$
52	51	a2d	$⊢ n \in ℤ_{\geq N} \to (((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (n) = 0) \to ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (n + 1) = 0))$
53	21 23 25 27 28 52	uzind4i	$⊢ k \in ℤ_{\geq N} \to ((φ \land seq M (\times F) (N) = 0) \to seq M (\times F) (k) = 0)$
54	53	impcom	$⊢ ((φ \land seq M (\times F) (N) = 0) \land k \in ℤ_{\geq N}) \to seq M (\times F) (k) = 0$
55	12 16 18 19 54	climconst	$⊢ (φ \land seq M (\times F) (N) = 0) \to seq M (\times F) ⇝ 0$
56		funbrfv	$⊢ Fun ⇝ \to (seq M (\times F) ⇝ 0 \to ⇝ (seq M (\times F)) = 0)$
57	8 55 56	mpsyl	$⊢ (φ \land seq M (\times F) (N) = 0) \to ⇝ (seq M (\times F)) = 0$
58	11 57	eqtr3d	$⊢ (φ \land seq M (\times F) (N) = 0) \to X = 0$
59	58	ex	$⊢ φ \to (seq M (\times F) (N) = 0 \to X = 0)$
60	59	necon3d	$⊢ φ \to (X \neq 0 \to seq M (\times F) (N) \neq 0)$
61	4 60	mpd	$⊢ φ \to seq M (\times F) (N) \neq 0$

Metamath Proof Explorer

Theorem ntrivcvgfvn0

Proof