Theorem mertens 15234

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 12268	. 2 ⊢ ℕ0 = (ℤ≥‘0)
2		0zd 11981	. 2 ⊢ (𝜑 → 0 ∈ ℤ)
3		seqex 13366	. . 3 ⊢ seq0( + , 𝐻) ∈ V
4	3	a1i 11	. 2 ⊢ (𝜑 → seq0( + , 𝐻) ∈ V)
5		mertens.6	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
6		fzfid 13336	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
7		simpl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝜑)
8		elfznn0 12995	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
9		mertens.3	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
10	7, 8, 9	syl2an 598	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
11		fveq2 6645	. . . . . . . . 9 ⊢ (𝑖 = (𝑘 − 𝑗) → (𝐺‘𝑖) = (𝐺‘(𝑘 − 𝑗)))
12	11	eleq1d 2874	. . . . . . . 8 ⊢ (𝑖 = (𝑘 − 𝑗) → ((𝐺‘𝑖) ∈ ℂ ↔ (𝐺‘(𝑘 − 𝑗)) ∈ ℂ))
13		mertens.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
14		mertens.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
15	13, 14	eqeltrd 2890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
16	15	ralrimiva 3149	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ)
17		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐺‘𝑘) = (𝐺‘𝑖))
18	17	eleq1d 2874	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝐺‘𝑘) ∈ ℂ ↔ (𝐺‘𝑖) ∈ ℂ))
19	18	cbvralvw 3396	. . . . . . . . . 10 ⊢ (∀𝑘 ∈ ℕ0 (𝐺‘𝑘) ∈ ℂ ↔ ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
20	16, 19	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
21	20	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ∀𝑖 ∈ ℕ0 (𝐺‘𝑖) ∈ ℂ)
22		fznn0sub 12934	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑘) → (𝑘 − 𝑗) ∈ ℕ0)
23	22	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘 − 𝑗) ∈ ℕ0)
24	12, 21, 23	rspcdva 3573	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘 − 𝑗)) ∈ ℂ)
25	10, 24	mulcld 10650	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
26	6, 25	fsumcl 15082	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
27	5, 26	eqeltrd 2890	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ)
28	1, 2, 27	serf 13394	. . 3 ⊢ (𝜑 → seq0( + , 𝐻):ℕ0⟶ℂ)
29	28	ffvelrnda 6828	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (seq0( + , 𝐻)‘𝑚) ∈ ℂ)
30		mertens.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
31	30	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴)
32		mertens.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
33	32	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴))
34	9	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
35	13	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
36	14	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
37	5	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
38		mertens.7	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
39	38	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐾) ∈ dom ⇝ )
40		mertens.8	. . . . . 6 ⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
41	40	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq0( + , 𝐺) ∈ dom ⇝ )
42		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
43		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑘 → (𝐺‘𝑙) = (𝐺‘𝑘))
44	43	cbvsumv 15045	. . . . . . . . . . 11 ⊢ Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘)
45		fvoveq1 7158	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑛 → (ℤ≥‘(𝑖 + 1)) = (ℤ≥‘(𝑛 + 1)))
46	45	sumeq1d 15050	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
47	44, 46	syl5eq 2845	. . . . . . . . . 10 ⊢ (𝑖 = 𝑛 → Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
48	47	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑖 = 𝑛 → (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
49	48	eqeq2d 2809	. . . . . . . 8 ⊢ (𝑖 = 𝑛 → (𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ 𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
50	49	cbvrexvw 3397	. . . . . . 7 ⊢ (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
51		eqeq1 2802	. . . . . . . 8 ⊢ (𝑢 = 𝑧 → (𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ 𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
52	51	rexbidv 3256	. . . . . . 7 ⊢ (𝑢 = 𝑧 → (∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
53	50, 52	syl5bb 286	. . . . . 6 ⊢ (𝑢 = 𝑧 → (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))))
54	53	cbvabv 2866	. . . . 5 ⊢ {𝑢 ∣ ∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ≥‘(𝑖 + 1))(𝐺‘𝑙))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))}
55		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐾‘𝑖) = (𝐾‘𝑗))
56	55	cbvsumv 15045	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)
57	56	oveq1i 7145	. . . . . . . . . 10 ⊢ (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)
58	57	oveq2i 7146	. . . . . . . . 9 ⊢ ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) = ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))
59	58	breq2i 5038	. . . . . . . 8 ⊢ ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
60		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
61	60	cbvsumv 15045	. . . . . . . . . . 11 ⊢ Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘)
62		fvoveq1 7158	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑛 → (ℤ≥‘(𝑢 + 1)) = (ℤ≥‘(𝑛 + 1)))
63	62	sumeq1d 15050	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
64	61, 63	syl5eq 2845	. . . . . . . . . 10 ⊢ (𝑢 = 𝑛 → Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))
65	64	fveq2d 6649	. . . . . . . . 9 ⊢ (𝑢 = 𝑛 → (abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))
66	65	breq1d 5040	. . . . . . . 8 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
67	59, 66	syl5bb 286	. . . . . . 7 ⊢ (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
68	67	cbvralvw 3396	. . . . . 6 ⊢ (∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))
69	68	anbi2i 625	. . . . 5 ⊢ ((𝑠 ∈ ℕ ∧ ∀𝑢 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑖 ∈ (ℤ≥‘(𝑢 + 1))(𝐺‘𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾‘𝑖) + 1))) ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))))
70	31, 33, 34, 35, 36, 37, 39, 41, 42, 54, 69	mertenslem2 15233	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥)
71		eluznn0 12305	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → 𝑚 ∈ ℕ0)
72		fzfid 13336	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
73		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
74		elfznn0 12995	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
75	74	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑗 ∈ ℕ0)
76	1, 2, 13, 14, 40	isumcl 15108	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
77	76	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
78	30, 9	eqeltrd 2890	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) ∈ ℂ)
79	77, 78	mulcld 10650	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
80	73, 75, 79	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ ℂ)
81		fzfid 13336	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(𝑚 − 𝑗)) ∈ Fin)
82		simplll 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝜑)
83	74	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑗 ∈ ℕ0)
84	82, 83, 9	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝐴 ∈ ℂ)
85		elfznn0 12995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...(𝑚 − 𝑗)) → 𝑘 ∈ ℕ0)
86	85	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → 𝑘 ∈ ℕ0)
87	82, 86, 15	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) ∈ ℂ)
88	84, 87	mulcld 10650	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
89	81, 88	fsumcl 15082	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) ∈ ℂ)
90	72, 80, 89	fsumsub 15135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
91	73, 75, 9	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
92	76	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
93	81, 87	fsumcl 15082	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) ∈ ℂ)
94	91, 92, 93	subdid 11085	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))))
95		eqid 2798	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ≥‘((𝑚 − 𝑗) + 1)) = (ℤ≥‘((𝑚 − 𝑗) + 1))
96		fznn0sub 12934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈ ℕ0)
97	96	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℕ0)
98		peano2nn0 11925	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℕ0)
100	99	nn0zd 12073	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ)
101		simplll 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑)
102		eluznn0 12305	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
103	99, 102	sylan 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0)
104	101, 103, 13	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵)
105	101, 103, 14	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ)
106	40	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
107	73, 13	sylan 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵)
108	73, 14	sylan 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
109	107, 108	eqeltrd 2890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ)
110	1, 99, 109	iserex 15005	. . . . . . . . . . . . . . . . . 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 15108	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ)
113	1, 95, 99, 107, 108, 106	isumsplit 15187	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
114	97	nn0cnd 11945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈ ℂ)
115		ax-1cn 10584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
116		pncan 10881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑚 − 𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
117	114, 115, 116	sylancl 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (((𝑚 − 𝑗) + 1) − 1) = (𝑚 − 𝑗))
118	117	oveq2d 7151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(((𝑚 − 𝑗) + 1) − 1)) = (0...(𝑚 − 𝑗)))
119	118	sumeq1d 15050	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
120	82, 86, 13	syl2anc 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗))) → (𝐺‘𝑘) = 𝐵)
121	120	sumeq2dv 15052	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))𝐵)
122	119, 121	eqtr4d 2836	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))
123	122	oveq1d 7150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ (0...(((𝑚 − 𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
124	113, 123	eqtrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘) + Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
125	93, 112, 124	mvrladdd 11042	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)
126	125	oveq2d 7151	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
127	9, 77	mulcomd 10651	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
128	30	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
129	127, 128	eqtr4d 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
130	73, 75, 129	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
131	81, 91, 87	fsummulc2 15131	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘)) = Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)))
132	130, 131	oveq12d 7153	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐺‘𝑘))) = ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))))
133	94, 126, 132	3eqtr3rd 2842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
134	133	sumeq2dv 15052	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
135		fveq2 6645	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗))
136	135	oveq2d 7151	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
137		eqid 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))
138		ovex 7168	. . . . . . . . . . . . . . . 16 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) ∈ V
139	136, 137, 138	fvmpt 6745	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
140	75, 139	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)))
141		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
142	141, 1	eleqtrdi 2900	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ≥‘0))
143	140, 142, 80	fsumser 15079	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚))
144		fveq2 6645	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
145	144	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘𝑘)))
146		fveq2 6645	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐺‘𝑛) = (𝐺‘(𝑘 − 𝑗)))
147	146	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 − 𝑗) → (𝐴 · (𝐺‘𝑛)) = (𝐴 · (𝐺‘(𝑘 − 𝑗))))
148	88	anasss 470	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ (𝑗 ∈ (0...𝑚) ∧ 𝑘 ∈ (0...(𝑚 − 𝑗)))) → (𝐴 · (𝐺‘𝑘)) ∈ ℂ)
149	145, 147, 148	fsum0diag2 15130	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
150		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝜑)
151		elfznn0 12995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0)
152	151	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → 𝑘 ∈ ℕ0)
153	150, 152, 5	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))))
154	150, 152, 26	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑚)) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) ∈ ℂ)
155	153, 142, 154	fsumser 15079	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑚)Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗))) = (seq0( + , 𝐻)‘𝑚))
156	149, 155	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘)) = (seq0( + , 𝐻)‘𝑚))
157	143, 156	oveq12d 7153	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑗)) − Σ𝑗 ∈ (0...𝑚)Σ𝑘 ∈ (0...(𝑚 − 𝑗))(𝐴 · (𝐺‘𝑘))) = ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)))
158	90, 134, 157	3eqtr3rd 2842	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))
159	158	fveq2d 6649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) = (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))
160	159	breq1d 5040	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
161	71, 160	sylan2 595	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ ℕ0 ∧ 𝑚 ∈ (ℤ≥‘𝑦))) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
162	161	anassrs 471	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑦)) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
163	162	ralbidva 3161	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
164	163	rexbidva 3255	. . . . 5 ⊢ (𝜑 → (∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝑥))
165	164	adantr 484	. . . 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 3149	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
168	30	fveq2d 6649	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (abs‘(𝐹‘𝑗)) = (abs‘𝐴))
169	32, 168	eqtr4d 2836	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘(𝐹‘𝑗)))
170	1, 2, 169, 78, 38	abscvgcvg 15166	. . . . 5 ⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
171	1, 2, 30, 9, 170	isumclim2 15105	. . . 4 ⊢ (𝜑 → seq0( + , 𝐹) ⇝ Σ𝑗 ∈ ℕ0 𝐴)
172	78	ralrimiva 3149	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ)
173		fveq2 6645	. . . . . . 7 ⊢ (𝑗 = 𝑚 → (𝐹‘𝑗) = (𝐹‘𝑚))
174	173	eleq1d 2874	. . . . . 6 ⊢ (𝑗 = 𝑚 → ((𝐹‘𝑗) ∈ ℂ ↔ (𝐹‘𝑚) ∈ ℂ))
175	174	rspccva 3570	. . . . 5 ⊢ ((∀𝑗 ∈ ℕ0 (𝐹‘𝑗) ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
176	172, 175	sylan 583	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ)
177		fveq2 6645	. . . . . . 7 ⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚))
178	177	oveq2d 7151	. . . . . 6 ⊢ (𝑛 = 𝑚 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
179		ovex 7168	. . . . . 6 ⊢ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)) ∈ V
180	178, 137, 179	fvmpt 6745	. . . . 5 ⊢ (𝑚 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
181	180	adantl 485	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑚)))
182	1, 2, 76, 171, 176, 181	isermulc2 15006	. . 3 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴))
183	1, 2, 30, 9, 170	isumcl 15108	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ ℕ0 𝐴 ∈ ℂ)
184	76, 183	mulcomd 10651	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴) = (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
185	182, 184	breqtrd 5056	. 2 ⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹‘𝑛)))) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
186	1, 2, 4, 29, 167, 185	2clim 14921	1 ⊢ (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  Vcvv 3441   class class class wbr 5030   ↦ cmpt 5110  dom cdm 5519  ‘cfv 6324  (class class class)co 7135  ℂcc 10524  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664   − cmin 10859   / cdiv 11286  ℕcn 11625  2c2 11680  ℕ₀cn0 11885  ℤ_≥cuz 12231  ℝ⁺crp 12377  ...cfz 12885  seqcseq 13364  abscabs 14585   ⇝ cli 14833  Σcsu 15034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-inf 8891  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-ico 12732  df-fz 12886  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035

This theorem is referenced by:  efaddlem  15438