ntrivcvg

Description: A non-trivially converging infinite product converges. (Contributed by Scott Fenton, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ntrivcvg.1	$⊢ Z = ℤ_{\geq M}$
2		ntrivcvg.2	$⊢ φ \to \exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y)$
3		ntrivcvg.3	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
4		uzm1	$⊢ n \in ℤ_{\geq M} \to (n = M \lor n - 1 \in ℤ_{\geq M})$
5	4 1	eleq2s	$⊢ n \in Z \to (n = M \lor n - 1 \in ℤ_{\geq M})$
6	5	ad2antlr	$⊢ ((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to (n = M \lor n - 1 \in ℤ_{\geq M})$
7		seqeq1	$⊢ n = M \to seq n (\times F) = seq M (\times F)$
8	7	breq1d	$⊢ n = M \to (seq n (\times F) ⇝ y \leftrightarrow seq M (\times F) ⇝ y)$
9		seqex	$⊢ seq M (\times F) \in V$
10		vex	$⊢ y \in V$
11	9 10	breldm	$⊢ seq M (\times F) ⇝ y \to seq M (\times F) \in dom ⇝$
12	8 11	syl6bi	$⊢ n = M \to (seq n (\times F) ⇝ y \to seq M (\times F) \in dom ⇝)$
13	12	adantld	$⊢ n = M \to (((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
14		simplr	$⊢ (((φ \land n \in Z) \land n - 1 \in Z) \land seq n (\times F) ⇝ y) \to n - 1 \in Z$
15	3	ad5ant15	$⊢ ((((φ \land n \in Z) \land n - 1 \in Z) \land seq n (\times F) ⇝ y) \land k \in Z) \to F (k) \in ℂ$
16		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
17	1 16	eqsstri	$⊢ Z \subseteq ℤ$
18		simplr	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to n \in Z$
19	17 18	sseldi	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to n \in ℤ$
20	19	zcnd	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to n \in ℂ$
21		1cnd	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to 1 \in ℂ$
22	20 21	npcand	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to n - 1 + 1 = n$
23	22	seqeq1d	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to seq (n - 1 + 1) (\times F) = seq n (\times F)$
24	23	breq1d	$⊢ ((φ \land n \in Z) \land n - 1 \in Z) \to (seq (n - 1 + 1) (\times F) ⇝ y \leftrightarrow seq n (\times F) ⇝ y)$
25	24	biimpar	$⊢ (((φ \land n \in Z) \land n - 1 \in Z) \land seq n (\times F) ⇝ y) \to seq (n - 1 + 1) (\times F) ⇝ y$
26	1 14 15 25	clim2prod	$⊢ (((φ \land n \in Z) \land n - 1 \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) ⇝ seq M (\times F) (n - 1) y$
27		ovex	$⊢ seq M (\times F) (n - 1) y \in V$
28	9 27	breldm	$⊢ seq M (\times F) ⇝ seq M (\times F) (n - 1) y \to seq M (\times F) \in dom ⇝$
29	26 28	syl	$⊢ (((φ \land n \in Z) \land n - 1 \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝$
30	29	an32s	$⊢ (((φ \land n \in Z) \land seq n (\times F) ⇝ y) \land n - 1 \in Z) \to seq M (\times F) \in dom ⇝$
31	30	expcom	$⊢ n - 1 \in Z \to (((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
32	1	eqcomi	$⊢ ℤ_{\geq M} = Z$
33	31 32	eleq2s	$⊢ n - 1 \in ℤ_{\geq M} \to (((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
34	13 33	jaoi	$⊢ (n = M \lor n - 1 \in ℤ_{\geq M}) \to (((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
35	6 34	mpcom	$⊢ ((φ \land n \in Z) \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝$
36	35	ex	$⊢ (φ \land n \in Z) \to (seq n (\times F) ⇝ y \to seq M (\times F) \in dom ⇝)$
37	36	adantld	$⊢ (φ \land n \in Z) \to ((y \neq 0 \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
38	37	exlimdv	$⊢ (φ \land n \in Z) \to (\exists y (y \neq 0 \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
39	38	rexlimdva	$⊢ φ \to (\exists n \in Z \exists y (y \neq 0 \land seq n (\times F) ⇝ y) \to seq M (\times F) \in dom ⇝)$
40	2 39	mpd	$⊢ φ \to seq M (\times F) \in dom ⇝$

Metamath Proof Explorer

Theorem ntrivcvg

Proof