Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 11014 |
. . . 4
β’ β
β {β, β} |
2 | 1 | a1i 11 |
. . 3
β’ (π΄ β β β β
β {β, β}) |
3 | | dvcncxp1.d |
. . . . . . 7
β’ π· = (β β
(-β(,]0)) |
4 | | difss 4072 |
. . . . . . 7
β’ (β
β (-β(,]0)) β β |
5 | 3, 4 | eqsstri 3960 |
. . . . . 6
β’ π· β
β |
6 | 5 | sseli 3922 |
. . . . 5
β’ (π₯ β π· β π₯ β β) |
7 | 3 | logdmn0 25844 |
. . . . 5
β’ (π₯ β π· β π₯ β 0) |
8 | 6, 7 | logcld 25775 |
. . . 4
β’ (π₯ β π· β (logβπ₯) β β) |
9 | 8 | adantl 483 |
. . 3
β’ ((π΄ β β β§ π₯ β π·) β (logβπ₯) β β) |
10 | 6, 7 | reccld 11794 |
. . . 4
β’ (π₯ β π· β (1 / π₯) β β) |
11 | 10 | adantl 483 |
. . 3
β’ ((π΄ β β β§ π₯ β π·) β (1 / π₯) β β) |
12 | | mulcl 11005 |
. . . 4
β’ ((π΄ β β β§ π¦ β β) β (π΄ Β· π¦) β β) |
13 | | efcl 15841 |
. . . 4
β’ ((π΄ Β· π¦) β β β (expβ(π΄ Β· π¦)) β β) |
14 | 12, 13 | syl 17 |
. . 3
β’ ((π΄ β β β§ π¦ β β) β
(expβ(π΄ Β·
π¦)) β
β) |
15 | | ovexd 7342 |
. . 3
β’ ((π΄ β β β§ π¦ β β) β
((expβ(π΄ Β·
π¦)) Β· π΄) β V) |
16 | 3 | logcn 25851 |
. . . . . . . 8
β’ (log
βΎ π·) β (π·βcnββ) |
17 | | cncff 24105 |
. . . . . . . 8
β’ ((log
βΎ π·) β (π·βcnββ) β (log βΎ π·):π·βΆβ) |
18 | 16, 17 | mp1i 13 |
. . . . . . 7
β’ (π΄ β β β (log
βΎ π·):π·βΆβ) |
19 | 18 | feqmptd 6869 |
. . . . . 6
β’ (π΄ β β β (log
βΎ π·) = (π₯ β π· β¦ ((log βΎ π·)βπ₯))) |
20 | | fvres 6823 |
. . . . . . 7
β’ (π₯ β π· β ((log βΎ π·)βπ₯) = (logβπ₯)) |
21 | 20 | mpteq2ia 5184 |
. . . . . 6
β’ (π₯ β π· β¦ ((log βΎ π·)βπ₯)) = (π₯ β π· β¦ (logβπ₯)) |
22 | 19, 21 | eqtrdi 2792 |
. . . . 5
β’ (π΄ β β β (log
βΎ π·) = (π₯ β π· β¦ (logβπ₯))) |
23 | 22 | oveq2d 7323 |
. . . 4
β’ (π΄ β β β (β
D (log βΎ π·)) =
(β D (π₯ β π· β¦ (logβπ₯)))) |
24 | 3 | dvlog 25855 |
. . . 4
β’ (β
D (log βΎ π·)) = (π₯ β π· β¦ (1 / π₯)) |
25 | 23, 24 | eqtr3di 2791 |
. . 3
β’ (π΄ β β β (β
D (π₯ β π· β¦ (logβπ₯))) = (π₯ β π· β¦ (1 / π₯))) |
26 | | simpl 484 |
. . . 4
β’ ((π΄ β β β§ π¦ β β) β π΄ β
β) |
27 | | efcl 15841 |
. . . . 5
β’ (π₯ β β β
(expβπ₯) β
β) |
28 | 27 | adantl 483 |
. . . 4
β’ ((π΄ β β β§ π₯ β β) β
(expβπ₯) β
β) |
29 | | simpr 486 |
. . . . . 6
β’ ((π΄ β β β§ π¦ β β) β π¦ β
β) |
30 | | 1cnd 11020 |
. . . . . 6
β’ ((π΄ β β β§ π¦ β β) β 1 β
β) |
31 | 2 | dvmptid 25170 |
. . . . . 6
β’ (π΄ β β β (β
D (π¦ β β β¦
π¦)) = (π¦ β β β¦ 1)) |
32 | | id 22 |
. . . . . 6
β’ (π΄ β β β π΄ β
β) |
33 | 2, 29, 30, 31, 32 | dvmptcmul 25177 |
. . . . 5
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ (π΄ Β· 1))) |
34 | | mulid1 11023 |
. . . . . 6
β’ (π΄ β β β (π΄ Β· 1) = π΄) |
35 | 34 | mpteq2dv 5183 |
. . . . 5
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· 1)) = (π¦ β β β¦ π΄)) |
36 | 33, 35 | eqtrd 2776 |
. . . 4
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ π΄)) |
37 | | dvef 25193 |
. . . . 5
β’ (β
D exp) = exp |
38 | | eff 15840 |
. . . . . . . 8
β’
exp:ββΆβ |
39 | 38 | a1i 11 |
. . . . . . 7
β’ (π΄ β β β
exp:ββΆβ) |
40 | 39 | feqmptd 6869 |
. . . . . 6
β’ (π΄ β β β exp =
(π₯ β β β¦
(expβπ₯))) |
41 | 40 | oveq2d 7323 |
. . . . 5
β’ (π΄ β β β (β
D exp) = (β D (π₯
β β β¦ (expβπ₯)))) |
42 | 37, 41, 40 | 3eqtr3a 2800 |
. . . 4
β’ (π΄ β β β (β
D (π₯ β β β¦
(expβπ₯))) = (π₯ β β β¦
(expβπ₯))) |
43 | | fveq2 6804 |
. . . 4
β’ (π₯ = (π΄ Β· π¦) β (expβπ₯) = (expβ(π΄ Β· π¦))) |
44 | 2, 2, 12, 26, 28, 28, 36, 42, 43, 43 | dvmptco 25185 |
. . 3
β’ (π΄ β β β (β
D (π¦ β β β¦
(expβ(π΄ Β·
π¦)))) = (π¦ β β β¦ ((expβ(π΄ Β· π¦)) Β· π΄))) |
45 | | oveq2 7315 |
. . . 4
β’ (π¦ = (logβπ₯) β (π΄ Β· π¦) = (π΄ Β· (logβπ₯))) |
46 | 45 | fveq2d 6808 |
. . 3
β’ (π¦ = (logβπ₯) β (expβ(π΄ Β· π¦)) = (expβ(π΄ Β· (logβπ₯)))) |
47 | 46 | oveq1d 7322 |
. . 3
β’ (π¦ = (logβπ₯) β ((expβ(π΄ Β· π¦)) Β· π΄) = ((expβ(π΄ Β· (logβπ₯))) Β· π΄)) |
48 | 2, 2, 9, 11, 14, 15, 25, 44, 46, 47 | dvmptco 25185 |
. 2
β’ (π΄ β β β (β
D (π₯ β π· β¦ (expβ(π΄ Β· (logβπ₯))))) = (π₯ β π· β¦ (((expβ(π΄ Β· (logβπ₯))) Β· π΄) Β· (1 / π₯)))) |
49 | 6 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β π₯ β β) |
50 | 7 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β π₯ β 0) |
51 | | simpl 484 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β π΄ β β) |
52 | 49, 50, 51 | cxpefd 25916 |
. . . 4
β’ ((π΄ β β β§ π₯ β π·) β (π₯βππ΄) = (expβ(π΄ Β· (logβπ₯)))) |
53 | 52 | mpteq2dva 5181 |
. . 3
β’ (π΄ β β β (π₯ β π· β¦ (π₯βππ΄)) = (π₯ β π· β¦ (expβ(π΄ Β· (logβπ₯))))) |
54 | 53 | oveq2d 7323 |
. 2
β’ (π΄ β β β (β
D (π₯ β π· β¦ (π₯βππ΄))) = (β D (π₯ β π· β¦ (expβ(π΄ Β· (logβπ₯)))))) |
55 | | 1cnd 11020 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β π·) β 1 β β) |
56 | 49, 50, 51, 55 | cxpsubd 25922 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β π·) β (π₯βπ(π΄ β 1)) = ((π₯βππ΄) / (π₯βπ1))) |
57 | 49 | cxp1d 25910 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β π·) β (π₯βπ1) = π₯) |
58 | 57 | oveq2d 7323 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β π·) β ((π₯βππ΄) / (π₯βπ1)) = ((π₯βππ΄) / π₯)) |
59 | 49, 51 | cxpcld 25912 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β π·) β (π₯βππ΄) β β) |
60 | 59, 49, 50 | divrecd 11804 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β π·) β ((π₯βππ΄) / π₯) = ((π₯βππ΄) Β· (1 / π₯))) |
61 | 56, 58, 60 | 3eqtrd 2780 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β (π₯βπ(π΄ β 1)) = ((π₯βππ΄) Β· (1 / π₯))) |
62 | 61 | oveq2d 7323 |
. . . 4
β’ ((π΄ β β β§ π₯ β π·) β (π΄ Β· (π₯βπ(π΄ β 1))) = (π΄ Β· ((π₯βππ΄) Β· (1 / π₯)))) |
63 | 51, 59, 11 | mul12d 11234 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β (π΄ Β· ((π₯βππ΄) Β· (1 / π₯))) = ((π₯βππ΄) Β· (π΄ Β· (1 / π₯)))) |
64 | 59, 51, 11 | mulassd 11048 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β (((π₯βππ΄) Β· π΄) Β· (1 / π₯)) = ((π₯βππ΄) Β· (π΄ Β· (1 / π₯)))) |
65 | 63, 64 | eqtr4d 2779 |
. . . 4
β’ ((π΄ β β β§ π₯ β π·) β (π΄ Β· ((π₯βππ΄) Β· (1 / π₯))) = (((π₯βππ΄) Β· π΄) Β· (1 / π₯))) |
66 | 52 | oveq1d 7322 |
. . . . 5
β’ ((π΄ β β β§ π₯ β π·) β ((π₯βππ΄) Β· π΄) = ((expβ(π΄ Β· (logβπ₯))) Β· π΄)) |
67 | 66 | oveq1d 7322 |
. . . 4
β’ ((π΄ β β β§ π₯ β π·) β (((π₯βππ΄) Β· π΄) Β· (1 / π₯)) = (((expβ(π΄ Β· (logβπ₯))) Β· π΄) Β· (1 / π₯))) |
68 | 62, 65, 67 | 3eqtrd 2780 |
. . 3
β’ ((π΄ β β β§ π₯ β π·) β (π΄ Β· (π₯βπ(π΄ β 1))) = (((expβ(π΄ Β· (logβπ₯))) Β· π΄) Β· (1 / π₯))) |
69 | 68 | mpteq2dva 5181 |
. 2
β’ (π΄ β β β (π₯ β π· β¦ (π΄ Β· (π₯βπ(π΄ β 1)))) = (π₯ β π· β¦ (((expβ(π΄ Β· (logβπ₯))) Β· π΄) Β· (1 / π₯)))) |
70 | 48, 54, 69 | 3eqtr4d 2786 |
1
β’ (π΄ β β β (β
D (π₯ β π· β¦ (π₯βππ΄))) = (π₯ β π· β¦ (π΄ Β· (π₯βπ(π΄ β 1))))) |