Step | Hyp | Ref
| Expression |
1 | | fzfid 12966 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0...𝑁) ∈
Fin) |
2 | | rpcn 12034 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
3 | 2 | adantl 473 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
4 | | rpdivcl 12049 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
5 | 4 | adantlr 753 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
6 | 5 | relogcld 24568 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℝ) |
7 | | elfznn0 12626 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
8 | | reexpcl 13071 |
. . . . . . . . 9
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
9 | 6, 7, 8 | syl2an 495 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
10 | 7 | adantl 473 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
11 | | faccl 13264 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
13 | 9, 12 | nndivred 11261 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
14 | 13 | recnd 10260 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ) |
15 | 1, 3, 14 | fsummulc2 14715 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
16 | | simplr 809 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℕ0) |
17 | | nn0uz 11915 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | syl6eleq 2849 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘0)) |
19 | 3 | adantr 472 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ) |
20 | 19, 14 | mulcld 10252 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
21 | | oveq2 6821 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0)) |
22 | | fveq2 6352 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
23 | | fac0 13257 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
24 | 22, 23 | syl6eq 2810 |
. . . . . . . 8
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
25 | 21, 24 | oveq12d 6831 |
. . . . . . 7
⊢ (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1)) |
26 | 25 | oveq2d 6829 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1))) |
27 | 18, 20, 26 | fsum1p 14681 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) |
28 | 6 | recnd 10260 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
29 | 28 | exp0d 13196 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑0) = 1) |
30 | 29 | oveq1d 6828 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) = (1 /
1)) |
31 | | 1div1e1 10909 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
32 | 30, 31 | syl6eq 2810 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) =
1) |
33 | 32 | oveq2d 6829 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1)) |
34 | 3 | mulid1d 10249 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥) |
35 | 33, 34 | eqtrd 2794 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥) |
36 | | 1zzd 11600 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℤ) |
37 | | nn0z 11592 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
38 | 37 | ad2antlr 765 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
39 | | fz1ssfz0 12629 |
. . . . . . . . . 10
⊢
(1...𝑁) ⊆
(0...𝑁) |
40 | 39 | sseli 3740 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁)) |
41 | 40, 20 | sylan2 492 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
42 | | oveq2 6821 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
43 | | fveq2 6352 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1))) |
44 | 42, 43 | oveq12d 6831 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
45 | 44 | oveq2d 6829 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
46 | 36, 36, 38, 41, 45 | fsumshftm 14712 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
47 | | 0p1e1 11324 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
48 | 47 | oveq1i 6823 |
. . . . . . . . 9
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
49 | 48 | sumeq1i 14627 |
. . . . . . . 8
⊢
Σ𝑘 ∈ ((0
+ 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
51 | | 1m1e0 11281 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
52 | 51 | oveq1i 6823 |
. . . . . . . . 9
⊢ ((1
− 1)..^𝑁) =
(0..^𝑁) |
53 | | fzoval 12665 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
54 | 38, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
55 | 52, 54 | syl5eqr 2808 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) = ((1 −
1)...(𝑁 −
1))) |
56 | 55 | sumeq1d 14630 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
57 | 46, 50, 56 | 3eqtr4d 2804 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
58 | 35, 57 | oveq12d 6831 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
59 | 15, 27, 58 | 3eqtrd 2798 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
60 | 59 | mpteq2dva 4896 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) |
61 | 60 | oveq2d 6829 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))) |
62 | | reelprrecn 10220 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
63 | 62 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ ∈ {ℝ, ℂ}) |
64 | | 1cnd 10248 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
65 | | recn 10218 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
66 | 65 | adantl 473 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
67 | | 1cnd 10248 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
68 | 63 | dvmptid 23919 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
69 | | rpssre 12036 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
70 | 69 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ⊆
ℝ) |
71 | | eqid 2760 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
72 | 71 | tgioo2 22807 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
73 | | ioorp 12444 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
74 | | iooretop 22770 |
. . . . . 6
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
75 | 73, 74 | eqeltrri 2836 |
. . . . 5
⊢
ℝ+ ∈ (topGen‘ran (,)) |
76 | 75 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ∈ (topGen‘ran
(,))) |
77 | 63, 66, 67, 68, 70, 72, 71, 76 | dvmptres 23925 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
78 | | fzofi 12967 |
. . . . 5
⊢
(0..^𝑁) ∈
Fin |
79 | 78 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) ∈
Fin) |
80 | 3 | adantr 472 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ) |
81 | | elfzonn0 12707 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0) |
82 | | peano2nn0 11525 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈
ℕ0) |
84 | | reexpcl 13071 |
. . . . . . . 8
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
(𝑗 + 1) ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
85 | 6, 83, 84 | syl2an 495 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
86 | 83 | adantl 473 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
87 | | faccl 13264 |
. . . . . . . 8
⊢ ((𝑗 + 1) ∈ ℕ0
→ (!‘(𝑗 + 1))
∈ ℕ) |
88 | 86, 87 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
89 | 85, 88 | nndivred 11261 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ) |
90 | 89 | recnd 10260 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
91 | 80, 90 | mulcld 10252 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
92 | 79, 91 | fsumcl 14663 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
93 | 6, 16 | reexpcld 13219 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ) |
94 | | faccl 13264 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
95 | 94 | ad2antlr 765 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) |
96 | 93, 95 | nndivred 11261 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ) |
97 | 96 | recnd 10260 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) |
98 | | ax-1cn 10186 |
. . . 4
⊢ 1 ∈
ℂ |
99 | | subcl 10472 |
. . . 4
⊢
(((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
100 | 97, 98, 99 | sylancl 697 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
101 | 78 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (0..^𝑁) ∈ Fin) |
102 | 91 | an32s 881 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
103 | 102 | 3impa 1101 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
104 | | reexpcl 13071 |
. . . . . . . . . . 11
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑗 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
105 | 6, 81, 104 | syl2an 495 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
106 | 81 | adantl 473 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
107 | | faccl 13264 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
→ (!‘𝑗) ∈
ℕ) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
109 | 105, 108 | nndivred 11261 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ) |
110 | 109 | recnd 10260 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
111 | 90, 110 | subcld 10584 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
112 | 111 | an32s 881 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
113 | 112 | 3impa 1101 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
114 | 62 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
115 | 2 | adantl 473 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
116 | | 1cnd 10248 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
117 | 77 | adantr 472 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
118 | 90 | an32s 881 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
119 | | negex 10471 |
. . . . . . . 8
⊢
-((((log‘(𝐴 /
𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V) |
121 | | cnelprrecn 10221 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
122 | 121 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ,
ℂ}) |
123 | 28 | adantlr 753 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
124 | | negex 10471 |
. . . . . . . . . 10
⊢ -(1 /
𝑥) ∈
V |
125 | 124 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -(1 /
𝑥) ∈
V) |
126 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
127 | 81 | adantl 473 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
128 | 127, 82 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
129 | | expcl 13072 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈
ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
130 | 126, 128,
129 | syl2anr 496 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
131 | 128, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
132 | 131 | nncnd 11228 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ) |
133 | 132 | adantr 472 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈
ℂ) |
134 | 131 | nnne0d 11257 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0) |
135 | 134 | adantr 472 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0) |
136 | 130, 133,
135 | divcld 10993 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
137 | | expcl 13072 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝑦↑𝑗) ∈
ℂ) |
138 | 126, 127,
137 | syl2anr 496 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑗) ∈ ℂ) |
139 | 127, 107 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
140 | 139 | nncnd 11228 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ) |
141 | 140 | adantr 472 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℂ) |
142 | 127 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0) |
143 | 142, 107 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℕ) |
144 | 143 | nnne0d 11257 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0) |
145 | 138, 141,
144 | divcld 10993 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑𝑗) / (!‘𝑗)) ∈ ℂ) |
146 | | simplll 815 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈
ℝ+) |
147 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
148 | 146, 147 | relogdivd 24571 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥))) |
149 | 148 | mpteq2dva 4896 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) |
150 | 149 | oveq2d 6829 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝐴)
− (log‘𝑥))))) |
151 | | relogcl 24521 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
152 | 151 | ad2antrr 764 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ) |
153 | 152 | recnd 10260 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ) |
154 | 153 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝐴) ∈
ℂ) |
155 | | 0cnd 10225 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈
ℂ) |
156 | 153 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈
ℂ) |
157 | | 0cnd 10225 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℂ) |
158 | 114, 153 | dvmptc 23920 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ ↦ (log‘𝐴))) = (𝑥 ∈ ℝ ↦ 0)) |
159 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ⊆
ℝ) |
160 | 75 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ+ ∈
(topGen‘ran (,))) |
161 | 114, 156,
157, 158, 159, 72, 71, 160 | dvmptres 23925 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝐴))) = (𝑥 ∈ ℝ+
↦ 0)) |
162 | 147 | relogcld 24568 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
163 | 162 | recnd 10260 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
164 | 147 | rpreccld 12075 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
165 | | dvrelog 24582 |
. . . . . . . . . . . . 13
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
166 | | relogf1o 24512 |
. . . . . . . . . . . . . . . . 17
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
167 | | f1of 6298 |
. . . . . . . . . . . . . . . . 17
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
168 | 166, 167 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾
ℝ+):ℝ+⟶ℝ) |
169 | 168 | feqmptd 6411 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ ((log ↾ ℝ+)‘𝑥))) |
170 | | fvres 6368 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
171 | 170 | mpteq2ia 4892 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
172 | 169, 171 | syl6eq 2810 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) |
173 | 172 | oveq2d 6829 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾
ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
174 | 165, 173 | syl5reqr 2809 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) = (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) |
175 | 114, 154,
155, 161, 163, 164, 174 | dvmptsub 23929 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥)))) |
176 | 150, 175 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0
− (1 / 𝑥)))) |
177 | | df-neg 10461 |
. . . . . . . . . . 11
⊢ -(1 /
𝑥) = (0 − (1 / 𝑥)) |
178 | 177 | mpteq2i 4893 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥))) |
179 | 176, 178 | syl6eqr 2812 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
180 | | ovexd 6843 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V) |
181 | | nn0p1nn 11524 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
182 | 127, 181 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ) |
183 | | dvexp 23915 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
185 | 122, 130,
180, 184, 132, 134 | dvmptdivc 23927 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))))) |
186 | 127 | nn0cnd 11545 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ) |
187 | 186 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ) |
188 | | pncan 10479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
189 | 187, 98, 188 | sylancl 697 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗) |
190 | 189 | oveq2d 6829 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦↑𝑗)) |
191 | 190 | oveq2d 6829 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦↑𝑗))) |
192 | | facp1 13259 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ (!‘(𝑗 + 1)) =
((!‘𝑗) ·
(𝑗 + 1))) |
193 | 142, 192 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1))) |
194 | | peano2cn 10400 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
195 | 187, 194 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ) |
196 | 141, 195 | mulcomd 10253 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
197 | 193, 196 | eqtrd 2794 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
198 | 191, 197 | oveq12d 6831 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗)))) |
199 | 182 | nnne0d 11257 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0) |
200 | 199 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0) |
201 | 138, 141,
195, 144, 200 | divcan5d 11019 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦↑𝑗) / (!‘𝑗))) |
202 | 198, 201 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦↑𝑗) / (!‘𝑗))) |
203 | 202 | mpteq2dva 4896 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
204 | 185, 203 | eqtrd 2794 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
205 | | oveq1 6820 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
206 | 205 | oveq1d 6828 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
207 | | oveq1 6820 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
208 | 207 | oveq1d 6828 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
209 | 114, 122,
123, 125, 136, 145, 179, 204, 206, 208 | dvmptco 23934 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)))) |
210 | 110 | an32s 881 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
211 | 164 | rpcnd 12067 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) |
212 | 210, 211 | mulneg2d 10676 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
213 | | rpne0 12041 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
214 | 213 | adantl 473 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
215 | 210, 115,
214 | divrecd 10996 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
216 | 215 | negeqd 10467 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
217 | 212, 216 | eqtr4d 2797 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)) |
218 | 217 | mpteq2dva 4896 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
219 | 209, 218 | eqtrd 2794 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
220 | 114, 115,
116, 117, 118, 120, 219 | dvmptmul 23923 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)))) |
221 | 90 | mulid2d 10250 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
222 | | simplr 809 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+) |
223 | 109, 222 | rerpdivcld 12096 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ) |
224 | 223 | recnd 10260 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ) |
225 | 224, 80 | mulneg1d 10675 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) |
226 | 214 | an32s 881 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0) |
227 | 110, 80, 226 | divcan1d 10994 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
228 | 227 | negeqd 10467 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
229 | 225, 228 | eqtrd 2794 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
230 | 221, 229 | oveq12d 6831 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
231 | 90, 110 | negsubd 10590 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
232 | 230, 231 | eqtrd 2794 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
233 | 232 | an32s 881 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
234 | 233 | mpteq2dva 4896 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
235 | 220, 234 | eqtrd 2794 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
236 | 72, 71, 63, 76, 101, 103, 113, 235 | dvmptfsum 23937 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
237 | | oveq2 6821 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
238 | | fveq2 6352 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗)) |
239 | 237, 238 | oveq12d 6831 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
240 | | oveq2 6821 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁)) |
241 | | fveq2 6352 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁)) |
242 | 240, 241 | oveq12d 6831 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
243 | 239, 44, 25, 242, 18, 14 | telfsumo2 14734 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1))) |
244 | 32 | oveq2d 6829 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
245 | 243, 244 | eqtrd 2794 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
246 | 245 | mpteq2dva 4896 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
247 | 236, 246 | eqtrd 2794 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
248 | 63, 3, 64, 77, 92, 100, 247 | dvmptadd 23922 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))) |
249 | | pncan3 10481 |
. . . 4
⊢ ((1
∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
250 | 98, 97, 249 | sylancr 698 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
251 | 250 | mpteq2dva 4896 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |
252 | 61, 248, 251 | 3eqtrd 2798 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |