Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0...𝑁) ∈
Fin) |
2 | | rpcn 11841 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
3 | 2 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
4 | | rpdivcl 11856 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
5 | 4 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝐴 / 𝑥) ∈
ℝ+) |
6 | 5 | relogcld 24369 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℝ) |
7 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
8 | | reexpcl 12877 |
. . . . . . . . 9
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑘 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
9 | 6, 7, 8 | syl2an 494 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑘) ∈ ℝ) |
10 | 7 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
11 | | faccl 13070 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
13 | 9, 12 | nndivred 11069 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℝ) |
14 | 13 | recnd 10068 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) ∈ ℂ) |
15 | 1, 3, 14 | fsummulc2 14516 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
16 | | simplr 792 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℕ0) |
17 | | nn0uz 11722 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
18 | 16, 17 | syl6eleq 2711 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
(ℤ≥‘0)) |
19 | 3 | adantr 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → 𝑥 ∈ ℂ) |
20 | 19, 14 | mulcld 10060 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
21 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑0)) |
22 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
23 | | fac0 13063 |
. . . . . . . . 9
⊢
(!‘0) = 1 |
24 | 22, 23 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
25 | 21, 24 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 0 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑0) / 1)) |
26 | 25 | oveq2d 6666 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1))) |
27 | 18, 20, 26 | fsum1p 14482 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (0...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) |
28 | 6 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
29 | 28 | exp0d 13002 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑0) = 1) |
30 | 29 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) = (1 /
1)) |
31 | | 1div1e1 10717 |
. . . . . . . . 9
⊢ (1 / 1) =
1 |
32 | 30, 31 | syl6eq 2672 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑0) / 1) =
1) |
33 | 32 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = (𝑥 · 1)) |
34 | 3 | mulid1d 10057 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥) |
35 | 33, 34 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) = 𝑥) |
36 | | 1zzd 11408 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℤ) |
37 | | nn0z 11400 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
38 | 37 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℤ) |
39 | | 0p1e1 11132 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
40 | 39 | oveq1i 6660 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
41 | | 0z 11388 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
42 | | fzp1ss 12392 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((0 +
1)...𝑁) ⊆ (0...𝑁) |
44 | 40, 43 | eqsstr3i 3636 |
. . . . . . . . . 10
⊢
(1...𝑁) ⊆
(0...𝑁) |
45 | 44 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ (0...𝑁)) |
46 | 45, 20 | sylan2 491 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) ∈ ℂ) |
47 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
48 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (!‘𝑘) = (!‘(𝑗 + 1))) |
49 | 47, 48 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
50 | 49 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
51 | 36, 36, 38, 46, 50 | fsumshftm 14513 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
52 | 40 | sumeq1i 14428 |
. . . . . . . 8
⊢
Σ𝑘 ∈ ((0
+ 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) |
53 | 52 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑘 ∈ (1...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) |
54 | | 1m1e0 11089 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
55 | 54 | oveq1i 6660 |
. . . . . . . . 9
⊢ ((1
− 1)..^𝑁) =
(0..^𝑁) |
56 | | fzoval 12471 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
57 | 38, 56 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((1
− 1)..^𝑁) = ((1
− 1)...(𝑁 −
1))) |
58 | 55, 57 | syl5eqr 2670 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) = ((1 −
1)...(𝑁 −
1))) |
59 | 58 | sumeq1d 14431 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
60 | 51, 53, 59 | 3eqtr4d 2666 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈ ((0 +
1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) |
61 | 35, 60 | oveq12d 6668 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → ((𝑥 · (((log‘(𝐴 / 𝑥))↑0) / 1)) + Σ𝑘 ∈ ((0 + 1)...𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
62 | 15, 27, 61 | 3eqtrd 2660 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))) = (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) |
63 | 62 | mpteq2dva 4744 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)))) = (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) |
64 | 63 | oveq2d 6666 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))))) |
65 | | reelprrecn 10028 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
66 | 65 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ ∈ {ℝ, ℂ}) |
67 | | 1cnd 10056 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
68 | | recn 10026 |
. . . . 5
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
69 | 68 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
70 | | 1cnd 10056 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
71 | 66 | dvmptid 23720 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1)) |
72 | | rpssre 11843 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
73 | 72 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ⊆
ℝ) |
74 | | eqid 2622 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
75 | 74 | tgioo2 22606 |
. . . 4
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
76 | | ioorp 12251 |
. . . . . 6
⊢
(0(,)+∞) = ℝ+ |
77 | | iooretop 22569 |
. . . . . 6
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
78 | 76, 77 | eqeltrri 2698 |
. . . . 5
⊢
ℝ+ ∈ (topGen‘ran (,)) |
79 | 78 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → ℝ+ ∈ (topGen‘ran
(,))) |
80 | 66, 69, 70, 71, 73, 75, 74, 79 | dvmptres 23726 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
81 | | fzofi 12773 |
. . . . 5
⊢
(0..^𝑁) ∈
Fin |
82 | 81 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(0..^𝑁) ∈
Fin) |
83 | 3 | adantr 481 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℂ) |
84 | | elfzonn0 12512 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℕ0) |
85 | | peano2nn0 11333 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
86 | 84, 85 | syl 17 |
. . . . . . . 8
⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈
ℕ0) |
87 | | reexpcl 12877 |
. . . . . . . 8
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
(𝑗 + 1) ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
88 | 6, 86, 87 | syl2an 494 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) ∈ ℝ) |
89 | 86 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
90 | | faccl 13070 |
. . . . . . . 8
⊢ ((𝑗 + 1) ∈ ℕ0
→ (!‘(𝑗 + 1))
∈ ℕ) |
91 | 89, 90 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
92 | 88, 91 | nndivred 11069 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℝ) |
93 | 92 | recnd 10068 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
94 | 83, 93 | mulcld 10060 |
. . . 4
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
95 | 82, 94 | fsumcl 14464 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
96 | 6, 16 | reexpcld 13025 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((log‘(𝐴 / 𝑥))↑𝑁) ∈ ℝ) |
97 | | faccl 13070 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ∈
ℕ) |
98 | 97 | ad2antlr 763 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(!‘𝑁) ∈
ℕ) |
99 | 96, 98 | nndivred 11069 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℝ) |
100 | 99 | recnd 10068 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) |
101 | | ax-1cn 9994 |
. . . 4
⊢ 1 ∈
ℂ |
102 | | subcl 10280 |
. . . 4
⊢
(((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((((log‘(𝐴 /
𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
103 | 100, 101,
102 | sylancl 694 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1) ∈
ℂ) |
104 | 81 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (0..^𝑁) ∈ Fin) |
105 | 94 | an32s 846 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
106 | 105 | 3impa 1259 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) → (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) ∈ ℂ) |
107 | | reexpcl 12877 |
. . . . . . . . . . 11
⊢
(((log‘(𝐴 /
𝑥)) ∈ ℝ ∧
𝑗 ∈
ℕ0) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
108 | 6, 84, 107 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((log‘(𝐴 / 𝑥))↑𝑗) ∈ ℝ) |
109 | 84 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
110 | | faccl 13070 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ0
→ (!‘𝑗) ∈
ℕ) |
111 | 109, 110 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
112 | 108, 111 | nndivred 11069 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℝ) |
113 | 112 | recnd 10068 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
114 | 93, 113 | subcld 10392 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
115 | 114 | an32s 846 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
116 | 115 | 3impa 1259 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) ∈ ℂ) |
117 | 65 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) |
118 | 2 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
119 | | 1cnd 10056 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
120 | 80 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ 𝑥)) = (𝑥 ∈ ℝ+ ↦
1)) |
121 | 93 | an32s 846 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
122 | | negex 10279 |
. . . . . . . 8
⊢
-((((log‘(𝐴 /
𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V |
123 | 122 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ V) |
124 | | cnelprrecn 10029 |
. . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} |
125 | 124 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → ℂ ∈ {ℝ,
ℂ}) |
126 | 28 | adantlr 751 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) ∈
ℂ) |
127 | | negex 10279 |
. . . . . . . . . 10
⊢ -(1 /
𝑥) ∈
V |
128 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → -(1 /
𝑥) ∈
V) |
129 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
130 | 84 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
131 | 130, 85 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈
ℕ0) |
132 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ (𝑗 + 1) ∈
ℕ0) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
133 | 129, 131,
132 | syl2anr 495 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑(𝑗 + 1)) ∈ ℂ) |
134 | 131, 90 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℕ) |
135 | 134 | nncnd 11036 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ∈ ℂ) |
136 | 135 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ∈
ℂ) |
137 | 134 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘(𝑗 + 1)) ≠ 0) |
138 | 137 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) ≠ 0) |
139 | 133, 136,
138 | divcld 10801 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) ∈ ℂ) |
140 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝑦↑𝑗) ∈
ℂ) |
141 | 129, 130,
140 | syl2anr 495 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑗) ∈ ℂ) |
142 | 130, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℕ) |
143 | 142 | nncnd 11036 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (!‘𝑗) ∈ ℂ) |
144 | 143 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℂ) |
145 | 130 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℕ0) |
146 | 145, 110 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ∈
ℕ) |
147 | 146 | nnne0d 11065 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘𝑗) ≠ 0) |
148 | 141, 144,
147 | divcld 10801 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑦↑𝑗) / (!‘𝑗)) ∈ ℂ) |
149 | | simplll 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝐴 ∈
ℝ+) |
150 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
151 | 149, 150 | relogdivd 24372 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘(𝐴 / 𝑥)) = ((log‘𝐴) − (log‘𝑥))) |
152 | 151 | mpteq2dva 4744 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) |
153 | 152 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (ℝ D (𝑥 ∈ ℝ+
↦ ((log‘𝐴)
− (log‘𝑥))))) |
154 | | relogcl 24322 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (log‘𝐴) ∈
ℝ) |
155 | 154 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℝ) |
156 | 155 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log‘𝐴) ∈ ℂ) |
157 | 156 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝐴) ∈
ℂ) |
158 | | 0cnd 10033 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 0 ∈
ℂ) |
159 | 156 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → (log‘𝐴) ∈
ℂ) |
160 | | 0cnd 10033 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ) → 0 ∈
ℂ) |
161 | 117, 156 | dvmptc 23721 |
. . . . . . . . . . . . 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 23726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝐴))) = (𝑥 ∈ ℝ+
↦ 0)) |
165 | 150 | relogcld 24369 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
166 | 165 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
167 | 150 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
168 | | dvrelog 24383 |
. . . . . . . . . . . . 13
⊢ (ℝ
D (log ↾ ℝ+)) = (𝑥 ∈ ℝ+ ↦ (1 /
𝑥)) |
169 | | relogf1o 24313 |
. . . . . . . . . . . . . . . . 17
⊢ (log
↾ ℝ+):ℝ+–1-1-onto→ℝ |
170 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
⊢ ((log
↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾
ℝ+):ℝ+⟶ℝ) |
171 | 169, 170 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾
ℝ+):ℝ+⟶ℝ) |
172 | 171 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ ((log ↾ ℝ+)‘𝑥))) |
173 | | fvres 6207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ ((log ↾ ℝ+)‘𝑥) = (log‘𝑥)) |
174 | 173 | mpteq2ia 4740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦
(log‘𝑥)) |
175 | 172, 174 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (log ↾ ℝ+)
= (𝑥 ∈
ℝ+ ↦ (log‘𝑥))) |
176 | 175 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (log ↾
ℝ+)) = (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥)))) |
177 | 168, 176 | syl5reqr 2671 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘𝑥))) = (𝑥 ∈ ℝ+
↦ (1 / 𝑥))) |
178 | 117, 157,
158, 164, 166, 167, 177 | dvmptsub 23730 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
((log‘𝐴) −
(log‘𝑥)))) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥)))) |
179 | 153, 178 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ (0
− (1 / 𝑥)))) |
180 | | df-neg 10269 |
. . . . . . . . . . 11
⊢ -(1 /
𝑥) = (0 − (1 / 𝑥)) |
181 | 180 | mpteq2i 4741 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ -(1 / 𝑥)) = (𝑥 ∈ ℝ+
↦ (0 − (1 / 𝑥))) |
182 | 179, 181 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(log‘(𝐴 / 𝑥)))) = (𝑥 ∈ ℝ+ ↦ -(1 /
𝑥))) |
183 | | ovexd 6680 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) ∈ V) |
184 | | nn0p1nn 11332 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ) |
185 | 130, 184 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ ℕ) |
186 | | dvexp 23716 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ →
(ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
187 | 185, 186 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))))) |
188 | 125, 133,
183, 187, 135, 137 | dvmptdivc 23728 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))))) |
189 | 130 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℂ) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → 𝑗 ∈ ℂ) |
191 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
192 | 190, 101,
191 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗) |
193 | 192 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑦↑((𝑗 + 1) − 1)) = (𝑦↑𝑗)) |
194 | 193 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑦↑𝑗))) |
195 | | facp1 13065 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ (!‘(𝑗 + 1)) =
((!‘𝑗) ·
(𝑗 + 1))) |
196 | 145, 195 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((!‘𝑗) · (𝑗 + 1))) |
197 | | peano2cn 10208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℂ → (𝑗 + 1) ∈
ℂ) |
198 | 190, 197 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ∈ ℂ) |
199 | 144, 198 | mulcomd 10061 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → ((!‘𝑗) · (𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
200 | 196, 199 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (!‘(𝑗 + 1)) = ((𝑗 + 1) · (!‘𝑗))) |
201 | 194, 200 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗)))) |
202 | 185 | nnne0d 11065 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ≠ 0) |
203 | 202 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (𝑗 + 1) ≠ 0) |
204 | 141, 144,
198, 147, 203 | divcan5d 10827 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑𝑗)) / ((𝑗 + 1) · (!‘𝑗))) = ((𝑦↑𝑗) / (!‘𝑗))) |
205 | 201, 204 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑦 ∈ ℂ) → (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1))) = ((𝑦↑𝑗) / (!‘𝑗))) |
206 | 205 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑦 ∈ ℂ ↦ (((𝑗 + 1) · (𝑦↑((𝑗 + 1) − 1))) / (!‘(𝑗 + 1)))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
207 | 188, 206 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℂ D (𝑦 ∈ ℂ ↦ ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑦 ∈ ℂ ↦ ((𝑦↑𝑗) / (!‘𝑗)))) |
208 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑(𝑗 + 1)) = ((log‘(𝐴 / 𝑥))↑(𝑗 + 1))) |
209 | 208 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑(𝑗 + 1)) / (!‘(𝑗 + 1))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
210 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → (𝑦↑𝑗) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
211 | 210 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑦 = (log‘(𝐴 / 𝑥)) → ((𝑦↑𝑗) / (!‘𝑗)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
212 | 117, 125,
126, 128, 139, 148, 182, 207, 209, 211 | dvmptco 23735 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)))) |
213 | 113 | an32s 846 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) ∈ ℂ) |
214 | 167 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) |
215 | 213, 214 | mulneg2d 10484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
216 | | rpne0 11848 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
217 | 216 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
218 | 213, 118,
217 | divrecd 10804 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
219 | 218 | negeqd 10275 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · (1 / 𝑥))) |
220 | 215, 219 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥)) = -((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥)) |
221 | 220 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) · -(1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
222 | 212, 221 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))) = (𝑥 ∈ ℝ+ ↦
-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥))) |
223 | 117, 118,
119, 120, 121, 123, 222 | dvmptmul 23724 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)))) |
224 | 93 | mulid2d 10058 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) = (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) |
225 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ∈ ℝ+) |
226 | 112, 225 | rerpdivcld 11903 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℝ) |
227 | 226 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) ∈ ℂ) |
228 | 227, 83 | mulneg1d 10483 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) |
229 | 217 | an32s 846 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑥 ≠ 0) |
230 | 113, 83, 229 | divcan1d 10802 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
231 | 230 | negeqd 10275 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → -(((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
232 | 228, 231 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥) = -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
233 | 224, 232 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
234 | 93, 113 | negsubd 10398 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) + -(((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
235 | 233, 234 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ (0..^𝑁)) → ((1 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) + (-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
236 | 235 | an32s 846 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 ∈ ℝ+) → ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥)) = ((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) |
237 | 236 | mpteq2dva 4744 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑥 ∈ ℝ+ ↦ ((1
· (((log‘(𝐴 /
𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))) +
(-((((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)) / 𝑥) · 𝑥))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
238 | 223, 237 | eqtrd 2656 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑗 ∈ (0..^𝑁)) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
239 | 75, 74, 66, 79, 104, 106, 116, 238 | dvmptfsum 23738 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))))) |
240 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑗)) |
241 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (!‘𝑘) = (!‘𝑗)) |
242 | 240, 241 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) |
243 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ((log‘(𝐴 / 𝑥))↑𝑘) = ((log‘(𝐴 / 𝑥))↑𝑁)) |
244 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (!‘𝑘) = (!‘𝑁)) |
245 | 243, 244 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
246 | 242, 49, 25, 245, 18, 14 | telfsumo2 14535 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1))) |
247 | 32 | oveq2d 6666 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − (((log‘(𝐴 / 𝑥))↑0) / 1)) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
248 | 246, 247 | eqtrd 2656 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) →
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗))) = ((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) |
249 | 248 | mpteq2dva 4744 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)((((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))) − (((log‘(𝐴 / 𝑥))↑𝑗) / (!‘𝑗)))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
250 | 239, 249 | eqtrd 2656 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦
Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1)))))) = (𝑥 ∈ ℝ+ ↦
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) |
251 | 66, 3, 67, 80, 95, 103, 250 | dvmptadd 23723 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 + Σ𝑗 ∈ (0..^𝑁)(𝑥 · (((log‘(𝐴 / 𝑥))↑(𝑗 + 1)) / (!‘(𝑗 + 1))))))) = (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)))) |
252 | | pncan3 10289 |
. . . 4
⊢ ((1
∈ ℂ ∧ (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) ∈ ℂ) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
253 | 101, 100,
252 | sylancr 695 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) ∧ 𝑥 ∈ ℝ+) → (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1)) = (((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁))) |
254 | 253 | mpteq2dva 4744 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (𝑥 ∈ ℝ+ ↦ (1 +
((((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)) − 1))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |
255 | 64, 251, 254 | 3eqtrd 2660 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝑁 ∈
ℕ0) → (ℝ D (𝑥 ∈ ℝ+ ↦ (𝑥 · Σ𝑘 ∈ (0...𝑁)(((log‘(𝐴 / 𝑥))↑𝑘) / (!‘𝑘))))) = (𝑥 ∈ ℝ+ ↦
(((log‘(𝐴 / 𝑥))↑𝑁) / (!‘𝑁)))) |