Step | Hyp | Ref
| Expression |
1 | | nnuz 12033 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11764 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | eqid 2778 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) |
4 | | lgamcvg.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
5 | | 1nn0 11664 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
7 | 4, 6 | dmgmaddnn0 25209 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ
∖ ℕ))) |
8 | 3, 7 | lgamcvg 25236 |
. . 3
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1)))) |
9 | | seqex 13125 |
. . . 4
⊢ seq1( + ,
𝐺) ∈
V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , 𝐺) ∈ V) |
11 | 4 | eldifad 3804 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
12 | 11 | abscld 14587 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
13 | | arch 11643 |
. . . . . . 7
⊢
((abs‘𝐴)
∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟) |
15 | | eqid 2778 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑟) = (ℤ≥‘𝑟) |
16 | | simprl 761 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ) |
17 | 16 | nnzd 11837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ) |
18 | | eqid 2778 |
. . . . . . . . . . 11
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
19 | 18 | logcn 24834 |
. . . . . . . . . 10
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖
(-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)) |
21 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
22 | 21 | dvlog2lem 24839 |
. . . . . . . . . . 11
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
(-∞(,]0)) |
23 | 11 | ad2antrr 716 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝐴 ∈ ℂ) |
24 | | eluznn 12069 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘𝑟)) → 𝑚 ∈ ℕ) |
25 | 24 | ex 403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℕ → (𝑚 ∈
(ℤ≥‘𝑟) → 𝑚 ∈ ℕ)) |
26 | 25 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) → 𝑚 ∈ ℕ)) |
27 | 26 | imp 397 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑚 ∈ ℕ) |
28 | 27 | nncnd 11396 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑚 ∈ ℂ) |
29 | | 1cnd 10373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℂ) |
30 | 28, 29 | addcld 10398 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℂ) |
31 | 27 | peano2nnd 11397 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℕ) |
32 | 31 | nnne0d 11429 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ≠ 0) |
33 | 23, 30, 32 | divcld 11153 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ) |
34 | 33, 29 | addcld 10398 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ) |
35 | | ax-1cn 10332 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
36 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) |
37 | 36 | cnmetdval 22986 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈
ℂ) → (((𝐴 /
(𝑚 + 1)) + 1)(abs ∘
− )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1))) |
38 | 34, 35, 37 | sylancl 580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) =
(abs‘(((𝐴 / (𝑚 + 1)) + 1) −
1))) |
39 | 33, 29 | pncand 10737 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1))) |
40 | 39 | fveq2d 6452 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1)))) |
41 | 23, 30, 32 | absdivd 14606 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1)))) |
42 | 31 | nnred 11395 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℝ) |
43 | 31 | nnrpd 12183 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈
ℝ+) |
44 | 43 | rpge0d 12189 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 0 ≤ (𝑚 + 1)) |
45 | 42, 44 | absidd 14573 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1)) |
46 | 45 | oveq2d 6940 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1))) |
47 | 41, 46 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1))) |
48 | 38, 40, 47 | 3eqtrd 2818 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) =
((abs‘𝐴) / (𝑚 + 1))) |
49 | 12 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) ∈
ℝ) |
50 | 16 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ∈ ℕ) |
51 | 50 | nnred 11395 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ∈ ℝ) |
52 | | simplrr 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < 𝑟) |
53 | | eluzle 12009 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘𝑟) → 𝑟 ≤ 𝑚) |
54 | 53 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ≤ 𝑚) |
55 | | nnleltp1 11788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1))) |
56 | 50, 27, 55 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1))) |
57 | 54, 56 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 < (𝑚 + 1)) |
58 | 49, 51, 42, 52, 57 | lttrd 10539 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < (𝑚 + 1)) |
59 | 30 | mulid1d 10396 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1)) |
60 | 58, 59 | breqtrrd 4916 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1)) |
61 | | 1red 10379 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℝ) |
62 | 49, 61, 43 | ltdivmuld 12236 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1))) |
63 | 60, 62 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1) |
64 | 48, 63 | eqbrtrd 4910 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) <
1) |
65 | | cnxmet 22988 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
67 | | 1rp 12145 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
68 | | rpxr 12152 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
69 | 67, 68 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℝ*) |
70 | | elbl3 22609 |
. . . . . . . . . . . . 13
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (1 ∈ ℂ ∧ ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘
− ))1) ↔ (((𝐴 /
(𝑚 + 1)) + 1)(abs ∘
− )1) < 1)) |
71 | 66, 69, 29, 34, 70 | syl22anc 829 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘
− ))1) ↔ (((𝐴 /
(𝑚 + 1)) + 1)(abs ∘
− )1) < 1)) |
72 | 64, 71 | mpbird 249 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘
− ))1)) |
73 | 22, 72 | sseldi 3819 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖
(-∞(,]0))) |
74 | 73 | fmpttd 6651 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) +
1)):(ℤ≥‘𝑟)⟶(ℂ ∖
(-∞(,]0))) |
75 | 26 | ssrdv 3827 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ≥‘𝑟) ⊆
ℕ) |
76 | 75 | resmptd 5704 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) |
77 | 12 | recnd 10407 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) |
78 | | divcnv 14993 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘𝐴)
∈ ℂ → (𝑚
∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0) |
80 | | nnex 11385 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ
∈ V |
81 | 80 | mptex 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1)))) ∈
V |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V) |
83 | | oveq2 6932 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → ((abs‘𝐴) / 𝑚) = ((abs‘𝐴) / 𝑛)) |
84 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦
((abs‘𝐴) / 𝑚)) = (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) |
85 | | ovex 6956 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘𝐴) /
𝑛) ∈
V |
86 | 83, 84, 85 | fvmpt 6544 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛)) |
87 | 86 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛)) |
88 | 11 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ) |
89 | 88 | abscld 14587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘𝐴) ∈
ℝ) |
90 | | simpr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
91 | 89, 90 | nndivred 11433 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / 𝑛) ∈ ℝ) |
92 | 87, 91 | eqeltrd 2859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) ∈ ℝ) |
93 | | oveq1 6931 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
94 | 93 | oveq2d 6940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1))) |
95 | 94 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (abs‘(𝐴 / (𝑚 + 1))) = (abs‘(𝐴 / (𝑛 + 1)))) |
96 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1)))) = (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) |
97 | | fvex 6461 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs‘(𝐴 /
(𝑛 + 1))) ∈
V |
98 | 95, 96, 97 | fvmpt 6544 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1)))) |
99 | 98 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1)))) |
100 | 90 | nncnd 11396 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
101 | | 1cnd 10373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
102 | 100, 101 | addcld 10398 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ) |
103 | 90 | peano2nnd 11397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
104 | 103 | nnne0d 11429 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0) |
105 | 88, 102, 104 | divcld 11153 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ) |
106 | 105 | abscld 14587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ∈ ℝ) |
107 | 99, 106 | eqeltrd 2859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ∈ ℝ) |
108 | 88, 102, 104 | absdivd 14606 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (abs‘(𝑛 + 1)))) |
109 | 103 | nnred 11395 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
110 | 103 | nnrpd 12183 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) |
111 | 110 | rpge0d 12189 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑛 + 1)) |
112 | 109, 111 | absidd 14573 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝑛 + 1)) = (𝑛 + 1)) |
113 | 112 | oveq2d 6940 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / (abs‘(𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1))) |
114 | 108, 113 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1))) |
115 | 90 | nnrpd 12183 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
116 | 88 | absge0d 14595 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(abs‘𝐴)) |
117 | 90 | nnred 11395 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
118 | 117 | lep1d 11311 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
119 | 115, 110,
89, 116, 118 | lediv2ad 12207 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / (𝑛 + 1)) ≤ ((abs‘𝐴) / 𝑛)) |
120 | 114, 119 | eqbrtrd 4910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ≤ ((abs‘𝐴) / 𝑛)) |
121 | 120, 99, 87 | 3brtr4d 4920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ≤ ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛)) |
122 | 105 | absge0d 14595 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(abs‘(𝐴 / (𝑛 + 1)))) |
123 | 122, 99 | breqtrrd 4916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1))))‘𝑛)) |
124 | 1, 2, 79, 82, 92, 107, 121, 123 | climsqz2 14784 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0) |
125 | 80 | mptex 6760 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V) |
127 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) |
128 | | ovex 6956 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 / (𝑛 + 1)) ∈ V |
129 | 94, 127, 128 | fvmpt 6544 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1))) |
130 | 129 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1))) |
131 | 130, 105 | eqeltrd 2859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ) |
132 | 130 | fveq2d 6452 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)) = (abs‘(𝐴 / (𝑛 + 1)))) |
133 | 99, 132 | eqtr4d 2817 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛))) |
134 | 1, 2, 126, 82, 131, 133 | climabs0 14728 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0)) |
135 | 124, 134 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0) |
136 | | 1cnd 10373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) |
137 | 80 | mptex 6760 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) |
139 | 94 | oveq1d 6939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1)) |
140 | | eqid 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) |
141 | | ovex 6956 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 / (𝑛 + 1)) + 1) ∈ V |
142 | 139, 140,
141 | fvmpt 6544 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1)) |
143 | 142 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1)) |
144 | 130 | oveq1d 6939 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1)) |
145 | 143, 144 | eqtr4d 2817 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1)) |
146 | 1, 2, 135, 136, 138, 131, 145 | climaddc1 14777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 +
1)) |
147 | | 0p1e1 11508 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
148 | 146, 147 | syl6breq 4929 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
149 | 148 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
150 | | climres 14718 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)) |
151 | 17, 137, 150 | sylancl 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)) |
152 | 149, 151 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1) |
153 | 76, 152 | eqbrtrrd 4912 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
154 | 67 | a1i 11 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ → 1 ∈ ℝ+) |
155 | 18 | ellogdm 24826 |
. . . . . . . . . . 11
⊢ (1 ∈
(ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈
ℝ → 1 ∈ ℝ+))) |
156 | 35, 154, 155 | mpbir2an 701 |
. . . . . . . . . 10
⊢ 1 ∈
(ℂ ∖ (-∞(,]0)) |
157 | 156 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖
(-∞(,]0))) |
158 | 15, 17, 20, 74, 153, 157 | climcncf 23115 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ
∖ (-∞(,]0)))‘1)) |
159 | 18 | logdmss 24829 |
. . . . . . . . . . 11
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
160 | 159, 73 | sseldi 3819 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖
{0})) |
161 | | eqidd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) |
162 | | logf1o 24752 |
. . . . . . . . . . . 12
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
163 | | f1of 6393 |
. . . . . . . . . . . 12
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
164 | 162, 163 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖
{0})⟶ran log) |
165 | 164 | feqmptd 6511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log = (𝑥 ∈ (ℂ ∖ {0}) ↦
(log‘𝑥))) |
166 | | fveq2 6448 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝐴 / (𝑚 + 1)) + 1) → (log‘𝑥) = (log‘((𝐴 / (𝑚 + 1)) + 1))) |
167 | 160, 161,
165, 166 | fmptco 6663 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))) |
168 | | frn 6299 |
. . . . . . . . . 10
⊢ ((𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) +
1)):(ℤ≥‘𝑟)⟶(ℂ ∖ (-∞(,]0))
→ ran (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖
(-∞(,]0))) |
169 | | cores 5894 |
. . . . . . . . . 10
⊢ (ran
(𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖
(-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘
(𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))) |
170 | 74, 168, 169 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))) |
171 | 75 | resmptd 5704 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))) |
172 | 167, 170,
171 | 3eqtr4d 2824 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟))) |
173 | | fvres 6467 |
. . . . . . . . . 10
⊢ (1 ∈
(ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = (log‘1)) |
174 | 156, 173 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = (log‘1)) |
175 | | log1 24773 |
. . . . . . . . 9
⊢
(log‘1) = 0 |
176 | 174, 175 | syl6eq 2830 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = 0) |
177 | 158, 172,
176 | 3brtr3d 4919 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0) |
178 | 80 | mptex 6760 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ∈
V |
179 | | climres 14718 |
. . . . . . . 8
⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) →
(((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)) |
180 | 17, 178, 179 | sylancl 580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)) |
181 | 177, 180 | mpbid 224 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0) |
182 | 14, 181 | rexlimddv 3218 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0) |
183 | 11, 136 | addcld 10398 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 1) ∈ ℂ) |
184 | 7 | dmgmn0 25208 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 1) ≠ 0) |
185 | 183, 184 | logcld 24758 |
. . . . 5
⊢ (𝜑 → (log‘(𝐴 + 1)) ∈
ℂ) |
186 | 80 | mptex 6760 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) + 1)))) ∈
V |
187 | 186 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈
V) |
188 | 94 | fvoveq1d 6946 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
189 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) |
190 | | fvex 6461 |
. . . . . . . 8
⊢
(log‘((𝐴 /
(𝑛 + 1)) + 1)) ∈
V |
191 | 188, 189,
190 | fvmpt 6544 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
192 | 191 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
193 | 105, 101 | addcld 10398 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ) |
194 | 4 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
195 | 194, 103 | dmgmdivn0 25210 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0) |
196 | 193, 195 | logcld 24758 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ) |
197 | 192, 196 | eqeltrd 2859 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ) |
198 | 188 | oveq2d 6940 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
199 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1)))) |
200 | | ovex 6956 |
. . . . . . . 8
⊢
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) + 1))) ∈
V |
201 | 198, 199,
200 | fvmpt 6544 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1))))‘𝑛) =
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) +
1)))) |
202 | 201 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
203 | 192 | oveq2d 6940 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
204 | 202, 203 | eqtr4d 2817 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛))) |
205 | 1, 2, 182, 185, 187, 197, 204 | climsubc2 14781 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝
((log‘(𝐴 + 1))
− 0)) |
206 | 185 | subid1d 10725 |
. . . 4
⊢ (𝜑 → ((log‘(𝐴 + 1)) − 0) =
(log‘(𝐴 +
1))) |
207 | 205, 206 | breqtrd 4914 |
. . 3
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝
(log‘(𝐴 +
1))) |
208 | | elfznn 12691 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
209 | 208 | adantl 475 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
210 | | oveq1 6931 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1)) |
211 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
212 | 210, 211 | oveq12d 6942 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘)) |
213 | 212 | fveq2d 6452 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘))) |
214 | 213 | oveq2d 6940 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘)))) |
215 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘)) |
216 | 215 | fvoveq1d 6946 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1))) |
217 | 214, 216 | oveq12d 6942 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
218 | | ovex 6956 |
. . . . . . 7
⊢ (((𝐴 + 1) ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V |
219 | 217, 3, 218 | fvmpt 6544 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
220 | 209, 219 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
221 | 90, 1 | syl6eleq 2869 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
222 | 11 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
223 | | 1cnd 10373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ) |
224 | 222, 223 | addcld 10398 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ) |
225 | 209 | peano2nnd 11397 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ) |
226 | 225 | nnrpd 12183 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈
ℝ+) |
227 | 209 | nnrpd 12183 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+) |
228 | 226, 227 | rpdivcld 12202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈
ℝ+) |
229 | 228 | relogcld 24810 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ) |
230 | 229 | recnd 10407 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ) |
231 | 224, 230 | mulcld 10399 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ) |
232 | 209 | nncnd 11396 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ) |
233 | 209 | nnne0d 11429 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0) |
234 | 224, 232,
233 | divcld 11153 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ) |
235 | 234, 223 | addcld 10398 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ) |
236 | 7 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ
∖ ℕ))) |
237 | 236, 209 | dmgmdivn0 25210 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0) |
238 | 235, 237 | logcld 24758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ) |
239 | 231, 238 | subcld 10736 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
240 | 220, 221,
239 | fsumser 14872 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛)) |
241 | | fzfid 13095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
242 | 241, 239 | fsumcl 14875 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
243 | 240, 242 | eqeltrrd 2860 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ) |
244 | 185 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈
ℂ) |
245 | 244, 196 | subcld 10736 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) ∈
ℂ) |
246 | 202, 245 | eqeltrd 2859 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈
ℂ) |
247 | 222, 230 | mulcld 10399 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ) |
248 | 222, 232,
233 | divcld 11153 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ) |
249 | 248, 223 | addcld 10398 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ) |
250 | 4 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
251 | 250, 209 | dmgmdivn0 25210 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0) |
252 | 249, 251 | logcld 24758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ) |
253 | 247, 252 | subcld 10736 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
254 | 241, 253 | fsumcl 14875 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
255 | 242, 254 | nncand 10741 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) = Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
256 | 231, 238,
247, 252 | sub4d 10785 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1))))) |
257 | 222, 223 | pncan2d 10738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1) |
258 | 257 | oveq1d 6939 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘)))) |
259 | 224, 222,
230 | subdird 10834 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘))))) |
260 | 230 | mulid2d 10397 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘))) |
261 | 258, 259,
260 | 3eqtr3d 2822 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘))) |
262 | 261 | oveq1d 6939 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1))))) |
263 | 230, 238,
252 | subsubd 10764 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1)))) |
264 | 230, 238 | subcld 10736 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
265 | 264, 252 | addcomd 10580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))))) |
266 | 252, 238,
230 | subsub2d 10765 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))))) |
267 | 225 | nncnd 11396 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ) |
268 | 222, 267 | addcld 10398 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ) |
269 | 225 | nnnn0d 11706 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈
ℕ0) |
270 | | dmgmaddn0 25205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) →
(𝐴 + (𝑘 + 1)) ≠ 0) |
271 | 250, 269,
270 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0) |
272 | 268, 271 | logcld 24758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ) |
273 | 226 | relogcld 24810 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ) |
274 | 273 | recnd 10407 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ) |
275 | 227 | relogcld 24810 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ) |
276 | 275 | recnd 10407 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ) |
277 | 272, 274,
276 | nnncan2d 10771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
278 | 224, 232,
232, 233 | divdird 11191 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘))) |
279 | 222, 232,
223 | add32d 10605 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘)) |
280 | 222, 232,
223 | addassd 10401 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1))) |
281 | 279, 280 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1))) |
282 | 281 | oveq1d 6939 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘)) |
283 | 232, 233 | dividd 11151 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1) |
284 | 283 | oveq2d 6940 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1)) |
285 | 278, 282,
284 | 3eqtr3rd 2823 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘)) |
286 | 285 | fveq2d 6452 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘))) |
287 | | logdiv2 24804 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) →
(log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
288 | 268, 271,
227, 287 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
289 | 286, 288 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
290 | 226, 227 | relogdivd 24813 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘))) |
291 | 289, 290 | oveq12d 6942 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘)))) |
292 | 225 | nnne0d 11429 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0) |
293 | 222, 267,
267, 292 | divdird 11191 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1)))) |
294 | 267, 292 | dividd 11151 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1) |
295 | 294 | oveq2d 6940 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1)) |
296 | 293, 295 | eqtr2d 2815 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) |
297 | 296 | fveq2d 6452 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))) |
298 | | logdiv2 24804 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) →
(log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
299 | 268, 271,
226, 298 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
300 | 297, 299 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
301 | 277, 291,
300 | 3eqtr4d 2824 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1))) |
302 | 301 | oveq2d 6940 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
303 | 266, 302 | eqtr3d 2816 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
304 | 263, 265,
303 | 3eqtrd 2818 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
305 | 256, 262,
304 | 3eqtrd 2818 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
306 | 305 | sumeq2dv 14845 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
307 | 241, 239,
253 | fsumsub 14928 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) |
308 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘)) |
309 | 308 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
310 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1))) |
311 | 310 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1))) |
312 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1)) |
313 | 312 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1))) |
314 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1))) |
315 | 314 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
316 | 90 | nnzd 11837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
317 | 103, 1 | syl6eleq 2869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
(ℤ≥‘1)) |
318 | 11 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ) |
319 | | elfznn 12691 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ) |
320 | 319 | adantl 475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ) |
321 | 320 | nncnd 11396 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ) |
322 | 320 | nnne0d 11429 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0) |
323 | 318, 321,
322 | divcld 11153 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ) |
324 | | 1cnd 10373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈
ℂ) |
325 | 323, 324 | addcld 10398 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ) |
326 | 4 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
327 | 326, 320 | dmgmdivn0 25210 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0) |
328 | 325, 327 | logcld 24758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ) |
329 | 309, 311,
313, 315, 316, 317, 328 | telfsum 14944 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
330 | 88 | div1d 11145 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴) |
331 | 330 | fvoveq1d 6946 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1))) |
332 | 331 | oveq1d 6939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) =
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) +
1)))) |
333 | 329, 332 | eqtrd 2814 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
334 | 306, 307,
333 | 3eqtr3d 2822 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))) |
335 | 334 | oveq2d 6940 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))))) |
336 | 255, 335 | eqtr3d 2816 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))))) |
337 | 213 | oveq2d 6940 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) |
338 | | oveq2 6932 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘)) |
339 | 338 | fvoveq1d 6946 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
340 | 337, 339 | oveq12d 6942 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
341 | | lgamcvg.g |
. . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
342 | | ovex 6956 |
. . . . . . 7
⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V |
343 | 340, 341,
342 | fvmpt 6544 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
344 | 209, 343 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
345 | 344, 221,
253 | fsumser 14872 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛)) |
346 | 202 | eqcomd 2784 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1))))‘𝑛)) |
347 | 240, 346 | oveq12d 6942 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) = ((seq1( + ,
(𝑚 ∈ ℕ ↦
(((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))) |
348 | 336, 345,
347 | 3eqtr3d 2822 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))) |
349 | 1, 2, 8, 10, 207, 243, 246, 348 | climsub 14776 |
. 2
⊢ (𝜑 → seq1( + , 𝐺) ⇝ (((log
Γ‘(𝐴 + 1)) +
(log‘(𝐴 + 1)))
− (log‘(𝐴 +
1)))) |
350 | | lgamcl 25223 |
. . . 4
⊢ ((𝐴 + 1) ∈ (ℂ ∖
(ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ) |
351 | 7, 350 | syl 17 |
. . 3
⊢ (𝜑 → (log Γ‘(𝐴 + 1)) ∈
ℂ) |
352 | 351, 185 | pncand 10737 |
. 2
⊢ (𝜑 → (((log
Γ‘(𝐴 + 1)) +
(log‘(𝐴 + 1)))
− (log‘(𝐴 +
1))) = (log Γ‘(𝐴 + 1))) |
353 | 349, 352 | breqtrd 4914 |
1
⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log
Γ‘(𝐴 +
1))) |