Metamath Proof Explorer

Theorem fsumcvg4

Description: A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fsumcvg4.s ⊢ 𝑆 = ( ℤ≥ ‘ 𝑀 )
fsumcvg4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fsumcvg4.c ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
fsumcvg4.f ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∈ Fin )
Assertion fsumcvg4 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 fsumcvg4.s ⊢ 𝑆 = ( ℤ≥ ‘ 𝑀 )
2 fsumcvg4.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fsumcvg4.c ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
4 fsumcvg4.f ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∈ Fin )
5 ffun ⊢ ( 𝐹 : 𝑆 ⟶ ℂ → Fun 𝐹 )
6 difpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) = ( ( ◡ 𝐹 “ ℂ ) ∖ ( ◡ 𝐹 “ { 0 } ) ) )
7 3 5 6 3syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) = ( ( ◡ 𝐹 “ ℂ ) ∖ ( ◡ 𝐹 “ { 0 } ) ) )
8 difss ⊢ ( ( ◡ 𝐹 “ ℂ ) ∖ ( ◡ 𝐹 “ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ℂ )
9 7 8 eqsstrdi ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ⊆ ( ◡ 𝐹 “ ℂ ) )
10 fimacnv ⊢ ( 𝐹 : 𝑆 ⟶ ℂ → ( ◡ 𝐹 “ ℂ ) = 𝑆 )
11 3 10 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ℂ ) = 𝑆 )
12 9 11 sseqtrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ⊆ 𝑆 )
13 exmidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∨ ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ) )
14 eqid ⊢ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 )
15 14 biantru ⊢ ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) )
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) ) )
17 1 fvexi ⊢ 𝑆 ∈ V
18 17 a1i ⊢ ( 𝜑 → 𝑆 ∈ V )
19 0nn0 ⊢ 0 ∈ ℕ0
20 19 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
21 eqid ⊢ ( ℂ ∖ { 0 } ) = ( ℂ ∖ { 0 } )
22 21 ffs2 ⊢ ( ( 𝑆 ∈ V ∧ 0 ∈ ℕ0 ∧ 𝐹 : 𝑆 ⟶ ℂ ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) )
23 18 20 3 22 syl3anc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) )
24 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
25 suppvalfn ⊢ ( ( 𝐹 Fn 𝑆 ∧ 𝑆 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝐹 supp 0 ) = { 𝑘 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
26 24 18 20 25 syl3anc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = { 𝑘 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
27 23 26 eqtr3d ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) = { 𝑘 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
28 27 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ 𝑘 ∈ { 𝑘 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ) )
29 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝑆 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ↔ ( 𝑘 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
30 28 29 bitrdi ⊢ ( 𝜑 → ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝑘 ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) ) )
31 30 baibd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
32 31 necon2bbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) = 0 ↔ ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ) )
33 32 biimprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ‘ 𝑘 ) = 0 ) )
34 33 pm4.71d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ↔ ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = 0 ) ) )
35 16 34 orbi12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∨ ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ) ↔ ( ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) ∨ ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = 0 ) ) ) )
36 13 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) ∨ ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = 0 ) ) )
37 eqif ⊢ ( ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) , ( 𝐹 ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) ∨ ( ¬ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ∧ ( 𝐹 ‘ 𝑘 ) = 0 ) ) )
38 36 37 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) , ( 𝐹 ‘ 𝑘 ) , 0 ) )
39 12 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ) → 𝑘 ∈ 𝑆 )
40 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
41 39 40 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ◡ 𝐹 “ ( ℂ ∖ { 0 } ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
42 1 2 4 12 38 41 fsumcvg3 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )