Theorem mertens 15922

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 12920	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		0zd 12625	. 2 ⊢ (𝜑 → 0 ∈ ℤ)
3		seqex 14044	. . 3 ⊢ seq0( + , 𝐻) ∈ V
4	3	a1i 11	. 2 ⊢ (𝜑 → seq0( + , 𝐻) ∈ V)
5		mertens.6	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
6		fzfid 14014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
7		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝜑)
8		elfznn0 13660	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
9		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
10	7, 8, 9	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
11		fveq2 6906	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 − 𝑗) → (𝐺‘𝑖) = (𝐺‘(𝑘 − 𝑗)))
12	11	eleq1d 2826	. . . . . . . 8 ⊢ (𝑖 = (𝑘 − 𝑗) → ((𝐺‘𝑖) ∈ ℂ ↔ (𝐺‘(𝑘 − 𝑗)) ∈ ℂ))
13		mertens.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
14		mertens.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
15	13, 14	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
16	15	ralrimiva 3146	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ)
17		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐺‘𝑘) = (𝐺‘𝑖))
18	17	eleq1d 2826	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑖) ∈ ℂ))
19	18	cbvralvw 3237	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ ↔ ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
20	16, 19	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
21	20	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
22		fznn0sub 13596	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑘) → (𝑘 − 𝑗) ∈ ℕ0)
23	22	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − 𝑗) ∈ ℕ0)
24	12, 21, 23	rspcdva 3623	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − 𝑗)) ∈ ℂ)
25	10, 24	mulcld 11281	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
26	6, 25	fsumcl 15769	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
27	5, 26	eqeltrd 2841	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ)
28	1, 2, 27	serf 14071	. . 3 ⊢ (𝜑 → seq0( + , 𝐻):ℕ0⟶ℂ)
29	28	ffvelcdmda 7104	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐻)‘𝑚) ∈ ℂ)
30		mertens.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
31	30	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
32		mertens.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
33	32	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
34	9	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
35	13	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
36	14	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
37	5	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
38		mertens.7	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
39	38	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐾) ∈ dom ⇝ )
40		mertens.8	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
41	40	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐺) ∈ dom ⇝ )
42		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
43		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑘 → (𝐺‘𝑙) = (𝐺‘𝑘))
44	43	cbvsumv 15732	. . . . . . . . . . 11 ⊢ Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘)
45		fvoveq1 7454	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → (ℤ≥‘(𝑖 + 1)) = (ℤ≥‘(𝑛 + 1)))
46	45	sumeq1d 15736	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
47	44, 46	eqtrid 2789	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
48	47	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
49	48	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → (𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ 𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
50	49	cbvrexvw 3238	. . . . . . 7 ⊢ (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
51		eqeq1 2741	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ 𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
52	51	rexbidv 3179	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
53	50, 52	bitrid 283	. . . . . 6 ⊢ (𝑢 = 𝑧 → (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
54	53	cbvabv 2812	. . . . 5 ⊢ {𝑢 ∣ ∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}
55		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐾‘𝑖) = (𝐾‘𝑗))
56	55	cbvsumv 15732	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)
57	56	oveq1i 7441	. . . . . . . . . 10 ⊢ (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)
58	57	oveq2i 7442	. . . . . . . . 9 ⊢ ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) = ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))
59	58	breq2i 5151	. . . . . . . 8 ⊢ ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
60		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
61	60	cbvsumv 15732	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘)
62		fvoveq1 7454	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑛 → (ℤ≥‘(𝑢 + 1)) = (ℤ≥‘(𝑛 + 1)))
63	62	sumeq1d 15736	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
64	61, 63	eqtrid 2789	. . . . . . . . . 10 ⊢ (𝑢 = 𝑛 → Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
65	64	fveq2d 6910	. . . . . . . . 9 ⊢ (𝑢 = 𝑛 → (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
66	65	breq1d 5153	. . . . . . . 8 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
67	59, 66	bitrid 283	. . . . . . 7 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
68	67	cbvralvw 3237	. . . . . 6 ⊢ (∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
69	68	anbi2i 623	. . . . 5 ⊢ ((𝑠 ∈ ℕ ∧ ∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1))) ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
70	31, 33, 34, 35, 36, 37, 39, 41, 42, 54, 69	mertenslem2 15921	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥)
71		eluznn0 12959	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → 𝑚 ∈ ℕ0)
72		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
73		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
74		elfznn0 13660	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
75	74	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑗 ∈ ℕ0)
76	1, 2, 13, 14, 40	isumcl 15797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
77	76	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
78	30, 9	eqeltrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) ∈ ℂ)
79	77, 78	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
80	73, 75, 79	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
81		fzfid 14014	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(𝑚 − 𝑗)) ∈ Fin)
82		simplll 775	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝜑)
83	74	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑗 ∈ ℕ0)
84	82, 83, 9	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝐴 ∈ ℂ)
85		elfznn0 13660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑚 − 𝑗)) → 𝑘 ∈ ℕ0)
86	85	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑘 ∈ ℕ0)
87	82, 86, 15	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) ∈ ℂ)
88	84, 87	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
89	81, 88	fsumcl 15769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) ∈ ℂ)
90	72, 80, 89	fsumsub 15824	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
91	73, 75, 9	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
92	76	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
93	81, 87	fsumcl 15769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) ∈ ℂ)
94	91, 92, 93	subdid 11719	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))))
95		eqid 2737	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ≥‘((𝑚 − 𝑗) + 1)) = (ℤ≥‘((𝑚 − 𝑗) + 1))
96		fznn0sub 13596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ0)
97	96	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ0)
98		peano2nn0 12566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
100	99	nn0zd 12639	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
101		simplll 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
102		eluznn0 12959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
103	99, 102	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
104	101, 103, 13	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
105	101, 103, 14	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
106	40	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
107	73, 13	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
108	73, 14	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
109	107, 108	eqeltrd 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
110	1, 99, 109	iserex 15693	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
111	106, 110	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
112	95, 100, 104, 105, 111	isumcl 15797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
113	1, 95, 99, 107, 108, 106	isumsplit 15876	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
114	97	nn0cnd 12589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℂ)
115		ax-1cn 11213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
116		pncan 11514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 − 𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
117	114, 115, 116	sylancl 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
118	117	oveq2d 7447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(((𝑚 − 𝑗) + 1) − 1)) = (0...(𝑚 − 𝑗)))
119	118	sumeq1d 15736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
120	82, 86, 13	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) = 𝐵)
121	120	sumeq2dv 15738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
122	119, 121	eqtr4d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))
123	122	oveq1d 7446	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
124	113, 123	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
125	93, 112, 124	mvrladdd 11676	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)
126	125	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
127	9, 77	mulcomd 11282	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
128	30	oveq2d 7447	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
129	127, 128	eqtr4d 2780	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
130	73, 75, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
131	81, 91, 87	fsummulc2 15820	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)))
132	130, 131	oveq12d 7449	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
133	94, 126, 132	3eqtr3rd 2786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
134	133	sumeq2dv 15738	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
135		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
136	135	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
137		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))
138		ovex 7464	. . . . . . . . . . . . . . . 16 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ V
139	136, 137, 138	fvmpt 7016	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
140	75, 139	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
141		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
142	141, 1	eleqtrdi 2851	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ≥‘0))
143	140, 142, 80	fsumser 15766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚))
144		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
145	144	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘𝑘)))
146		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐺‘𝑛) = (𝐺‘(𝑘 − 𝑗)))
147	146	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘(𝑘 − 𝑗))))
148	88	anasss 466	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ (𝑗 ∈ (0...𝑚) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗)))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
149	145, 147, 148	fsum0diag2 15819	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
150		simpll 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝜑)
151		elfznn0 13660	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0)
152	151	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ0)
153	150, 152, 5	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
154	150, 152, 26	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
155	153, 142, 154	fsumser 15766	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) = (seq0( + , 𝐻)‘𝑚))
156	149, 155	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = (seq0( + , 𝐻)‘𝑚))
157	143, 156	oveq12d 7449	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)))
158	90, 134, 157	3eqtr3rd 2786	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
159	158	fveq2d 6910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) = (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))
160	159	breq1d 5153	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
161	71, 160	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦))) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
162	161	anassrs 467	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
163	162	ralbidva 3176	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
164	163	rexbidva 3177	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
165	164	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
166	70, 165	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
167	166	ralrimiva 3146	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
168	30	fveq2d 6910	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐹‘𝑗)) = (abs‘𝐴))
169	32, 168	eqtr4d 2780	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘(𝐹‘𝑗)))
170	1, 2, 169, 78, 38	abscvgcvg 15855	. . . . 5 ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
171	1, 2, 30, 9, 170	isumclim2 15794	. . . 4 ⊢ (𝜑 → seq0( + , 𝐹) ⇝ Σ𝑗 ∈ ℕ0 𝐴)
172	78	ralrimiva 3146	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ)
173		fveq2 6906	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝐹‘𝑗) = (𝐹‘𝑚))
174	173	eleq1d 2826	. . . . . 6 ⊢ (𝑗 = 𝑚 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ))
175	174	rspccva 3621	. . . . 5 ⊢ ((∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
176	172, 175	sylan 580	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
177		fveq2 6906	. . . . . . 7 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
178	177	oveq2d 7447	. . . . . 6 ⊢ (𝑛 = 𝑚 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
179		ovex 7464	. . . . . 6 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)) ∈ V
180	178, 137, 179	fvmpt 7016	. . . . 5 ⊢ (𝑚 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
181	180	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
182	1, 2, 76, 171, 176, 181	isermulc2 15694	. . 3 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴))
183	1, 2, 30, 9, 170	isumcl 15797	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ ℕ0 𝐴 ∈ ℂ)
184	76, 183	mulcomd 11282	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴) = (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
185	182, 184	breqtrd 5169	. 2 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
186	1, 2, 4, 29, 167, 185	2clim 15608	1 ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070  Vcvv 3480   class class class wbr 5143   ↦ cmpt 5225  dom cdm 5685  ‘cfv 6561  (class class class)co 7431  ℂcc 11153  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295   − cmin 11492   / cdiv 11920  ℕcn 12266  2c2 12321  ℕ₀cn0 12526  ℤ_≥cuz 12878  ℝ⁺crp 13034  ...cfz 13547  seqcseq 14042  abscabs 15273   ⇝ cli 15520  Σcsu 15722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-ico 13393  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723

This theorem is referenced by:  efaddlem  16129