ntrivcvgn0

Description: A product that converges to a nonzero value converges non-trivially. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	ntrivcvgn0.1	$⊢ Z = ℤ_{\geq M}$
	ntrivcvgn0.2	$⊢ φ \to M \in ℤ$
	ntrivcvgn0.3	$⊢ φ \to seq M (\times F) ⇝ X$
	ntrivcvgn0.4	$⊢ φ \to X \neq 0$
Assertion	ntrivcvgn0	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$

Step	Hyp	Ref	Expression
1		ntrivcvgn0.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvgn0.2	$⊢ φ \to M \in ℤ$
3		ntrivcvgn0.3	$⊢ φ \to seq M (\times F) ⇝ X$
4		ntrivcvgn0.4	$⊢ φ \to X \neq 0$
5	2	uzidd	$⊢ φ \to M \in ℤ_{\geq M}$
6	5 1	eleqtrrdi	$⊢ φ \to M \in Z$
7		climrel	$⊢ Rel ⇝$
8	7	brrelex2i	$⊢ seq M (\times F) ⇝ X \to X \in V$
9	3 8	syl	$⊢ φ \to X \in V$
10	4 3	jca	$⊢ φ \to (X \neq 0 \land seq M (\times F) ⇝ X)$
11		neeq1	$⊢ y = X \to (y \neq 0 \leftrightarrow X \neq 0)$
12		breq2	$⊢ y = X \to (seq M (\times F) ⇝ y \leftrightarrow seq M (\times F) ⇝ X)$
13	11 12	anbi12d	$⊢ y = X \to ((y \neq 0 \land seq M (\times F) ⇝ y) \leftrightarrow (X \neq 0 \land seq M (\times F) ⇝ X))$
14	9 10 13	spcedv	$⊢ φ \to \exists y (y \neq 0 \land seq M (\times F) ⇝ y)$
15		seqeq1	$⊢ n = M \to seq n (\times F) = seq M (\times F)$
16	15	breq1d	$⊢ n = M \to (seq n (\times F) ⇝ y \leftrightarrow seq M (\times F) ⇝ y)$
17	16	anbi2d	$⊢ n = M \to ((y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow (y \neq 0 \land seq M (\times F) ⇝ y))$
18	17	exbidv	$⊢ n = M \to (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \leftrightarrow \exists y (y \neq 0 \land seq M (\times F) ⇝ y))$
19	18	rspcev	$⊢ (M \in Z \land \exists y (y \neq 0 \land seq M (\times F) ⇝ y)) \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
20	6 14 19	syl2anc	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$

Metamath Proof Explorer