Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0...𝑁) ∈
Fin) |
2 | | rpcn 11717 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
3 | 2 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
4 | | rpdivcl 11732 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
5 | 4 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
6 | 5 | relogcld 24173 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℝ) |
7 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
8 | | reexpcl 12739 |
. . . . . . . . 9
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
9 | 6, 7, 8 | syl2an 493 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
10 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
11 | | faccl 12932 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
13 | 9, 12 | nndivred 10946 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
14 | 13 | recnd 9947 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ) |
15 | 1, 3, 14 | fsummulc2 14358 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
16 | | simplr 788 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℕ0) |
17 | | nn0uz 11598 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | syl6eleq 2698 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘0)) |
19 | 3 | adantr 480 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ) |
20 | 19, 14 | mulcld 9939 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
21 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0)) |
22 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
23 | | fac0 12925 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
24 | 22, 23 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
25 | 21, 24 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1)) |
26 | 25 | oveq2d 6565 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1))) |
27 | 18, 20, 26 | fsum1p 14326 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) |
28 | 6 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
29 | 28 | exp0d 12864 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑0) = 1) |
30 | 29 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) = (1 /
1)) |
31 | | 1div1e1 10596 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
32 | 30, 31 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) =
1) |
33 | 32 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1)) |
34 | 3 | mulid1d 9936 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥) |
35 | 33, 34 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥) |
36 | | 1zzd 11285 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℤ) |
37 | | nn0z 11277 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
38 | 37 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
39 | | 0p1e1 11009 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
40 | 39 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
41 | | 0z 11265 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
42 | | fzp1ss 12262 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) ⊆ (0...𝑁) |
44 | 40, 43 | eqsstr3i 3599 |
. . . . . . . . . 10
⊢
(1...𝑁) ⊆
(0...𝑁) |
45 | 44 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁)) |
46 | 45, 20 | sylan2 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
47 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
48 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1))) |
49 | 47, 48 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
50 | 49 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
51 | 36, 36, 38, 46, 50 | fsumshftm 14355 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
52 | 40 | sumeq1i 14276 |
. . . . . . . 8
⊢
Σ𝑘 ∈ ((0
+ 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) |
53 | 52 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
54 | | 1m1e0 10966 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
55 | 54 | oveq1i 6559 |
. . . . . . . . 9
⊢ ((1
− 1)..^𝑁) =
(0..^𝑁) |
56 | | fzoval 12340 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
57 | 38, 56 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
58 | 55, 57 | syl5eqr 2658 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) = ((1 −
1)...(𝑁 −
1))) |
59 | 58 | sumeq1d 14279 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
60 | 51, 53, 59 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
61 | 35, 60 | oveq12d 6567 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
62 | 15, 27, 61 | 3eqtrd 2648 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
63 | 62 | mpteq2dva 4672 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) |
64 | 63 | oveq2d 6565 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))) |
65 | | reelprrecn 9907 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
66 | 65 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ ∈ {ℝ, ℂ}) |
67 | | 1cnd 9935 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
68 | | recn 9905 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
69 | 68 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
70 | | 1cnd 9935 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
71 | 66 | dvmptid 23526 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
72 | | rpssre 11719 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
73 | 72 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ⊆
ℝ) |
74 | | eqid 2610 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
75 | 74 | tgioo2 22414 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
76 | | ioorp 12122 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
77 | | iooretop 22379 |
. . . . . 6
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
78 | 76, 77 | eqeltrri 2685 |
. . . . 5
⊢
ℝ+ ∈ (topGen‘ran (,)) |
79 | 78 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ∈ (topGen‘ran
(,))) |
80 | 66, 69, 70, 71, 73, 75, 74, 79 | dvmptres 23532 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
81 | | fzofi 12635 |
. . . . 5
⊢
(0..^𝑁) ∈
Fin |
82 | 81 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) ∈
Fin) |
83 | 3 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ) |
84 | | elfzonn0 12380 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0) |
85 | | peano2nn0 11210 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
86 | 84, 85 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈
ℕ0) |
87 | | reexpcl 12739 |
. . . . . . . 8
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
(𝑗 + 1) ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
88 | 6, 86, 87 | syl2an 493 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
89 | 86 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
90 | | faccl 12932 |
. . . . . . . 8
⊢ ((𝑗 + 1) ∈ ℕ0
→ (!‘(𝑗 + 1))
∈ ℕ) |
91 | 89, 90 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
92 | 88, 91 | nndivred 10946 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ) |
93 | 92 | recnd 9947 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
94 | 83, 93 | mulcld 9939 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
95 | 82, 94 | fsumcl 14311 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
96 | 6, 16 | reexpcld 12887 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ) |
97 | | faccl 12932 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
98 | 97 | ad2antlr 759 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) |
99 | 96, 98 | nndivred 10946 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ) |
100 | 99 | recnd 9947 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) |
101 | | ax-1cn 9873 |
. . . 4
⊢ 1 ∈
ℂ |
102 | | subcl 10159 |
. . . 4
⊢
(((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
103 | 100, 101,
102 | sylancl 693 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
104 | 81 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (0..^𝑁) ∈ Fin) |
105 | 94 | an32s 842 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
106 | 105 | 3impa 1251 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
107 | | reexpcl 12739 |
. . . . . . . . . . 11
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑗 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
108 | 6, 84, 107 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
109 | 84 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
110 | | faccl 12932 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
→ (!‘𝑗) ∈
ℕ) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
112 | 108, 111 | nndivred 10946 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ) |
113 | 112 | recnd 9947 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
114 | 93, 113 | subcld 10271 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
115 | 114 | an32s 842 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
116 | 115 | 3impa 1251 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
117 | 65 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
118 | 2 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
119 | | 1cnd 9935 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
120 | 80 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
121 | 93 | an32s 842 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
122 | | negex 10158 |
. . . . . . . 8
⊢
-((((log‘(𝐴 /
𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V |
123 | 122 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V) |
124 | | cnelprrecn 9908 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
125 | 124 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ,
ℂ}) |
126 | 28 | adantlr 747 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
127 | | negex 10158 |
. . . . . . . . . 10
⊢ -(1 /
𝑥) ∈
V |
128 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -(1 /
𝑥) ∈
V) |
129 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
130 | 84 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
131 | 130, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
132 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈
ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
133 | 129, 131,
132 | syl2anr 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
134 | 131, 90 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
135 | 134 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ) |
136 | 135 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈
ℂ) |
137 | 134 | nnne0d 10942 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0) |
138 | 137 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0) |
139 | 133, 136,
138 | divcld 10680 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
140 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝑦↑𝑗) ∈
ℂ) |
141 | 129, 130,
140 | syl2anr 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑗) ∈ ℂ) |
142 | 130, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
143 | 142 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ) |
144 | 143 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℂ) |
145 | 130 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0) |
146 | 145, 110 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℕ) |
147 | 146 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0) |
148 | 141, 144,
147 | divcld 10680 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑𝑗) / (!‘𝑗)) ∈ ℂ) |
149 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈
ℝ+) |
150 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
151 | 149, 150 | relogdivd 24176 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥))) |
152 | 151 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝐴)
− (log‘𝑥))))) |
154 | | relogcl 24126 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
155 | 154 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ) |
156 | 155 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ) |
157 | 156 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝐴) ∈
ℂ) |
158 | | 0cnd 9912 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈
ℂ) |
159 | 156 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈
ℂ) |
160 | | 0cnd 9912 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℂ) |
161 | 117, 156 | dvmptc 23527 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ ↦ 0)) |
162 | 72 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ⊆
ℝ) |
163 | 78 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ∈
(topGen‘ran (,))) |
164 | 117, 159,
160, 161, 162, 75, 74, 163 | dvmptres 23532 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝐴))) = (𝑥 ∈ ℝ+
↦ 0)) |
165 | 150 | relogcld 24173 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
166 | 165 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
167 | 150 | rpreccld 11758 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
168 | | dvrelog 24183 |
. . . . . . . . . . . . 13
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
169 | | relogf1o 24117 |
. . . . . . . . . . . . . . . . 17
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
170 | | f1of 6050 |
. . . . . . . . . . . . . . . . 17
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
171 | 169, 170 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾
ℝ+):ℝ+⟶ℝ) |
172 | 171 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ ((log ↾ ℝ+)‘𝑥))) |
173 | | fvres 6117 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
174 | 173 | mpteq2ia 4668 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
175 | 172, 174 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) |
176 | 175 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾
ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
177 | 168, 176 | syl5reqr 2659 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) = (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) |
178 | 117, 157,
158, 164, 166, 167, 177 | dvmptsub 23536 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥)))) |
179 | 153, 178 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0
− (1 / 𝑥)))) |
180 | | df-neg 10148 |
. . . . . . . . . . 11
⊢ -(1 /
𝑥) = (0 − (1 / 𝑥)) |
181 | 180 | mpteq2i 4669 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥))) |
182 | 179, 181 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
183 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V |
184 | 183 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V) |
185 | | nn0p1nn 11209 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
186 | 130, 185 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ) |
187 | | dvexp 23522 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
188 | 186, 187 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
189 | 125, 133,
184, 188, 135, 137 | dvmptdivc 23534 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))))) |
190 | 130 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ) |
191 | 190 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ) |
192 | | pncan 10166 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
193 | 191, 101,
192 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗) |
194 | 193 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦↑𝑗)) |
195 | 194 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦↑𝑗))) |
196 | | facp1 12927 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ (!‘(𝑗 + 1)) =
((!‘𝑗) ·
(𝑗 + 1))) |
197 | 145, 196 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1))) |
198 | | peano2cn 10087 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
199 | 191, 198 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ) |
200 | 144, 199 | mulcomd 9940 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
201 | 197, 200 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
202 | 195, 201 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗)))) |
203 | 186 | nnne0d 10942 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0) |
204 | 203 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0) |
205 | 141, 144,
199, 147, 204 | divcan5d 10706 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦↑𝑗) / (!‘𝑗))) |
206 | 202, 205 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦↑𝑗) / (!‘𝑗))) |
207 | 206 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
208 | 189, 207 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
209 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
210 | 209 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
211 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
212 | 211 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
213 | 117, 125,
126, 128, 139, 148, 182, 208, 210, 212 | dvmptco 23541 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)))) |
214 | 113 | an32s 842 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
215 | 167 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) |
216 | 214, 215 | mulneg2d 10363 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
217 | | rpne0 11724 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
218 | 217 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
219 | 214, 118,
218 | divrecd 10683 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
220 | 219 | negeqd 10154 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
221 | 216, 220 | eqtr4d 2647 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)) |
222 | 221 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
223 | 213, 222 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
224 | 117, 118,
119, 120, 121, 123, 223 | dvmptmul 23530 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)))) |
225 | 93 | mulid2d 9937 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
226 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+) |
227 | 112, 226 | rerpdivcld 11779 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ) |
228 | 227 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ) |
229 | 228, 83 | mulneg1d 10362 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) |
230 | 218 | an32s 842 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0) |
231 | 113, 83, 230 | divcan1d 10681 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
232 | 231 | negeqd 10154 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
233 | 229, 232 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
234 | 225, 233 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
235 | 93, 113 | negsubd 10277 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
236 | 234, 235 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
237 | 236 | an32s 842 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
238 | 237 | mpteq2dva 4672 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
239 | 224, 238 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
240 | 75, 74, 66, 79, 104, 106, 116, 239 | dvmptfsum 23542 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
241 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
242 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗)) |
243 | 241, 242 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
244 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁)) |
245 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁)) |
246 | 244, 245 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
247 | 243, 49, 25, 246, 18, 14 | telfsumo2 14376 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1))) |
248 | 32 | oveq2d 6565 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
249 | 247, 248 | eqtrd 2644 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
250 | 249 | mpteq2dva 4672 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
251 | 240, 250 | eqtrd 2644 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
252 | 66, 3, 67, 80, 95, 103, 251 | dvmptadd 23529 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))) |
253 | | pncan3 10168 |
. . . 4
⊢ ((1
∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
254 | 101, 100,
253 | sylancr 694 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
255 | 254 | mpteq2dva 4672 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |
256 | 64, 252, 255 | 3eqtrd 2648 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |