Metamath Proof Explorer


Theorem climfsum

Description: Limit of a finite sum of converging sequences. Note that F ( k ) is a collection of functions with implicit parameter k , each of which converges to B ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-Jul-2014) (Proof shortened by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses climfsum.1 𝑍 = ( ℤ𝑀 )
climfsum.2 ( 𝜑𝑀 ∈ ℤ )
climfsum.3 ( 𝜑𝐴 ∈ Fin )
climfsum.5 ( ( 𝜑𝑘𝐴 ) → 𝐹𝐵 )
climfsum.6 ( 𝜑𝐻𝑊 )
climfsum.7 ( ( 𝜑 ∧ ( 𝑘𝐴𝑛𝑍 ) ) → ( 𝐹𝑛 ) ∈ ℂ )
climfsum.8 ( ( 𝜑𝑛𝑍 ) → ( 𝐻𝑛 ) = Σ 𝑘𝐴 ( 𝐹𝑛 ) )
Assertion climfsum ( 𝜑𝐻 ⇝ Σ 𝑘𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 climfsum.1 𝑍 = ( ℤ𝑀 )
2 climfsum.2 ( 𝜑𝑀 ∈ ℤ )
3 climfsum.3 ( 𝜑𝐴 ∈ Fin )
4 climfsum.5 ( ( 𝜑𝑘𝐴 ) → 𝐹𝐵 )
5 climfsum.6 ( 𝜑𝐻𝑊 )
6 climfsum.7 ( ( 𝜑 ∧ ( 𝑘𝐴𝑛𝑍 ) ) → ( 𝐹𝑛 ) ∈ ℂ )
7 climfsum.8 ( ( 𝜑𝑛𝑍 ) → ( 𝐻𝑛 ) = Σ 𝑘𝐴 ( 𝐹𝑛 ) )
8 7 mpteq2dva ( 𝜑 → ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) ) = ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) )
9 uzssz ( ℤ𝑀 ) ⊆ ℤ
10 1 9 eqsstri 𝑍 ⊆ ℤ
11 zssre ℤ ⊆ ℝ
12 10 11 sstri 𝑍 ⊆ ℝ
13 12 a1i ( 𝜑𝑍 ⊆ ℝ )
14 fvexd ( ( 𝜑 ∧ ( 𝑛𝑍𝑘𝐴 ) ) → ( 𝐹𝑛 ) ∈ V )
15 2 adantr ( ( 𝜑𝑘𝐴 ) → 𝑀 ∈ ℤ )
16 climrel Rel ⇝
17 16 brrelex1i ( 𝐹𝐵𝐹 ∈ V )
18 4 17 syl ( ( 𝜑𝑘𝐴 ) → 𝐹 ∈ V )
19 eqid ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) = ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) )
20 1 19 climmpt ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ V ) → ( 𝐹𝐵 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐵 ) )
21 15 18 20 syl2anc ( ( 𝜑𝑘𝐴 ) → ( 𝐹𝐵 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐵 ) )
22 4 21 mpbid ( ( 𝜑𝑘𝐴 ) → ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐵 )
23 6 anassrs ( ( ( 𝜑𝑘𝐴 ) ∧ 𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ ℂ )
24 23 fmpttd ( ( 𝜑𝑘𝐴 ) → ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) : 𝑍 ⟶ ℂ )
25 1 15 24 rlimclim ( ( 𝜑𝑘𝐴 ) → ( ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝𝑟 𝐵 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐵 ) )
26 22 25 mpbird ( ( 𝜑𝑘𝐴 ) → ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝𝑟 𝐵 )
27 13 3 14 26 fsumrlim ( 𝜑 → ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) ⇝𝑟 Σ 𝑘𝐴 𝐵 )
28 3 adantr ( ( 𝜑𝑛𝑍 ) → 𝐴 ∈ Fin )
29 6 anass1rs ( ( ( 𝜑𝑛𝑍 ) ∧ 𝑘𝐴 ) → ( 𝐹𝑛 ) ∈ ℂ )
30 28 29 fsumcl ( ( 𝜑𝑛𝑍 ) → Σ 𝑘𝐴 ( 𝐹𝑛 ) ∈ ℂ )
31 30 fmpttd ( 𝜑 → ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) : 𝑍 ⟶ ℂ )
32 1 2 31 rlimclim ( 𝜑 → ( ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) ⇝𝑟 Σ 𝑘𝐴 𝐵 ↔ ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) ⇝ Σ 𝑘𝐴 𝐵 ) )
33 27 32 mpbid ( 𝜑 → ( 𝑛𝑍 ↦ Σ 𝑘𝐴 ( 𝐹𝑛 ) ) ⇝ Σ 𝑘𝐴 𝐵 )
34 8 33 eqbrtrd ( 𝜑 → ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) ) ⇝ Σ 𝑘𝐴 𝐵 )
35 eqid ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) ) = ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) )
36 1 35 climmpt ( ( 𝑀 ∈ ℤ ∧ 𝐻𝑊 ) → ( 𝐻 ⇝ Σ 𝑘𝐴 𝐵 ↔ ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) ) ⇝ Σ 𝑘𝐴 𝐵 ) )
37 2 5 36 syl2anc ( 𝜑 → ( 𝐻 ⇝ Σ 𝑘𝐴 𝐵 ↔ ( 𝑛𝑍 ↦ ( 𝐻𝑛 ) ) ⇝ Σ 𝑘𝐴 𝐵 ) )
38 34 37 mpbird ( 𝜑𝐻 ⇝ Σ 𝑘𝐴 𝐵 )