Metamath Proof Explorer

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 syl6bi ⊢ ( 𝑛 = 𝑀 → ( 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 ⇝ )