ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mertensabs GIF version

Theorem mertensabs 11529
Description: Mertens' theorem. If 𝐴(𝑗) is an absolutely convergent series and 𝐵(𝑘) is convergent, then 𝑗 ∈ ℕ0𝐴(𝑗) · Σ𝑘 ∈ ℕ0𝐵(𝑘)) = Σ𝑘 ∈ ℕ0Σ𝑗 ∈ (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.) (Revised by Jim Kingdon, 8-Dec-2022.)
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 ⇝ )
mertens.f (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
Assertion
Ref Expression
mertensabs (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
Distinct variable groups:   𝐵,𝑗   𝑗,𝑘,𝐺   𝜑,𝑗,𝑘   𝐴,𝑘   𝑗,𝐾,𝑘   𝑗,𝐹   𝑘,𝐻
Allowed substitution hints:   𝐴(𝑗)   𝐵(𝑘)   𝐹(𝑘)   𝐻(𝑗)

Proof of Theorem mertensabs
Dummy variables 𝑚 𝑛 𝑠 𝑥 𝑦 𝑧 𝑖 𝑙 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 9551 . 2 0 = (ℤ‘0)
2 0zd 9254 . 2 (𝜑 → 0 ∈ ℤ)
3 seqex 10433 . . 3 seq0( + , 𝐻) ∈ V
43a1i 9 . 2 (𝜑 → seq0( + , 𝐻) ∈ V)
5 mertens.6 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
6 0zd 9254 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 0 ∈ ℤ)
7 nn0z 9262 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
87adantl 277 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
96, 8fzfigd 10417 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (0...𝑘) ∈ Fin)
10 simpl 109 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝜑)
11 elfznn0 10100 . . . . . . . 8 (𝑗 ∈ (0...𝑘) → 𝑗 ∈ ℕ0)
12 mertens.3 . . . . . . . 8 ((𝜑𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
1310, 11, 12syl2an 289 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → 𝐴 ∈ ℂ)
14 fveq2 5511 . . . . . . . . 9 (𝑖 = (𝑘𝑗) → (𝐺𝑖) = (𝐺‘(𝑘𝑗)))
1514eleq1d 2246 . . . . . . . 8 (𝑖 = (𝑘𝑗) → ((𝐺𝑖) ∈ ℂ ↔ (𝐺‘(𝑘𝑗)) ∈ ℂ))
16 mertens.4 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
17 mertens.5 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
1816, 17eqeltrd 2254 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
1918ralrimiva 2550 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ℕ0 (𝐺𝑘) ∈ ℂ)
20 fveq2 5511 . . . . . . . . . . . 12 (𝑘 = 𝑖 → (𝐺𝑘) = (𝐺𝑖))
2120eleq1d 2246 . . . . . . . . . . 11 (𝑘 = 𝑖 → ((𝐺𝑘) ∈ ℂ ↔ (𝐺𝑖) ∈ ℂ))
2221cbvralv 2703 . . . . . . . . . 10 (∀𝑘 ∈ ℕ0 (𝐺𝑘) ∈ ℂ ↔ ∀𝑖 ∈ ℕ0 (𝐺𝑖) ∈ ℂ)
2319, 22sylib 122 . . . . . . . . 9 (𝜑 → ∀𝑖 ∈ ℕ0 (𝐺𝑖) ∈ ℂ)
2423ad2antrr 488 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → ∀𝑖 ∈ ℕ0 (𝐺𝑖) ∈ ℂ)
25 fznn0sub 10043 . . . . . . . . 9 (𝑗 ∈ (0...𝑘) → (𝑘𝑗) ∈ ℕ0)
2625adantl 277 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝑘𝑗) ∈ ℕ0)
2715, 24, 26rspcdva 2846 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐺‘(𝑘𝑗)) ∈ ℂ)
2813, 27mulcld 7968 . . . . . 6 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑘)) → (𝐴 · (𝐺‘(𝑘𝑗))) ∈ ℂ)
299, 28fsumcl 11392 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))) ∈ ℂ)
305, 29eqeltrd 2254 . . . 4 ((𝜑𝑘 ∈ ℕ0) → (𝐻𝑘) ∈ ℂ)
311, 2, 30serf 10460 . . 3 (𝜑 → seq0( + , 𝐻):ℕ0⟶ℂ)
3231ffvelcdmda 5647 . 2 ((𝜑𝑚 ∈ ℕ0) → (seq0( + , 𝐻)‘𝑚) ∈ ℂ)
33 mertens.1 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
3433adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐹𝑗) = 𝐴)
35 mertens.2 . . . . . 6 ((𝜑𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
3635adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → (𝐾𝑗) = (abs‘𝐴))
3712adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈ ℂ)
3816adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
3917adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
405adantlr 477 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
41 mertens.7 . . . . . 6 (𝜑 → seq0( + , 𝐾) ∈ dom ⇝ )
4241adantr 276 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → seq0( + , 𝐾) ∈ dom ⇝ )
43 mertens.8 . . . . . 6 (𝜑 → seq0( + , 𝐺) ∈ dom ⇝ )
4443adantr 276 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → seq0( + , 𝐺) ∈ dom ⇝ )
45 simpr 110 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
46 fveq2 5511 . . . . . . . . . . . 12 (𝑙 = 𝑘 → (𝐺𝑙) = (𝐺𝑘))
4746cbvsumv 11353 . . . . . . . . . . 11 Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙) = Σ𝑘 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑘)
48 fvoveq1 5892 . . . . . . . . . . . 12 (𝑖 = 𝑛 → (ℤ‘(𝑖 + 1)) = (ℤ‘(𝑛 + 1)))
4948sumeq1d 11358 . . . . . . . . . . 11 (𝑖 = 𝑛 → Σ𝑘 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
5047, 49eqtrid 2222 . . . . . . . . . 10 (𝑖 = 𝑛 → Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
5150fveq2d 5515 . . . . . . . . 9 (𝑖 = 𝑛 → (abs‘Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
5251eqeq2d 2189 . . . . . . . 8 (𝑖 = 𝑛 → (𝑢 = (abs‘Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙)) ↔ 𝑢 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
5352cbvrexv 2704 . . . . . . 7 (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
54 eqeq1 2184 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ 𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
5554rexbidv 2478 . . . . . . 7 (𝑢 = 𝑧 → (∃𝑛 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
5653, 55bitrid 192 . . . . . 6 (𝑢 = 𝑧 → (∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))))
5756cbvabv 2302 . . . . 5 {𝑢 ∣ ∃𝑖 ∈ (0...(𝑠 − 1))𝑢 = (abs‘Σ𝑙 ∈ (ℤ‘(𝑖 + 1))(𝐺𝑙))} = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))}
58 fveq2 5511 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (𝐾𝑖) = (𝐾𝑗))
5958cbvsumv 11353 . . . . . . . . . . 11 Σ𝑖 ∈ ℕ0 (𝐾𝑖) = Σ𝑗 ∈ ℕ0 (𝐾𝑗)
6059oveq1i 5879 . . . . . . . . . 10 𝑖 ∈ ℕ0 (𝐾𝑖) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)
6160oveq2i 5880 . . . . . . . . 9 ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾𝑖) + 1)) = ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))
6261breq2i 4008 . . . . . . . 8 ((abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾𝑖) + 1)) ↔ (abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
63 fveq2 5511 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (𝐺𝑖) = (𝐺𝑘))
6463cbvsumv 11353 . . . . . . . . . . 11 Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖) = Σ𝑘 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑘)
65 fvoveq1 5892 . . . . . . . . . . . 12 (𝑢 = 𝑛 → (ℤ‘(𝑢 + 1)) = (ℤ‘(𝑛 + 1)))
6665sumeq1d 11358 . . . . . . . . . . 11 (𝑢 = 𝑛 → Σ𝑘 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑘) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
6764, 66eqtrid 2222 . . . . . . . . . 10 (𝑢 = 𝑛 → Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖) = Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘))
6867fveq2d 5515 . . . . . . . . 9 (𝑢 = 𝑛 → (abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) = (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)))
6968breq1d 4010 . . . . . . . 8 (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7062, 69bitrid 192 . . . . . . 7 (𝑢 = 𝑛 → ((abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾𝑖) + 1)) ↔ (abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7170cbvralv 2703 . . . . . 6 (∀𝑢 ∈ (ℤ𝑠)(abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾𝑖) + 1)) ↔ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1)))
7271anbi2i 457 . . . . 5 ((𝑠 ∈ ℕ ∧ ∀𝑢 ∈ (ℤ𝑠)(abs‘Σ𝑖 ∈ (ℤ‘(𝑢 + 1))(𝐺𝑖)) < ((𝑥 / 2) / (Σ𝑖 ∈ ℕ0 (𝐾𝑖) + 1))) ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈ (ℤ𝑠)(abs‘Σ𝑘 ∈ (ℤ‘(𝑛 + 1))(𝐺𝑘)) < ((𝑥 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾𝑗) + 1))))
7334, 36, 37, 38, 39, 40, 42, 44, 45, 57, 72mertenslem2 11528 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥)
74 eluznn0 9588 . . . . . . . . 9 ((𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)) → 𝑚 ∈ ℕ0)
75 0zd 9254 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → 0 ∈ ℤ)
76 nn0z 9262 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℕ0𝑚 ∈ ℤ)
7776adantl 277 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → 𝑚 ∈ ℤ)
7875, 77fzfigd 10417 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ0) → (0...𝑚) ∈ Fin)
79 simpll 527 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑)
80 elfznn0 10100 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0)
8180adantl 277 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑗 ∈ ℕ0)
821, 2, 16, 17, 43isumcl 11417 . . . . . . . . . . . . . . . 16 (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
8382adantr 276 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
8433, 12eqeltrd 2254 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ ℕ0) → (𝐹𝑗) ∈ ℂ)
8583, 84mulcld 7968 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) ∈ ℂ)
8679, 81, 85syl2anc 411 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) ∈ ℂ)
87 0zd 9254 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 0 ∈ ℤ)
8877adantr 276 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑚 ∈ ℤ)
8981nn0zd 9362 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝑗 ∈ ℤ)
9088, 89zsubcld 9369 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℤ)
9187, 90fzfigd 10417 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(𝑚𝑗)) ∈ Fin)
92 simplll 533 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → 𝜑)
9380ad2antlr 489 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → 𝑗 ∈ ℕ0)
9492, 93, 12syl2anc 411 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → 𝐴 ∈ ℂ)
95 elfznn0 10100 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑚𝑗)) → 𝑘 ∈ ℕ0)
9695adantl 277 . . . . . . . . . . . . . . . 16 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → 𝑘 ∈ ℕ0)
9792, 96, 18syl2anc 411 . . . . . . . . . . . . . . 15 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → (𝐺𝑘) ∈ ℂ)
9894, 97mulcld 7968 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → (𝐴 · (𝐺𝑘)) ∈ ℂ)
9991, 98fsumcl 11392 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘)) ∈ ℂ)
10078, 86, 99fsumsub 11444 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))) = (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑗 ∈ (0...𝑚𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))))
10179, 81, 12syl2anc 411 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ)
10282ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
10391, 97fsumcl 11392 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) ∈ ℂ)
104101, 102, 103subdid 8361 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘))) = ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘))))
105 eqid 2177 . . . . . . . . . . . . . . . . . . 19 (ℤ‘((𝑚𝑗) + 1)) = (ℤ‘((𝑚𝑗) + 1))
106 fznn0sub 10043 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (0...𝑚) → (𝑚𝑗) ∈ ℕ0)
107106adantl 277 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℕ0)
108 peano2nn0 9205 . . . . . . . . . . . . . . . . . . . 20 ((𝑚𝑗) ∈ ℕ0 → ((𝑚𝑗) + 1) ∈ ℕ0)
109107, 108syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℕ0)
11079, 16sylan 283 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = 𝐵)
11179, 17sylan 283 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
11243ad2antrr 488 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ )
1131, 105, 109, 110, 111, 112isumsplit 11483 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(((𝑚𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
114107nn0cnd 9220 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚𝑗) ∈ ℂ)
115 ax-1cn 7895 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
116 pncan 8153 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚𝑗) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑚𝑗) + 1) − 1) = (𝑚𝑗))
117114, 115, 116sylancl 413 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (((𝑚𝑗) + 1) − 1) = (𝑚𝑗))
118117oveq2d 5885 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (0...(((𝑚𝑗) + 1) − 1)) = (0...(𝑚𝑗)))
119118sumeq1d 11358 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚𝑗))𝐵)
12092, 96, 16syl2anc 411 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (0...(𝑚𝑗))) → (𝐺𝑘) = 𝐵)
121120sumeq2dv 11360 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) = Σ𝑘 ∈ (0...(𝑚𝑗))𝐵)
122119, 121eqtr4d 2213 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (0...(((𝑚𝑗) + 1) − 1))𝐵 = Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘))
123122oveq1d 5884 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ (0...(((𝑚𝑗) + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) = (Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
124113, 123eqtrd 2210 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ ℕ0 𝐵 = (Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
125124oveq1d 5884 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘)) = ((Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘)))
126109nn0zd 9362 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚𝑗) + 1) ∈ ℤ)
127 simplll 533 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝜑)
128 eluznn0 9588 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚𝑗) + 1) ∈ ℕ0𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
129109, 128sylan 283 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝑘 ∈ ℕ0)
130127, 129, 16syl2anc 411 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → (𝐺𝑘) = 𝐵)
131127, 129, 17syl2anc 411 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))) → 𝐵 ∈ ℂ)
132110, 111eqeltrd 2254 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
1331, 109, 132iserex 11331 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ))
134112, 133mpbid 147 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )
135105, 126, 130, 131, 134isumcl 11417 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵 ∈ ℂ)
136103, 135pncan2d 8260 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘) + Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘)) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
137125, 136eqtrd 2210 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘)) = Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)
138137oveq2d 5885 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · (Σ𝑘 ∈ ℕ0 𝐵 − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
13912, 83mulcomd 7969 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
14033oveq2d 5885 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) = (Σ𝑘 ∈ ℕ0 𝐵 · 𝐴))
141139, 140eqtr4d 2213 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ ℕ0) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)))
14279, 81, 141syl2anc 411 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ ℕ0 𝐵) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)))
14391, 101, 97fsummulc2 11440 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘)) = Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘)))
144142, 143oveq12d 5887 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((𝐴 · Σ𝑘 ∈ ℕ0 𝐵) − (𝐴 · Σ𝑘 ∈ (0...(𝑚𝑗))(𝐺𝑘))) = ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))))
145104, 138, 1443eqtr3rd 2219 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑚)) → ((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))) = (𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
146145sumeq2dv 11360 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)((Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
147 elnn0uz 9554 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ0𝑗 ∈ (ℤ‘0))
148147biimpri 133 . . . . . . . . . . . . . . 15 (𝑗 ∈ (ℤ‘0) → 𝑗 ∈ ℕ0)
14982ad2antrr 488 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (ℤ‘0)) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
150148, 84sylan2 286 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (ℤ‘0)) → (𝐹𝑗) ∈ ℂ)
151150adantlr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (ℤ‘0)) → (𝐹𝑗) ∈ ℂ)
152149, 151mulcld 7968 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (ℤ‘0)) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) ∈ ℂ)
153 fveq2 5511 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
154153oveq2d 5885 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)))
155 eqid 2177 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))) = (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))
156154, 155fvmptg 5588 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℕ0 ∧ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)))
157148, 152, 156syl2an2 594 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑗 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))‘𝑗) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)))
158 simpr 110 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
159158, 1eleqtrdi 2270 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → 𝑚 ∈ (ℤ‘0))
160157, 159, 152fsum3ser 11389 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚))
161 fveq2 5511 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
162161oveq2d 5885 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝐴 · (𝐺𝑛)) = (𝐴 · (𝐺𝑘)))
163 fveq2 5511 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑘𝑗) → (𝐺𝑛) = (𝐺‘(𝑘𝑗)))
164163oveq2d 5885 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘𝑗) → (𝐴 · (𝐺𝑛)) = (𝐴 · (𝐺‘(𝑘𝑗))))
16598anasss 399 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ (𝑗 ∈ (0...𝑚) ∧ 𝑘 ∈ (0...(𝑚𝑗)))) → (𝐴 · (𝐺𝑘)) ∈ ℂ)
166162, 164, 165, 77fisum0diag2 11439 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘)) = Σ𝑘 ∈ (0...𝑚𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
167 simpll 527 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → 𝜑)
168 elnn0uz 9554 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
169168biimpri 133 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
170169adantl 277 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → 𝑘 ∈ ℕ0)
171167, 170, 5syl2anc 411 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → (𝐻𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))))
172167, 170, 29syl2anc 411 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ0) ∧ 𝑘 ∈ (ℤ‘0)) → Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))) ∈ ℂ)
173171, 159, 172fsum3ser 11389 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑚𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘𝑗))) = (seq0( + , 𝐻)‘𝑚))
174166, 173eqtrd 2210 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ0) → Σ𝑗 ∈ (0...𝑚𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘)) = (seq0( + , 𝐻)‘𝑚))
175160, 174oveq12d 5887 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ0) → (Σ𝑗 ∈ (0...𝑚)(Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑗)) − Σ𝑗 ∈ (0...𝑚𝑘 ∈ (0...(𝑚𝑗))(𝐴 · (𝐺𝑘))) = ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)))
176100, 146, 1753eqtr3rd 2219 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ0) → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚)) = Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵))
177176fveq2d 5515 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ0) → (abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) = (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)))
178177breq1d 4010 . . . . . . . . 9 ((𝜑𝑚 ∈ ℕ0) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
17974, 178sylan2 286 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦))) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
180179anassrs 400 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑚 ∈ (ℤ𝑦)) → ((abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
181180ralbidva 2473 . . . . . 6 ((𝜑𝑦 ∈ ℕ0) → (∀𝑚 ∈ (ℤ𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
182181rexbidva 2474 . . . . 5 (𝜑 → (∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
183182adantr 276 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥 ↔ ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ‘((𝑚𝑗) + 1))𝐵)) < 𝑥))
18473, 183mpbird 167 . . 3 ((𝜑𝑥 ∈ ℝ+) → ∃𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
185184ralrimiva 2550 . 2 (𝜑 → ∀𝑥 ∈ ℝ+𝑦 ∈ ℕ0𝑚 ∈ (ℤ𝑦)(abs‘((seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛))))‘𝑚) − (seq0( + , 𝐻)‘𝑚))) < 𝑥)
186 mertens.f . . . . 5 (𝜑 → seq0( + , 𝐹) ∈ dom ⇝ )
1871, 2, 33, 12, 186isumclim2 11414 . . . 4 (𝜑 → seq0( + , 𝐹) ⇝ Σ𝑗 ∈ ℕ0 𝐴)
18884ralrimiva 2550 . . . . 5 (𝜑 → ∀𝑗 ∈ ℕ0 (𝐹𝑗) ∈ ℂ)
189 fveq2 5511 . . . . . . 7 (𝑗 = 𝑚 → (𝐹𝑗) = (𝐹𝑚))
190189eleq1d 2246 . . . . . 6 (𝑗 = 𝑚 → ((𝐹𝑗) ∈ ℂ ↔ (𝐹𝑚) ∈ ℂ))
191190rspccva 2840 . . . . 5 ((∀𝑗 ∈ ℕ0 (𝐹𝑗) ∈ ℂ ∧ 𝑚 ∈ ℕ0) → (𝐹𝑚) ∈ ℂ)
192188, 191sylan 283 . . . 4 ((𝜑𝑚 ∈ ℕ0) → (𝐹𝑚) ∈ ℂ)
19382adantr 276 . . . . . 6 ((𝜑𝑚 ∈ ℕ0) → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ)
194193, 192mulcld 7968 . . . . 5 ((𝜑𝑚 ∈ ℕ0) → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑚)) ∈ ℂ)
195 fveq2 5511 . . . . . . 7 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
196195oveq2d 5885 . . . . . 6 (𝑛 = 𝑚 → (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑚)))
197196, 155fvmptg 5588 . . . . 5 ((𝑚 ∈ ℕ0 ∧ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑚)) ∈ ℂ) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑚)))
198158, 194, 197syl2anc 411 . . . 4 ((𝜑𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))‘𝑚) = (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑚)))
1991, 2, 82, 187, 192, 198isermulc2 11332 . . 3 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))) ⇝ (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴))
2001, 2, 33, 12, 186isumcl 11417 . . . 4 (𝜑 → Σ𝑗 ∈ ℕ0 𝐴 ∈ ℂ)
20182, 200mulcomd 7969 . . 3 (𝜑 → (Σ𝑘 ∈ ℕ0 𝐵 · Σ𝑗 ∈ ℕ0 𝐴) = (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
202199, 201breqtrd 4026 . 2 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (Σ𝑘 ∈ ℕ0 𝐵 · (𝐹𝑛)))) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
2031, 2, 4, 32, 185, 2022clim 11293 1 (𝜑 → seq0( + , 𝐻) ⇝ (Σ𝑗 ∈ ℕ0 𝐴 · Σ𝑘 ∈ ℕ0 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  {cab 2163  wral 2455  wrex 2456  Vcvv 2737   class class class wbr 4000  cmpt 4061  dom cdm 4623  cfv 5212  (class class class)co 5869  cc 7800  0cc0 7802  1c1 7803   + caddc 7805   · cmul 7807   < clt 7982  cmin 8118   / cdiv 8618  cn 8908  2c2 8959  0cn0 9165  cz 9242  cuz 9517  +crp 9640  ...cfz 9995  seqcseq 10431  abscabs 10990  cli 11270  Σcsu 11345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-disj 3978  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-oadd 6415  df-er 6529  df-en 6735  df-dom 6736  df-fin 6737  df-sup 6977  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-ico 9881  df-fz 9996  df-fzo 10129  df-seqfrec 10432  df-exp 10506  df-ihash 10740  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-clim 11271  df-sumdc 11346
This theorem is referenced by:  efaddlem  11666
  Copyright terms: Public domain W3C validator