Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | eqid 2622 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))) |
4 | | lgamcvg.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
5 | | 1nn0 11308 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
7 | 4, 6 | dmgmaddnn0 24753 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ∈ (ℂ ∖ (ℤ
∖ ℕ))) |
8 | 3, 7 | lgamcvg 24780 |
. . 3
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))) ⇝ ((log Γ‘(𝐴 + 1)) + (log‘(𝐴 + 1)))) |
9 | | seqex 12803 |
. . . 4
⊢ seq1( + ,
𝐺) ∈
V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → seq1( + , 𝐺) ∈ V) |
11 | 4 | eldifad 3586 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
12 | 11 | abscld 14175 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐴) ∈
ℝ) |
13 | | arch 11289 |
. . . . . . 7
⊢
((abs‘𝐴)
∈ ℝ → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∃𝑟 ∈ ℕ (abs‘𝐴) < 𝑟) |
15 | | eqid 2622 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑟) = (ℤ≥‘𝑟) |
16 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℕ) |
17 | 16 | nnzd 11481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 𝑟 ∈ ℤ) |
18 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (ℂ
∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0)) |
19 | 18 | logcn 24393 |
. . . . . . . . . 10
⊢ (log
↾ (ℂ ∖ (-∞(,]0))) ∈ ((ℂ ∖
(-∞(,]0))–cn→ℂ) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ↾ (ℂ ∖
(-∞(,]0))) ∈ ((ℂ ∖ (-∞(,]0))–cn→ℂ)) |
21 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(1(ball‘(abs ∘ − ))1) = (1(ball‘(abs ∘
− ))1) |
22 | 21 | dvlog2lem 24398 |
. . . . . . . . . . 11
⊢
(1(ball‘(abs ∘ − ))1) ⊆ (ℂ ∖
(-∞(,]0)) |
23 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝐴 ∈ ℂ) |
24 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘𝑟)) → 𝑚 ∈ ℕ) |
25 | 24 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 ∈ ℕ → (𝑚 ∈
(ℤ≥‘𝑟) → 𝑚 ∈ ℕ)) |
26 | 25 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) → 𝑚 ∈ ℕ)) |
27 | 26 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑚 ∈ ℕ) |
28 | 27 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑚 ∈ ℂ) |
29 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℂ) |
30 | 28, 29 | addcld 10059 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℂ) |
31 | 27 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℕ) |
32 | 31 | nnne0d 11065 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ≠ 0) |
33 | 23, 30, 32 | divcld 10801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝐴 / (𝑚 + 1)) ∈ ℂ) |
34 | 33, 29 | addcld 10059 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ) |
35 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) |
37 | 36 | cnmetdval 22574 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 / (𝑚 + 1)) + 1) ∈ ℂ ∧ 1 ∈
ℂ) → (((𝐴 /
(𝑚 + 1)) + 1)(abs ∘
− )1) = (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1))) |
38 | 34, 35, 37 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) =
(abs‘(((𝐴 / (𝑚 + 1)) + 1) −
1))) |
39 | 33, 29 | pncand 10393 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) − 1) = (𝐴 / (𝑚 + 1))) |
40 | 39 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(((𝐴 / (𝑚 + 1)) + 1) − 1)) = (abs‘(𝐴 / (𝑚 + 1)))) |
41 | 23, 30, 32 | absdivd 14194 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (abs‘(𝑚 + 1)))) |
42 | 31 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈ ℝ) |
43 | 31 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑚 + 1) ∈
ℝ+) |
44 | 43 | rpge0d 11876 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 0 ≤ (𝑚 + 1)) |
45 | 42, 44 | absidd 14161 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝑚 + 1)) = (𝑚 + 1)) |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((abs‘𝐴) / (abs‘(𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1))) |
47 | 41, 46 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘(𝐴 / (𝑚 + 1))) = ((abs‘𝐴) / (𝑚 + 1))) |
48 | 38, 40, 47 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) =
((abs‘𝐴) / (𝑚 + 1))) |
49 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) ∈
ℝ) |
50 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ∈ ℕ) |
51 | 50 | nnred 11035 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ∈ ℝ) |
52 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < 𝑟) |
53 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘𝑟) → 𝑟 ≤ 𝑚) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 ≤ 𝑚) |
55 | | nnleltp1 11432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1))) |
56 | 50, 27, 55 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (𝑟 ≤ 𝑚 ↔ 𝑟 < (𝑚 + 1))) |
57 | 54, 56 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 𝑟 < (𝑚 + 1)) |
58 | 49, 51, 42, 52, 57 | lttrd 10198 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < (𝑚 + 1)) |
59 | 30 | mulid1d 10057 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝑚 + 1) · 1) = (𝑚 + 1)) |
60 | 58, 59 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs‘𝐴) < ((𝑚 + 1) · 1)) |
61 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℝ) |
62 | 49, 61, 43 | ltdivmuld 11923 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((abs‘𝐴) / (𝑚 + 1)) < 1 ↔ (abs‘𝐴) < ((𝑚 + 1) · 1))) |
63 | 60, 62 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((abs‘𝐴) / (𝑚 + 1)) < 1) |
64 | 48, 63 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1)(abs ∘ − )1) <
1) |
65 | | cnxmet 22576 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (abs ∘ − )
∈ (∞Met‘ℂ)) |
67 | | 1rp 11836 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
68 | | rpxr 11840 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
69 | 67, 68 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → 1 ∈
ℝ*) |
70 | | elbl3 22197 |
. . . . . . . . . . . . 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 1327 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → (((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘
− ))1) ↔ (((𝐴 /
(𝑚 + 1)) + 1)(abs ∘
− )1) < 1)) |
72 | 64, 71 | mpbird 247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (1(ball‘(abs ∘
− ))1)) |
73 | 22, 72 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖
(-∞(,]0))) |
74 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) |
75 | 73, 74 | fmptd 6385 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) +
1)):(ℤ≥‘𝑟)⟶(ℂ ∖
(-∞(,]0))) |
76 | 26 | ssrdv 3609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (ℤ≥‘𝑟) ⊆
ℕ) |
77 | 76 | resmptd 5452 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) |
78 | 12 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝐴) ∈
ℂ) |
79 | | divcnv 14585 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘𝐴)
∈ ℂ → (𝑚
∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) ⇝ 0) |
81 | | nnex 11026 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ
∈ V |
82 | 81 | mptex 6486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1)))) ∈
V |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ∈ V) |
84 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → ((abs‘𝐴) / 𝑚) = ((abs‘𝐴) / 𝑛)) |
85 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦
((abs‘𝐴) / 𝑚)) = (𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚)) |
86 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘𝐴) /
𝑛) ∈
V |
87 | 84, 85, 86 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛)) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) = ((abs‘𝐴) / 𝑛)) |
89 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ) |
90 | 89 | abscld 14175 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘𝐴) ∈
ℝ) |
91 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
92 | 90, 91 | nndivred 11069 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / 𝑛) ∈ ℝ) |
93 | 88, 92 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛) ∈ ℝ) |
94 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
95 | 94 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (𝐴 / (𝑚 + 1)) = (𝐴 / (𝑛 + 1))) |
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (abs‘(𝐴 / (𝑚 + 1))) = (abs‘(𝐴 / (𝑛 + 1)))) |
97 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1)))) = (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) |
98 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs‘(𝐴 /
(𝑛 + 1))) ∈
V |
99 | 96, 97, 98 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1)))) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘(𝐴 / (𝑛 + 1)))) |
101 | 91 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
102 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
103 | 101, 102 | addcld 10059 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ) |
104 | 91 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
105 | 104 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0) |
106 | 89, 103, 105 | divcld 10801 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / (𝑛 + 1)) ∈ ℂ) |
107 | 106 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ∈ ℝ) |
108 | 100, 107 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ∈ ℝ) |
109 | 89, 103, 105 | absdivd 14194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (abs‘(𝑛 + 1)))) |
110 | 104 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ) |
111 | 104 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) |
112 | 111 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝑛 + 1)) |
113 | 110, 112 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝑛 + 1)) = (𝑛 + 1)) |
114 | 113 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / (abs‘(𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1))) |
115 | 109, 114 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) = ((abs‘𝐴) / (𝑛 + 1))) |
116 | 91 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
117 | 89 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(abs‘𝐴)) |
118 | 91 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ) |
119 | 118 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≤ (𝑛 + 1)) |
120 | 116, 111,
90, 117, 119 | lediv2ad 11894 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((abs‘𝐴) / (𝑛 + 1)) ≤ ((abs‘𝐴) / 𝑛)) |
121 | 115, 120 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘(𝐴 / (𝑛 + 1))) ≤ ((abs‘𝐴) / 𝑛)) |
122 | 121, 100,
88 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) ≤ ((𝑚 ∈ ℕ ↦ ((abs‘𝐴) / 𝑚))‘𝑛)) |
123 | 106 | absge0d 14183 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(abs‘(𝐴 / (𝑛 + 1)))) |
124 | 123, 100 | breqtrrd 4681 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ ((𝑚 ∈ ℕ ↦
(abs‘(𝐴 / (𝑚 + 1))))‘𝑛)) |
125 | 1, 2, 80, 83, 93, 108, 122, 124 | climsqz2 14372 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0) |
126 | 81 | mptex 6486 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ∈ V) |
128 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) = (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) |
129 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 / (𝑛 + 1)) ∈ V |
130 | 95, 128, 129 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1))) |
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) = (𝐴 / (𝑛 + 1))) |
132 | 131, 106 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) ∈ ℂ) |
133 | 131 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛)) = (abs‘(𝐴 / (𝑛 + 1)))) |
134 | 100, 133 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1))))‘𝑛) = (abs‘((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛))) |
135 | 1, 2, 127, 83, 132, 134 | climabs0 14316 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (abs‘(𝐴 / (𝑚 + 1)))) ⇝ 0)) |
136 | 125, 135 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1))) ⇝ 0) |
137 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℂ) |
138 | 81 | mptex 6486 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) |
140 | 95 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → ((𝐴 / (𝑚 + 1)) + 1) = ((𝐴 / (𝑛 + 1)) + 1)) |
141 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) |
142 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 / (𝑛 + 1)) + 1) ∈ V |
143 | 140, 141,
142 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1)) |
144 | 143 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = ((𝐴 / (𝑛 + 1)) + 1)) |
145 | 131 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1) = ((𝐴 / (𝑛 + 1)) + 1)) |
146 | 144, 145 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1))‘𝑛) = (((𝑚 ∈ ℕ ↦ (𝐴 / (𝑚 + 1)))‘𝑛) + 1)) |
147 | 1, 2, 136, 137, 139, 132, 146 | climaddc1 14365 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ (0 +
1)) |
148 | | 0p1e1 11132 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
149 | 147, 148 | syl6breq 4694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
150 | 149 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
151 | | climres 14306 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ∈ V) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)) |
152 | 17, 138, 151 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1 ↔ (𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1)) |
153 | 150, 152 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ ((𝐴 / (𝑚 + 1)) + 1)) ↾
(ℤ≥‘𝑟)) ⇝ 1) |
154 | 77, 153 | eqbrtrrd 4677 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⇝ 1) |
155 | 67 | a1i 11 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ → 1 ∈ ℝ+) |
156 | 18 | ellogdm 24385 |
. . . . . . . . . . 11
⊢ (1 ∈
(ℂ ∖ (-∞(,]0)) ↔ (1 ∈ ℂ ∧ (1 ∈
ℝ → 1 ∈ ℝ+))) |
157 | 35, 155, 156 | mpbir2an 955 |
. . . . . . . . . 10
⊢ 1 ∈
(ℂ ∖ (-∞(,]0)) |
158 | 157 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → 1 ∈ (ℂ ∖
(-∞(,]0))) |
159 | 15, 17, 20, 75, 154, 158 | climcncf 22703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) ⇝ ((log ↾ (ℂ
∖ (-∞(,]0)))‘1)) |
160 | 18 | logdmss 24388 |
. . . . . . . . . . 11
⊢ (ℂ
∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}) |
161 | 160, 73 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) ∧ 𝑚 ∈ (ℤ≥‘𝑟)) → ((𝐴 / (𝑚 + 1)) + 1) ∈ (ℂ ∖
{0})) |
162 | | eqidd 2623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) |
163 | | logf1o 24311 |
. . . . . . . . . . . 12
⊢
log:(ℂ ∖ {0})–1-1-onto→ran
log |
164 | | f1of 6137 |
. . . . . . . . . . . 12
⊢
(log:(ℂ ∖ {0})–1-1-onto→ran
log → log:(ℂ ∖ {0})⟶ran log) |
165 | 163, 164 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log:(ℂ ∖
{0})⟶ran log) |
166 | 165 | feqmptd 6249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → log = (𝑥 ∈ (ℂ ∖ {0}) ↦
(log‘𝑥))) |
167 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝐴 / (𝑚 + 1)) + 1) → (log‘𝑥) = (log‘((𝐴 / (𝑚 + 1)) + 1))) |
168 | 161, 162,
166, 167 | fmptco 6396 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (log ∘ (𝑚 ∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))) |
169 | | frn 6053 |
. . . . . . . . . 10
⊢ ((𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) +
1)):(ℤ≥‘𝑟)⟶(ℂ ∖ (-∞(,]0))
→ ran (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖
(-∞(,]0))) |
170 | | cores 5638 |
. . . . . . . . . 10
⊢ (ran
(𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)) ⊆ (ℂ ∖
(-∞(,]0)) → ((log ↾ (ℂ ∖ (-∞(,]0))) ∘
(𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))) |
171 | 75, 169, 170 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = (log ∘ (𝑚 ∈
(ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1)))) |
172 | 76 | resmptd 5452 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) = (𝑚 ∈ (ℤ≥‘𝑟) ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))) |
173 | 168, 171,
172 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0))) ∘ (𝑚
∈ (ℤ≥‘𝑟) ↦ ((𝐴 / (𝑚 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟))) |
174 | | fvres 6207 |
. . . . . . . . . 10
⊢ (1 ∈
(ℂ ∖ (-∞(,]0)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = (log‘1)) |
175 | 157, 174 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = (log‘1)) |
176 | | log1 24332 |
. . . . . . . . 9
⊢
(log‘1) = 0 |
177 | 175, 176 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((log ↾ (ℂ ∖
(-∞(,]0)))‘1) = 0) |
178 | 159, 173,
177 | 3brtr3d 4684 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0) |
179 | 81 | mptex 6486 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ∈
V |
180 | | climres 14306 |
. . . . . . . 8
⊢ ((𝑟 ∈ ℤ ∧ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ∈ V) →
(((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)) |
181 | 17, 179, 180 | sylancl 694 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ↾
(ℤ≥‘𝑟)) ⇝ 0 ↔ (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0)) |
182 | 178, 181 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ (abs‘𝐴) < 𝑟)) → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0) |
183 | 14, 182 | rexlimddv 3035 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1))) ⇝ 0) |
184 | 11, 137 | addcld 10059 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 1) ∈ ℂ) |
185 | 7 | dmgmn0 24752 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 1) ≠ 0) |
186 | 184, 185 | logcld 24317 |
. . . . 5
⊢ (𝜑 → (log‘(𝐴 + 1)) ∈
ℂ) |
187 | 81 | mptex 6486 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) + 1)))) ∈
V |
188 | 187 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ∈
V) |
189 | 140 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (log‘((𝐴 / (𝑚 + 1)) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
190 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) = (𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1))) |
191 | | fvex 6201 |
. . . . . . . 8
⊢
(log‘((𝐴 /
(𝑛 + 1)) + 1)) ∈
V |
192 | 189, 190,
191 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
193 | 192 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
194 | 106, 102 | addcld 10059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ∈ ℂ) |
195 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
196 | 195, 104 | dmgmdivn0 24754 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / (𝑛 + 1)) + 1) ≠ 0) |
197 | 194, 196 | logcld 24317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / (𝑛 + 1)) + 1)) ∈ ℂ) |
198 | 193, 197 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛) ∈ ℂ) |
199 | 189 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑚 + 1)) + 1))) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
200 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) + 1)))) = (𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1)))) |
201 | | ovex 6678 |
. . . . . . . 8
⊢
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) + 1))) ∈
V |
202 | 199, 200,
201 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1))))‘𝑛) =
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) +
1)))) |
203 | 202 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
204 | 193 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛)) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
205 | 203, 204 | eqtr4d 2659 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) = ((log‘(𝐴 + 1)) − ((𝑚 ∈ ℕ ↦
(log‘((𝐴 / (𝑚 + 1)) + 1)))‘𝑛))) |
206 | 1, 2, 183, 186, 188, 198, 205 | climsubc2 14369 |
. . . 4
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝
((log‘(𝐴 + 1))
− 0)) |
207 | 186 | subid1d 10381 |
. . . 4
⊢ (𝜑 → ((log‘(𝐴 + 1)) − 0) =
(log‘(𝐴 +
1))) |
208 | 206, 207 | breqtrd 4679 |
. . 3
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1)))) ⇝
(log‘(𝐴 +
1))) |
209 | | elfznn 12370 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
210 | 209 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
211 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑚 + 1) = (𝑘 + 1)) |
212 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
213 | 211, 212 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝑚 + 1) / 𝑚) = ((𝑘 + 1) / 𝑘)) |
214 | 213 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑘 + 1) / 𝑘))) |
215 | 214 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → ((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) = ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘)))) |
216 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝐴 + 1) / 𝑚) = ((𝐴 + 1) / 𝑘)) |
217 | 216 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (((𝐴 + 1) / 𝑚) + 1) = (((𝐴 + 1) / 𝑘) + 1)) |
218 | 217 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (log‘(((𝐴 + 1) / 𝑚) + 1)) = (log‘(((𝐴 + 1) / 𝑘) + 1))) |
219 | 215, 218 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
220 | | ovex 6678 |
. . . . . . 7
⊢ (((𝐴 + 1) ·
(log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ V |
221 | 219, 3, 220 | fvmpt 6282 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
222 | 210, 221 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1))))‘𝑘) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) |
223 | 91, 1 | syl6eleq 2711 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
(ℤ≥‘1)) |
224 | 11 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ ℂ) |
225 | | 1cnd 10056 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 1 ∈ ℂ) |
226 | 224, 225 | addcld 10059 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ ℂ) |
227 | 210 | peano2nnd 11037 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℕ) |
228 | 227 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈
ℝ+) |
229 | 210 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+) |
230 | 228, 229 | rpdivcld 11889 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / 𝑘) ∈
ℝ+) |
231 | 230 | relogcld 24369 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℝ) |
232 | 231 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) ∈ ℂ) |
233 | 226, 232 | mulcld 10060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ) |
234 | 210 | nncnd 11036 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℂ) |
235 | 210 | nnne0d 11065 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ≠ 0) |
236 | 226, 234,
235 | divcld 10801 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) / 𝑘) ∈ ℂ) |
237 | 236, 225 | addcld 10059 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ∈ ℂ) |
238 | 7 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + 1) ∈ (ℂ ∖ (ℤ
∖ ℕ))) |
239 | 238, 210 | dmgmdivn0 24754 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) ≠ 0) |
240 | 237, 239 | logcld 24317 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) ∈ ℂ) |
241 | 233, 240 | subcld 10392 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
242 | 222, 223,
241 | fsumser 14461 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) = (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛)) |
243 | | fzfid 12772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
244 | 243, 241 | fsumcl 14464 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
245 | 242, 244 | eqeltrrd 2702 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) ·
(log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) ∈ ℂ) |
246 | 186 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘(𝐴 + 1)) ∈
ℂ) |
247 | 246, 197 | subcld 10392 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) ∈
ℂ) |
248 | 203, 247 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛) ∈
ℂ) |
249 | 224, 232 | mulcld 10060 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 · (log‘((𝑘 + 1) / 𝑘))) ∈ ℂ) |
250 | 224, 234,
235 | divcld 10801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 / 𝑘) ∈ ℂ) |
251 | 250, 225 | addcld 10059 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ∈ ℂ) |
252 | 4 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
253 | 252, 210 | dmgmdivn0 24754 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / 𝑘) + 1) ≠ 0) |
254 | 251, 253 | logcld 24317 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / 𝑘) + 1)) ∈ ℂ) |
255 | 249, 254 | subcld 10392 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
256 | 243, 255 | fsumcl 14464 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ ℂ) |
257 | 244, 256 | nncand 10397 |
. . . . 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)))) |
258 | 233, 240,
249, 254 | sub4d 10441 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1))))) |
259 | 224, 225 | pncan2d 10394 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) − 𝐴) = 1) |
260 | 259 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (1 · (log‘((𝑘 + 1) / 𝑘)))) |
261 | 226, 224,
232 | subdird 10487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) − 𝐴) · (log‘((𝑘 + 1) / 𝑘))) = (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘))))) |
262 | 232 | mulid2d 10058 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1 · (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝑘 + 1) / 𝑘))) |
263 | 260, 261,
262 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) = (log‘((𝑘 + 1) / 𝑘))) |
264 | 263 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1))))) |
265 | 232, 240,
254 | subsubd 10420 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1)))) |
266 | 232, 240 | subcld 10392 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) ∈ ℂ) |
267 | 266, 254 | addcomd 10238 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))) + (log‘((𝐴 / 𝑘) + 1))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))))) |
268 | 254, 240,
232 | subsub2d 10421 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1))))) |
269 | 227 | nncnd 11036 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈ ℂ) |
270 | 224, 269 | addcld 10059 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ∈ ℂ) |
271 | 227 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ∈
ℕ0) |
272 | | dmgmaddn0 24749 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (ℂ ∖
(ℤ ∖ ℕ)) ∧ (𝑘 + 1) ∈ ℕ0) →
(𝐴 + (𝑘 + 1)) ≠ 0) |
273 | 252, 271,
272 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐴 + (𝑘 + 1)) ≠ 0) |
274 | 270, 273 | logcld 24317 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝐴 + (𝑘 + 1))) ∈ ℂ) |
275 | 228 | relogcld 24369 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℝ) |
276 | 275 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(𝑘 + 1)) ∈ ℂ) |
277 | 229 | relogcld 24369 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ) |
278 | 277 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℂ) |
279 | 274, 276,
278 | nnncan2d 10427 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
280 | 226, 234,
234, 235 | divdird 10839 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘))) |
281 | 224, 234,
225 | add32d 10263 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = ((𝐴 + 1) + 𝑘)) |
282 | 224, 234,
225 | addassd 10062 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 𝑘) + 1) = (𝐴 + (𝑘 + 1))) |
283 | 281, 282 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + 1) + 𝑘) = (𝐴 + (𝑘 + 1))) |
284 | 283 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) + 𝑘) / 𝑘) = ((𝐴 + (𝑘 + 1)) / 𝑘)) |
285 | 234, 235 | dividd 10799 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 / 𝑘) = 1) |
286 | 285 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + (𝑘 / 𝑘)) = (((𝐴 + 1) / 𝑘) + 1)) |
287 | 280, 284,
286 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((𝐴 + 1) / 𝑘) + 1) = ((𝐴 + (𝑘 + 1)) / 𝑘)) |
288 | 287 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / 𝑘))) |
289 | | logdiv2 24363 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ 𝑘 ∈ ℝ+) →
(log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
290 | 270, 273,
229, 289 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / 𝑘)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
291 | 288, 290 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘(((𝐴 + 1) / 𝑘) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘))) |
292 | 228, 229 | relogdivd 24372 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝑘 + 1) / 𝑘)) = ((log‘(𝑘 + 1)) − (log‘𝑘))) |
293 | 291, 292 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (((log‘(𝐴 + (𝑘 + 1))) − (log‘𝑘)) − ((log‘(𝑘 + 1)) − (log‘𝑘)))) |
294 | 227 | nnne0d 11065 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 1) ≠ 0) |
295 | 224, 269,
269, 294 | divdird 10839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 + (𝑘 + 1)) / (𝑘 + 1)) = ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1)))) |
296 | 269, 294 | dividd 10799 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑘 + 1) / (𝑘 + 1)) = 1) |
297 | 296 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + ((𝑘 + 1) / (𝑘 + 1))) = ((𝐴 / (𝑘 + 1)) + 1)) |
298 | 295, 297 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝐴 / (𝑘 + 1)) + 1) = ((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) |
299 | 298 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1)))) |
300 | | logdiv2 24363 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 + (𝑘 + 1)) ∈ ℂ ∧ (𝐴 + (𝑘 + 1)) ≠ 0 ∧ (𝑘 + 1) ∈ ℝ+) →
(log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
301 | 270, 273,
228, 300 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 + (𝑘 + 1)) / (𝑘 + 1))) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
302 | 299, 301 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (log‘((𝐴 / (𝑘 + 1)) + 1)) = ((log‘(𝐴 + (𝑘 + 1))) − (log‘(𝑘 + 1)))) |
303 | 279, 293,
302 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘))) = (log‘((𝐴 / (𝑘 + 1)) + 1))) |
304 | 303 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝑘 + 1) / 𝑘)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
305 | 268, 304 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝐴 / 𝑘) + 1)) + ((log‘((𝑘 + 1) / 𝑘)) − (log‘(((𝐴 + 1) / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
306 | 265, 267,
305 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((log‘((𝑘 + 1) / 𝑘)) − ((log‘(((𝐴 + 1) / 𝑘) + 1)) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
307 | 258, 264,
306 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
308 | 307 | sumeq2dv 14433 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1)))) |
309 | 243, 241,
255 | fsumsub 14520 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))))) |
310 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑘 → (𝐴 / 𝑥) = (𝐴 / 𝑘)) |
311 | 310 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑘 → ((𝐴 / 𝑥) + 1) = ((𝐴 / 𝑘) + 1)) |
312 | 311 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 𝑘 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
313 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑘 + 1))) |
314 | 313 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑘 + 1) → ((𝐴 / 𝑥) + 1) = ((𝐴 / (𝑘 + 1)) + 1)) |
315 | 314 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑘 + 1)) + 1))) |
316 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝐴 / 𝑥) = (𝐴 / 1)) |
317 | 316 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ((𝐴 / 𝑥) + 1) = ((𝐴 / 1) + 1)) |
318 | 317 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / 1) + 1))) |
319 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑛 + 1) → (𝐴 / 𝑥) = (𝐴 / (𝑛 + 1))) |
320 | 319 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑛 + 1) → ((𝐴 / 𝑥) + 1) = ((𝐴 / (𝑛 + 1)) + 1)) |
321 | 320 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → (log‘((𝐴 / 𝑥) + 1)) = (log‘((𝐴 / (𝑛 + 1)) + 1))) |
322 | 91 | nnzd 11481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
323 | 104, 1 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
(ℤ≥‘1)) |
324 | 11 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ ℂ) |
325 | | elfznn 12370 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ) |
326 | 325 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ) |
327 | 326 | nncnd 11036 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℂ) |
328 | 326 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ≠ 0) |
329 | 324, 327,
328 | divcld 10801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (𝐴 / 𝑥) ∈ ℂ) |
330 | | 1cnd 10056 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 1 ∈
ℂ) |
331 | 329, 330 | addcld 10059 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ∈ ℂ) |
332 | 4 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) |
333 | 332, 326 | dmgmdivn0 24754 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → ((𝐴 / 𝑥) + 1) ≠ 0) |
334 | 331, 333 | logcld 24317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘((𝐴 / 𝑥) + 1)) ∈ ℂ) |
335 | 312, 315,
318, 321, 322, 323, 334 | telfsum 14536 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘((𝐴 / 1) + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
336 | 89 | div1d 10793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 1) = 𝐴) |
337 | 336 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / 1) + 1) = (𝐴 + 1)) |
338 | 337 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 1) + 1)) = (log‘(𝐴 + 1))) |
339 | 338 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝐴 / 1) + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) =
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑛 + 1)) +
1)))) |
340 | 335, 339 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((log‘((𝐴 / 𝑘) + 1)) − (log‘((𝐴 / (𝑘 + 1)) + 1))) = ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1)))) |
341 | 308, 309,
340 | 3eqtr3d 2664 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) = ((log‘(𝐴 + 1)) − (log‘((𝐴 / (𝑛 + 1)) + 1)))) |
342 | 341 | oveq2d 6666 |
. . . . 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))))) |
343 | 257, 342 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (Σ𝑘 ∈ (1...𝑛)(((𝐴 + 1) · (log‘((𝑘 + 1) / 𝑘))) − (log‘(((𝐴 + 1) / 𝑘) + 1))) − ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))))) |
344 | 214 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑘 + 1) / 𝑘)))) |
345 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → (𝐴 / 𝑚) = (𝐴 / 𝑘)) |
346 | 345 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → ((𝐴 / 𝑚) + 1) = ((𝐴 / 𝑘) + 1)) |
347 | 346 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑘) + 1))) |
348 | 344, 347 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
349 | | lgamcvg.g |
. . . . . . 7
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) |
350 | | ovex 6678 |
. . . . . . 7
⊢ ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) ∈ V |
351 | 348, 349,
350 | fvmpt 6282 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
352 | 210, 351 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝐺‘𝑘) = ((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1)))) |
353 | 352, 223,
255 | fsumser 14461 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((𝐴 · (log‘((𝑘 + 1) / 𝑘))) − (log‘((𝐴 / 𝑘) + 1))) = (seq1( + , 𝐺)‘𝑛)) |
354 | 203 | eqcomd 2628 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑛 + 1)) + 1))) = ((𝑚 ∈ ℕ ↦
((log‘(𝐴 + 1))
− (log‘((𝐴 /
(𝑚 + 1)) +
1))))‘𝑛)) |
355 | 242, 354 | oveq12d 6668 |
. . . 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))))‘𝑛))) |
356 | 343, 353,
355 | 3eqtr3d 2664 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) = ((seq1( + , (𝑚 ∈ ℕ ↦ (((𝐴 + 1) · (log‘((𝑚 + 1) / 𝑚))) − (log‘(((𝐴 + 1) / 𝑚) + 1)))))‘𝑛) − ((𝑚 ∈ ℕ ↦ ((log‘(𝐴 + 1)) −
(log‘((𝐴 / (𝑚 + 1)) + 1))))‘𝑛))) |
357 | 1, 2, 8, 10, 208, 245, 248, 356 | climsub 14364 |
. 2
⊢ (𝜑 → seq1( + , 𝐺) ⇝ (((log
Γ‘(𝐴 + 1)) +
(log‘(𝐴 + 1)))
− (log‘(𝐴 +
1)))) |
358 | | lgamcl 24767 |
. . . 4
⊢ ((𝐴 + 1) ∈ (ℂ ∖
(ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) ∈ ℂ) |
359 | 7, 358 | syl 17 |
. . 3
⊢ (𝜑 → (log Γ‘(𝐴 + 1)) ∈
ℂ) |
360 | 359, 186 | pncand 10393 |
. 2
⊢ (𝜑 → (((log
Γ‘(𝐴 + 1)) +
(log‘(𝐴 + 1)))
− (log‘(𝐴 +
1))) = (log Γ‘(𝐴 + 1))) |
361 | 357, 360 | breqtrd 4679 |
1
⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log
Γ‘(𝐴 +
1))) |