Metamath Proof Explorer

Theorem mertens

Description: Mertens' theorem. If A ( j ) is an absolutely convergent series and B ( k ) is convergent, then ( sum_ j e. NN0 A ( j ) x. sum_ k e. NN0 B ( k ) ) = sum_ k e. NN0 sum_ j e. ( 0 ... k ) ( A ( j ) x. B ( k - j ) ) (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem . (Contributed by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses mertens.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
mertens.2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
mertens.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
mertens.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
mertens.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
mertens.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
mertens.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
mertens.8 ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
Assertion mertens ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( Σ 𝑗 ∈ ℕ0 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mertens.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
2 mertens.2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
3 mertens.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
4 mertens.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
5 mertens.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
6 mertens.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
7 mertens.7 ⊢ ( 𝜑 → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
8 mertens.8 ⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
11 seqex ⊢ seq 0 ( + , 𝐻 ) ∈ V
12 11 a1i ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ∈ V )
13 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
14 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝜑 )
15 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → 𝑗 ∈ ℕ0 )
16 14 15 3 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝐴 ∈ ℂ )
17 fveq2 ⊢ ( 𝑖 = ( 𝑘 − 𝑗 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) )
18 17 eleq1d ⊢ ( 𝑖 = ( 𝑘 − 𝑗 ) → ( ( 𝐺 ‘ 𝑖 ) ∈ ℂ ↔ ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ∈ ℂ ) )
19 4 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
20 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
21 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑖 ) )
22 21 eleq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐺 ‘ 𝑖 ) ∈ ℂ ) )
23 22 cbvralvw ⊢ ( ∀ 𝑘 ∈ ℕ0 ( 𝐺 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑖 ∈ ℕ0 ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
24 20 23 sylib ⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ0 ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ∀ 𝑖 ∈ ℕ0 ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
26 fznn0sub ⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → ( 𝑘 − 𝑗 ) ∈ ℕ0 )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑗 ) ∈ ℕ0 )
28 18 25 27 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ∈ ℂ )
29 16 28 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) ∈ ℂ )
30 13 29 fsumcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) ∈ ℂ )
31 6 30 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) ∈ ℂ )
32 9 10 31 serf ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) : ℕ0 ⟶ ℂ )
33 32 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ∈ ℂ )
34 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = 𝐴 )
35 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ 𝐴 ) )
36 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
37 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
38 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
39 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
40 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → seq 0 ( + , 𝐾 ) ∈ dom ⇝ )
41 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
43 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐺 ‘ 𝑙 ) = ( 𝐺 ‘ 𝑘 ) )
44 43 cbvsumv ⊢ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑘 )
45 fvoveq1 ⊢ ( 𝑖 = 𝑛 → ( ℤ≥ ‘ ( 𝑖 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
46 45 sumeq1d ⊢ ( 𝑖 = 𝑛 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
47 44 46 eqtrid ⊢ ( 𝑖 = 𝑛 → Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
48 47 fveq2d ⊢ ( 𝑖 = 𝑛 → ( abs ‘ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
49 48 eqeq2d ⊢ ( 𝑖 = 𝑛 → ( 𝑢 = ( abs ‘ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) ) ↔ 𝑢 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑢 = ( abs ‘ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑢 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
51 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
52 51 rexbidv ⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑢 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
53 50 52 bitrid ⊢ ( 𝑢 = 𝑧 → ( ∃ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑢 = ( abs ‘ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
54 53 cbvabv ⊢ { 𝑢 ∣ ∃ 𝑖 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑢 = ( abs ‘ Σ 𝑙 ∈ ( ℤ≥ ‘ ( 𝑖 + 1 ) ) ( 𝐺 ‘ 𝑙 ) ) } = { 𝑧 ∣ ∃ 𝑛 ∈ ( 0 ... ( 𝑠 − 1 ) ) 𝑧 = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) }
55 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐾 ‘ 𝑖 ) = ( 𝐾 ‘ 𝑗 ) )
56 55 cbvsumv ⊢ Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) = Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 )
57 56 oveq1i ⊢ ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) = ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 )
58 57 oveq2i ⊢ ( ( 𝑥 / 2 ) / ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) ) = ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) )
59 58 breq2i ⊢ ( ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
60 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑘 ) )
61 60 cbvsumv ⊢ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑘 )
62 fvoveq1 ⊢ ( 𝑢 = 𝑛 → ( ℤ≥ ‘ ( 𝑢 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
63 62 sumeq1d ⊢ ( 𝑢 = 𝑛 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
64 61 63 eqtrid ⊢ ( 𝑢 = 𝑛 → Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) )
65 64 fveq2d ⊢ ( 𝑢 = 𝑛 → ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) = ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) )
66 65 breq1d ⊢ ( 𝑢 = 𝑛 → ( ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
67 59 66 bitrid ⊢ ( 𝑢 = 𝑛 → ( ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) ) ↔ ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
68 67 cbvralvw ⊢ ( ∀ 𝑢 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) )
69 68 anbi2i ⊢ ( ( 𝑠 ∈ ℕ ∧ ∀ 𝑢 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝑢 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑖 ∈ ℕ0 ( 𝐾 ‘ 𝑖 ) + 1 ) ) ) ↔ ( 𝑠 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑠 ) ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐺 ‘ 𝑘 ) ) < ( ( 𝑥 / 2 ) / ( Σ 𝑗 ∈ ℕ0 ( 𝐾 ‘ 𝑗 ) + 1 ) ) ) )
70 34 35 36 37 38 39 40 41 42 54 69 mertenslem2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 )
71 eluznn0 ⊢ ( ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ) → 𝑚 ∈ ℕ0 )
72 fzfid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 0 ... 𝑚 ) ∈ Fin )
73 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → 𝜑 )
74 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑚 ) → 𝑗 ∈ ℕ0 )
75 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → 𝑗 ∈ ℕ0 )
76 9 10 4 5 8 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
78 1 3 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
79 77 78 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
80 73 75 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) ∈ ℂ )
81 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 0 ... ( 𝑚 − 𝑗 ) ) ∈ Fin )
82 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → 𝜑 )
83 74 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → 𝑗 ∈ ℕ0 )
84 82 83 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → 𝐴 ∈ ℂ )
85 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) → 𝑘 ∈ ℕ0 )
86 85 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → 𝑘 ∈ ℕ0 )
87 82 86 19 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
88 84 87 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
89 81 88 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
90 72 80 89 fsumsub ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑗 ∈ ( 0 ... 𝑚 ) Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) )
91 73 75 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → 𝐴 ∈ ℂ )
92 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ℕ0 𝐵 ∈ ℂ )
93 81 87 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
94 91 92 93 subdid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝐴 · ( Σ 𝑘 ∈ ℕ0 𝐵 − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) ) = ( ( 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) − ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) ) )
95 eqid ⊢ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) = ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) )
96 fznn0sub ⊢ ( 𝑗 ∈ ( 0 ... 𝑚 ) → ( 𝑚 − 𝑗 ) ∈ ℕ0 )
97 96 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝑚 − 𝑗 ) ∈ ℕ0 )
98 peano2nn0 ⊢ ( ( 𝑚 − 𝑗 ) ∈ ℕ0 → ( ( 𝑚 − 𝑗 ) + 1 ) ∈ ℕ0 )
99 97 98 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝑚 − 𝑗 ) + 1 ) ∈ ℕ0 )
100 99 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝑚 − 𝑗 ) + 1 ) ∈ ℤ )
101 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) ) → 𝜑 )
102 eluznn0 ⊢ ( ( ( ( 𝑚 − 𝑗 ) + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) ) → 𝑘 ∈ ℕ0 )
103 99 102 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) ) → 𝑘 ∈ ℕ0 )
104 101 103 4 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
105 101 103 5 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) ) → 𝐵 ∈ ℂ )
106 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
107 73 4 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
108 73 5 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
109 107 108 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
110 9 99 109 iserex ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( seq 0 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq ( ( 𝑚 − 𝑗 ) + 1 ) ( + , 𝐺 ) ∈ dom ⇝ ) )
111 106 110 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → seq ( ( 𝑚 − 𝑗 ) + 1 ) ( + , 𝐺 ) ∈ dom ⇝ )
112 95 100 104 105 111 isumcl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ∈ ℂ )
113 9 95 99 107 108 106 isumsplit ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( Σ 𝑘 ∈ ( 0 ... ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
114 97 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝑚 − 𝑗 ) ∈ ℂ )
115 ax-1cn ⊢ 1 ∈ ℂ
116 pncan ⊢ ( ( ( 𝑚 − 𝑗 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) = ( 𝑚 − 𝑗 ) )
117 114 115 116 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) = ( 𝑚 − 𝑗 ) )
118 117 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 0 ... ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) ) = ( 0 ... ( 𝑚 − 𝑗 ) ) )
119 118 sumeq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 0 ... ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) ) 𝐵 = Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) 𝐵 )
120 82 86 4 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
121 120 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) 𝐵 )
122 119 121 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ( 0 ... ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) ) 𝐵 = Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) )
123 122 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( Σ 𝑘 ∈ ( 0 ... ( ( ( 𝑚 − 𝑗 ) + 1 ) − 1 ) ) 𝐵 + Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
124 113 123 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑘 ∈ ℕ0 𝐵 = ( Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
125 93 112 124 mvrladdd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( Σ 𝑘 ∈ ℕ0 𝐵 − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 )
126 125 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝐴 · ( Σ 𝑘 ∈ ℕ0 𝐵 − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
127 3 77 mulcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · 𝐴 ) )
128 1 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · 𝐴 ) )
129 127 128 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) )
130 73 75 129 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) )
131 81 91 87 fsummulc2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) )
132 130 131 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) − ( 𝐴 · Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) ) = ( ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) )
133 94 126 132 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
134 133 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
135 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
136 135 oveq2d ⊢ ( 𝑛 = 𝑗 → ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) )
137 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) )
138 ovex ⊢ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) ∈ V
139 136 137 138 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) )
140 75 139 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) )
141 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
142 141 9 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
143 140 142 80 fsumser ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) )
144 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
145 144 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 𝐴 · ( 𝐺 ‘ 𝑛 ) ) = ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) )
146 fveq2 ⊢ ( 𝑛 = ( 𝑘 − 𝑗 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) )
147 146 oveq2d ⊢ ( 𝑛 = ( 𝑘 − 𝑗 ) → ( 𝐴 · ( 𝐺 ‘ 𝑛 ) ) = ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
148 88 anasss ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑚 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ) ) → ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
149 145 147 148 fsum0diag2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑚 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
150 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → 𝜑 )
151 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑚 ) → 𝑘 ∈ ℕ0 )
152 151 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → 𝑘 ∈ ℕ0 )
153 150 152 6 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
154 150 152 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑚 ) ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) ∈ ℂ )
155 153 142 154 fsumser ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑚 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( 𝐴 · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) = ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) )
156 149 155 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑚 ) Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) = ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) )
157 143 156 oveq12d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑗 ) ) − Σ 𝑗 ∈ ( 0 ... 𝑚 ) Σ 𝑘 ∈ ( 0 ... ( 𝑚 − 𝑗 ) ) ( 𝐴 · ( 𝐺 ‘ 𝑘 ) ) ) = ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) )
158 90 134 157 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) )
159 158 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) = ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) )
160 159 breq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
161 71 160 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ) ) → ( ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
162 161 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ) → ( ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
163 162 ralbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
164 163 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
165 164 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ Σ 𝑗 ∈ ( 0 ... 𝑚 ) ( 𝐴 · Σ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑚 − 𝑗 ) + 1 ) ) 𝐵 ) ) < 𝑥 ) )
166 70 165 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 )
167 166 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ0 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑦 ) ( abs ‘ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ‘ 𝑚 ) − ( seq 0 ( + , 𝐻 ) ‘ 𝑚 ) ) ) < 𝑥 )
168 1 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) = ( abs ‘ 𝐴 ) )
169 2 168 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐾 ‘ 𝑗 ) = ( abs ‘ ( 𝐹 ‘ 𝑗 ) ) )
170 9 10 169 78 7 abscvgcvg ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
171 9 10 1 3 170 isumclim2 ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ Σ 𝑗 ∈ ℕ0 𝐴 )
172 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
173 fveq2 ⊢ ( 𝑗 = 𝑚 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑚 ) )
174 173 eleq1d ⊢ ( 𝑗 = 𝑚 → ( ( 𝐹 ‘ 𝑗 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) )
175 174 rspccva ⊢ ( ( ∀ 𝑗 ∈ ℕ0 ( 𝐹 ‘ 𝑗 ) ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
176 172 175 sylan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
177 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑚 ) )
178 177 oveq2d ⊢ ( 𝑛 = 𝑚 → ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
179 ovex ⊢ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑚 ) ) ∈ V
180 178 137 179 fvmpt ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
181 180 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑚 ) ) )
182 9 10 76 171 176 181 isermulc2 ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ⇝ ( Σ 𝑘 ∈ ℕ0 𝐵 · Σ 𝑗 ∈ ℕ0 𝐴 ) )
183 9 10 1 3 170 isumcl ⊢ ( 𝜑 → Σ 𝑗 ∈ ℕ0 𝐴 ∈ ℂ )
184 76 183 mulcomd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ℕ0 𝐵 · Σ 𝑗 ∈ ℕ0 𝐴 ) = ( Σ 𝑗 ∈ ℕ0 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) )
185 182 184 breqtrd ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑘 ∈ ℕ0 𝐵 · ( 𝐹 ‘ 𝑛 ) ) ) ) ⇝ ( Σ 𝑗 ∈ ℕ0 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) )
186 9 10 12 33 167 185 2clim ⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( Σ 𝑗 ∈ ℕ0 𝐴 · Σ 𝑘 ∈ ℕ0 𝐵 ) )