Theorem mertens 15930

Description: Mertens' theorem. If 𝐴(𝑗) is an absolutely convergent series and 𝐵(𝑘) is convergent, then (Σ𝑗 ∈ ℕ₀𝐴(𝑗) · Σ𝑘 ∈ ℕ₀𝐵(𝑘)) = Σ𝑘 ∈ ℕ₀Σ𝑗 ∈ (0...𝑘)(𝐴(𝑗) · 𝐵(𝑘 − 𝑗)) (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.)

Hypotheses

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

Assertion

Ref	Expression
mertens	⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))

Distinct variable groups:   𝐵,𝑗   𝑗,𝑘,𝐺   𝜑,𝑗,𝑘   𝐴,𝑘   𝑗,𝐾,𝑘   𝑗,𝐹   𝑘,𝐻

Allowed substitution hints:   𝐴(𝑗)   𝐵(𝑘)   𝐹(𝑘)   𝐻(𝑗)

Proof of Theorem mertens

Dummy variables 𝑚 𝑛 𝑠 𝑥 𝑦 𝑧 𝑖 𝑙 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0uz 12891	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		0zd 12594	. 2 ⊢ (𝜑 → 0 ∈ ℤ)
3		seqex 14030	. . 3 ⊢ seq0( + , 𝐻) ∈ V
4	3	a1i 11	. 2 ⊢ (𝜑 → seq0( + , 𝐻) ∈ V)
5		mertens.6	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
6		fzfid 14000	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
7		simpl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝜑)
8		elfznn0 13639	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
9		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
10	7, 8, 9	syl2an 607	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
11		fveq2 6871	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 − 𝑗) → (𝐺‘𝑖) = (𝐺‘(𝑘 − 𝑗)))
12	11	eleq1d 2850	. . . . . . . 8 ⊢ (𝑖 = (𝑘 − 𝑗) → ((𝐺‘𝑖) ∈ ℂ ↔ (𝐺‘(𝑘 − 𝑗)) ∈ ℂ))
13		mertens.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
14		mertens.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
15	13, 14	eqeltrd 2865	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
16	15	ralrimiva 3157	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ)
17		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐺‘𝑘) = (𝐺‘𝑖))
18	17	eleq1d 2850	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑖) ∈ ℂ))
19	18	cbvralvw 3243	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ ↔ ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
20	16, 19	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
21	20	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
22		fznn0sub 13575	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑘) → (𝑘 − 𝑗) ∈ ℕ0)
23	22	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − 𝑗) ∈ ℕ0)
24	12, 21, 23	rspcdva 3585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − 𝑗)) ∈ ℂ)
25	10, 24	mulcld 11217	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
26	6, 25	fsumcl 15774	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
27	5, 26	eqeltrd 2865	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ)
28	1, 2, 27	serf 14057	. . 3 ⊢ (𝜑 → seq0( + , 𝐻):ℕ0⟶ℂ)
29	28	ffvelcdmda 7069	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐻)‘𝑚) ∈ ℂ)
30		mertens.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
31	30	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
32		mertens.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
33	32	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
34	9	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
35	13	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
36	14	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
37	5	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
38		mertens.7	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
39	38	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐾) ∈ dom ⇝ )
40		mertens.8	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
41	40	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐺) ∈ dom ⇝ )
42		simpr 489	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
43		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑘 → (𝐺‘𝑙) = (𝐺‘𝑘))
44	43	cbvsumv 15737	. . . . . . . . . . 11 ⊢ Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘)
45		fvoveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → (ℤ≥‘(𝑖 + 1)) = (ℤ≥‘(𝑛 + 1)))
46	45	sumeq1d 15741	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
47	44, 46	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
48	47	fveq2d 6875	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
49	48	eqeq2d 2776	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → (𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ 𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
50	49	cbvrexvw 3244	. . . . . . 7 ⊢ (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
51		eqeq1 2769	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ 𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
52	51	rexbidv 3189	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
53	50, 52	bitrid 286	. . . . . 6 ⊢ (𝑢 = 𝑧 → (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
54	53	cbvabv 2835	. . . . 5 ⊢ {𝑢 ∣ ∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}
55		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐾‘𝑖) = (𝐾‘𝑗))
56	55	cbvsumv 15737	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)
57	56	oveq1i 7410	. . . . . . . . . 10 ⊢ (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)
58	57	oveq2i 7411	. . . . . . . . 9 ⊢ ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) = ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))
59	58	breq2i 5113	. . . . . . . 8 ⊢ ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
60		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
61	60	cbvsumv 15737	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘)
62		fvoveq1 7423	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑛 → (ℤ≥‘(𝑢 + 1)) = (ℤ≥‘(𝑛 + 1)))
63	62	sumeq1d 15741	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
64	61, 63	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝑢 = 𝑛 → Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
65	64	fveq2d 6875	. . . . . . . . 9 ⊢ (𝑢 = 𝑛 → (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
66	65	breq1d 5115	. . . . . . . 8 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
67	59, 66	bitrid 286	. . . . . . 7 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
68	67	cbvralvw 3243	. . . . . 6 ⊢ (∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
69	68	anbi2i 634	. . . . 5 ⊢ ((𝑠 ∈ ℕ ∧ ∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1))) ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
70	31, 33, 34, 35, 36, 37, 39, 41, 42, 54, 69	mertenslem2 15929	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥)
71		eluznn0 12932	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → 𝑚 ∈ ℕ0)
72		fzfid 14000	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
73		simpll 778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
74		elfznn0 13639	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
75	74	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑗 ∈ ℕ0)
76	1, 2, 13, 14, 40	isumcl 15802	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
77	76	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
78	30, 9	eqeltrd 2865	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) ∈ ℂ)
79	77, 78	mulcld 11217	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
80	73, 75, 79	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
81		fzfid 14000	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(𝑚 − 𝑗)) ∈ Fin)
82		simplll 786	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝜑)
83	74	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑗 ∈ ℕ0)
84	82, 83, 9	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝐴 ∈ ℂ)
85		elfznn0 13639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑚 − 𝑗)) → 𝑘 ∈ ℕ0)
86	85	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑘 ∈ ℕ0)
87	82, 86, 15	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) ∈ ℂ)
88	84, 87	mulcld 11217	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
89	81, 88	fsumcl 15774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) ∈ ℂ)
90	72, 80, 89	fsumsub 15829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
91	73, 75, 9	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
92	76	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
93	81, 87	fsumcl 15774	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) ∈ ℂ)
94	91, 92, 93	subdid 11658	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))))
95		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ≥‘((𝑚 − 𝑗) + 1)) = (ℤ≥‘((𝑚 − 𝑗) + 1))
96		fznn0sub 13575	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ0)
97	96	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ0)
98		peano2nn0 12535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
99	97, 98	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
100	99	nn0zd 12607	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
101		simplll 786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
102		eluznn0 12932	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
103	99, 102	sylan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
104	101, 103, 13	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
105	101, 103, 14	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
106	40	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
107	73, 13	sylan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
108	73, 14	sylan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
109	107, 108	eqeltrd 2865	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
110	1, 99, 109	iserex 15698	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
111	106, 110	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
112	95, 100, 104, 105, 111	isumcl 15802	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
113	1, 95, 99, 107, 108, 106	isumsplit 15884	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
114	97	nn0cnd 12558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℂ)
115		ax-1cn 11146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
116		pncan 11451	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 − 𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
117	114, 115, 116	sylancl 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
118	117	oveq2d 7416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(((𝑚 − 𝑗) + 1) − 1)) = (0...(𝑚 − 𝑗)))
119	118	sumeq1d 15741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
120	82, 86, 13	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) = 𝐵)
121	120	sumeq2dv 15743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
122	119, 121	eqtr4d 2803	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))
123	122	oveq1d 7415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
124	113, 123	eqtrd 2800	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
125	93, 112, 124	mvrladdd 11615	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)
126	125	oveq2d 7416	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
127	9, 77	mulcomd 11218	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
128	30	oveq2d 7416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
129	127, 128	eqtr4d 2803	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
130	73, 75, 129	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
131	81, 91, 87	fsummulc2 15825	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)))
132	130, 131	oveq12d 7418	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
133	94, 126, 132	3eqtr3rd 2809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
134	133	sumeq2dv 15743	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
135		fveq2 6871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
136	135	oveq2d 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
137		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))
138		ovex 7433	. . . . . . . . . . . . . . . 16 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ V
139	136, 137, 138	fvmpt 6979	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
140	75, 139	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
141		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
142	141, 1	eleqtrdi 2875	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ≥‘0))
143	140, 142, 80	fsumser 15771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚))
144		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
145	144	oveq2d 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘𝑘)))
146		fveq2 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐺‘𝑛) = (𝐺‘(𝑘 − 𝑗)))
147	146	oveq2d 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘(𝑘 − 𝑗))))
148	88	anasss 471	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ (𝑗 ∈ (0...𝑚) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗)))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
149	145, 147, 148	fsum0diag2 15824	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
150		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝜑)
151		elfznn0 13639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0)
152	151	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ0)
153	150, 152, 5	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
154	150, 152, 26	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
155	153, 142, 154	fsumser 15771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) = (seq0( + , 𝐻)‘𝑚))
156	149, 155	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = (seq0( + , 𝐻)‘𝑚))
157	143, 156	oveq12d 7418	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)))
158	90, 134, 157	3eqtr3rd 2809	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
159	158	fveq2d 6875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) = (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))
160	159	breq1d 5115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
161	71, 160	sylan2 604	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦))) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
162	161	anassrs 472	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
163	162	ralbidva 3186	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
164	163	rexbidva 3187	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
165	164	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
166	70, 165	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
167	166	ralrimiva 3157	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
168	30	fveq2d 6875	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐹‘𝑗)) = (abs‘𝐴))
169	32, 168	eqtr4d 2803	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘(𝐹‘𝑗)))
170	1, 2, 169, 78, 38	abscvgcvg 15861	. . . . 5 ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
171	1, 2, 30, 9, 170	isumclim2 15799	. . . 4 ⊢ (𝜑 → seq0( + , 𝐹) ⇝ Σ𝑗 ∈ ℕ0 𝐴)
172	78	ralrimiva 3157	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ)
173		fveq2 6871	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝐹‘𝑗) = (𝐹‘𝑚))
174	173	eleq1d 2850	. . . . . 6 ⊢ (𝑗 = 𝑚 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ))
175	174	rspccva 3583	. . . . 5 ⊢ ((∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
176	172, 175	sylan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
177		fveq2 6871	. . . . . . 7 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
178	177	oveq2d 7416	. . . . . 6 ⊢ (𝑛 = 𝑚 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
179		ovex 7433	. . . . . 6 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)) ∈ V
180	178, 137, 179	fvmpt 6979	. . . . 5 ⊢ (𝑚 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
181	180	adantl 486	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
182	1, 2, 76, 171, 176, 181	isermulc2 15699	. . 3 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴))
183	1, 2, 30, 9, 170	isumcl 15802	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ ℕ0 𝐴 ∈ ℂ)
184	76, 183	mulcomd 11218	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴) = (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
185	182, 184	breqtrd 5131	. 2 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
186	1, 2, 4, 29, 167, 185	2clim 15613	1 ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {cab 2743  ∀wral 3079  ∃wrex 3089  Vcvv 3457   class class class wbr 5105   ↦ cmpt 5186  dom cdm 5652  ‘cfv 6525  (class class class)co 7400  ℂcc 11086  0cc0 11088  1c1 11089   + caddc 11091   · cmul 11093   < clt 11231   − cmin 11429   / cdiv 11859  ℕcn 12224  2c2 12286  ℕ₀cn0 12495  ℤ_≥cuz 12853  ℝ⁺crp 13007  ...cfz 13526  seqcseq 14028  abscabs 15275   ⇝ cli 15525  Σcsu 15727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-inf2 9598  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-se 5606  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-er 8682  df-pm 8815  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-sup 9390  df-inf 9391  df-oi 9460  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12225  df-2 12294  df-3 12295  df-n0 12496  df-z 12583  df-uz 12854  df-rp 13008  df-ico 13369  df-fz 13527  df-fzo 13674  df-fl 13816  df-seq 14029  df-exp 14089  df-hash 14358  df-cj 15140  df-re 15141  df-im 15142  df-sqrt 15276  df-abs 15277  df-limsup 15512  df-clim 15529  df-rlim 15530  df-sum 15728

This theorem is referenced by:  efaddlem  16137