Theorem ntrivcvg

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

	Ref	Expression
Hypotheses	ntrivcvg.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	ntrivcvg.2	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
	ntrivcvg.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion	ntrivcvg	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )

Proof

Step	Hyp	Ref	Expression
1		ntrivcvg.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		ntrivcvg.2	⊢ ( 𝜑 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
3		ntrivcvg.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4		uzm1	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑛 = 𝑀 ∨ ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
5	4 1	eleq2s	⊢ ( 𝑛 ∈ 𝑍 → ( 𝑛 = 𝑀 ∨ ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
6	5	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → ( 𝑛 = 𝑀 ∨ ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
7		seqeq1	⊢ ( 𝑛 = 𝑀 → seq 𝑛 ( · , 𝐹 ) = seq 𝑀 ( · , 𝐹 ) )
8	7	breq1d	⊢ ( 𝑛 = 𝑀 → ( seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ↔ seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 ) )
9		seqex	⊢ seq 𝑀 ( · , 𝐹 ) ∈ V
10		vex	⊢ 𝑦 ∈ V
11	9 10	breldm	⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ 𝑦 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
12	8 11	biimtrdi	⊢ ( 𝑛 = 𝑀 → ( seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
13	12	adantld	⊢ ( 𝑛 = 𝑀 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
14		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → ( 𝑛 − 1 ) ∈ 𝑍 )
15	3	ad5ant15	⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
17	1 16	eqsstri	⊢ 𝑍 ⊆ ℤ
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
19	17 18	sselid	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → 𝑛 ∈ ℤ )
20	19	zcnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → 𝑛 ∈ ℂ )
21		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → 1 ∈ ℂ )
22	20 21	npcand	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
23	22	seqeq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → seq ( ( 𝑛 − 1 ) + 1 ) ( · , 𝐹 ) = seq 𝑛 ( · , 𝐹 ) )
24	23	breq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → ( seq ( ( 𝑛 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ 𝑦 ↔ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) )
25	24	biimpar	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq ( ( 𝑛 − 1 ) + 1 ) ( · , 𝐹 ) ⇝ 𝑦 )
26	1 14 15 25	clim2prod	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ⇝ ( ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 − 1 ) ) · 𝑦 ) )
27		ovex	⊢ ( ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 − 1 ) ) · 𝑦 ) ∈ V
28	9 27	breldm	⊢ ( seq 𝑀 ( · , 𝐹 ) ⇝ ( ( seq 𝑀 ( · , 𝐹 ) ‘ ( 𝑛 − 1 ) ) · 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
29	26 28	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
30	29	an32s	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) ∧ ( 𝑛 − 1 ) ∈ 𝑍 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
31	30	expcom	⊢ ( ( 𝑛 − 1 ) ∈ 𝑍 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
32	1	eqcomi	⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
33	31 32	eleq2s	⊢ ( ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
34	13 33	jaoi	⊢ ( ( 𝑛 = 𝑀 ∨ ( 𝑛 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
35	6 34	mpcom	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )
36	35	ex	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
37	36	adantld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
38	37	exlimdv	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
39	38	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝑍 ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , 𝐹 ) ⇝ 𝑦 ) → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ ) )
40	2 39	mpd	⊢ ( 𝜑 → seq 𝑀 ( · , 𝐹 ) ∈ dom ⇝ )