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 𝐵 ) )