Step | Hyp | Ref
| Expression |
1 | | reelprrecn 11009 |
. . . 4
β’ β
β {β, β} |
2 | 1 | a1i 11 |
. . 3
β’ (π΄ β β β β
β {β, β}) |
3 | | relogcl 25776 |
. . . 4
β’ (π₯ β β+
β (logβπ₯) β
β) |
4 | 3 | adantl 483 |
. . 3
β’ ((π΄ β β β§ π₯ β β+)
β (logβπ₯) β
β) |
5 | | rpreccl 12802 |
. . . 4
β’ (π₯ β β+
β (1 / π₯) β
β+) |
6 | 5 | adantl 483 |
. . 3
β’ ((π΄ β β β§ π₯ β β+)
β (1 / π₯) β
β+) |
7 | | recn 11007 |
. . . 4
β’ (π¦ β β β π¦ β
β) |
8 | | mulcl 11001 |
. . . . 5
β’ ((π΄ β β β§ π¦ β β) β (π΄ Β· π¦) β β) |
9 | | efcl 15837 |
. . . . 5
β’ ((π΄ Β· π¦) β β β (expβ(π΄ Β· π¦)) β β) |
10 | 8, 9 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π¦ β β) β
(expβ(π΄ Β·
π¦)) β
β) |
11 | 7, 10 | sylan2 594 |
. . 3
β’ ((π΄ β β β§ π¦ β β) β
(expβ(π΄ Β·
π¦)) β
β) |
12 | | ovexd 7342 |
. . 3
β’ ((π΄ β β β§ π¦ β β) β
((expβ(π΄ Β·
π¦)) Β· π΄) β V) |
13 | | relogf1o 25767 |
. . . . . . . 8
β’ (log
βΎ β+):β+β1-1-ontoββ |
14 | | f1of 6746 |
. . . . . . . 8
β’ ((log
βΎ β+):β+β1-1-ontoββ β (log βΎ
β+):β+βΆβ) |
15 | 13, 14 | mp1i 13 |
. . . . . . 7
β’ (π΄ β β β (log
βΎ
β+):β+βΆβ) |
16 | 15 | feqmptd 6869 |
. . . . . 6
β’ (π΄ β β β (log
βΎ β+) = (π₯ β β+ β¦ ((log
βΎ β+)βπ₯))) |
17 | | fvres 6823 |
. . . . . . 7
β’ (π₯ β β+
β ((log βΎ β+)βπ₯) = (logβπ₯)) |
18 | 17 | mpteq2ia 5184 |
. . . . . 6
β’ (π₯ β β+
β¦ ((log βΎ β+)βπ₯)) = (π₯ β β+ β¦
(logβπ₯)) |
19 | 16, 18 | eqtrdi 2792 |
. . . . 5
β’ (π΄ β β β (log
βΎ β+) = (π₯ β β+ β¦
(logβπ₯))) |
20 | 19 | oveq2d 7323 |
. . . 4
β’ (π΄ β β β (β
D (log βΎ β+)) = (β D (π₯ β β+ β¦
(logβπ₯)))) |
21 | | dvrelog 25837 |
. . . 4
β’ (β
D (log βΎ β+)) = (π₯ β β+ β¦ (1 /
π₯)) |
22 | 20, 21 | eqtr3di 2791 |
. . 3
β’ (π΄ β β β (β
D (π₯ β
β+ β¦ (logβπ₯))) = (π₯ β β+ β¦ (1 /
π₯))) |
23 | | eqid 2736 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
24 | 23 | cnfldtopon 23991 |
. . . . 5
β’
(TopOpenββfld) β
(TopOnββ) |
25 | | toponmax 22120 |
. . . . 5
β’
((TopOpenββfld) β (TopOnββ)
β β β (TopOpenββfld)) |
26 | 24, 25 | mp1i 13 |
. . . 4
β’ (π΄ β β β β
β (TopOpenββfld)) |
27 | | ax-resscn 10974 |
. . . . . 6
β’ β
β β |
28 | 27 | a1i 11 |
. . . . 5
β’ (π΄ β β β β
β β) |
29 | | df-ss 3909 |
. . . . 5
β’ (β
β β β (β β© β) = β) |
30 | 28, 29 | sylib 217 |
. . . 4
β’ (π΄ β β β (β
β© β) = β) |
31 | | ovexd 7342 |
. . . 4
β’ ((π΄ β β β§ π¦ β β) β
((expβ(π΄ Β·
π¦)) Β· π΄) β V) |
32 | | cnelprrecn 11010 |
. . . . . 6
β’ β
β {β, β} |
33 | 32 | a1i 11 |
. . . . 5
β’ (π΄ β β β β
β {β, β}) |
34 | | simpl 484 |
. . . . 5
β’ ((π΄ β β β§ π¦ β β) β π΄ β
β) |
35 | | efcl 15837 |
. . . . . 6
β’ (π₯ β β β
(expβπ₯) β
β) |
36 | 35 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β) β
(expβπ₯) β
β) |
37 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β β) β π¦ β
β) |
38 | | 1cnd 11016 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β β) β 1 β
β) |
39 | 33 | dvmptid 25166 |
. . . . . . 7
β’ (π΄ β β β (β
D (π¦ β β β¦
π¦)) = (π¦ β β β¦ 1)) |
40 | | id 22 |
. . . . . . 7
β’ (π΄ β β β π΄ β
β) |
41 | 33, 37, 38, 39, 40 | dvmptcmul 25173 |
. . . . . 6
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ (π΄ Β· 1))) |
42 | | mulid1 11019 |
. . . . . . 7
β’ (π΄ β β β (π΄ Β· 1) = π΄) |
43 | 42 | mpteq2dv 5183 |
. . . . . 6
β’ (π΄ β β β (π¦ β β β¦ (π΄ Β· 1)) = (π¦ β β β¦ π΄)) |
44 | 41, 43 | eqtrd 2776 |
. . . . 5
β’ (π΄ β β β (β
D (π¦ β β β¦
(π΄ Β· π¦))) = (π¦ β β β¦ π΄)) |
45 | | dvef 25189 |
. . . . . 6
β’ (β
D exp) = exp |
46 | | eff 15836 |
. . . . . . . . . 10
β’
exp:ββΆβ |
47 | 46 | a1i 11 |
. . . . . . . . 9
β’ (π΄ β β β
exp:ββΆβ) |
48 | 47 | feqmptd 6869 |
. . . . . . . 8
β’ (π΄ β β β exp =
(π₯ β β β¦
(expβπ₯))) |
49 | 48 | eqcomd 2742 |
. . . . . . 7
β’ (π΄ β β β (π₯ β β β¦
(expβπ₯)) =
exp) |
50 | 49 | oveq2d 7323 |
. . . . . 6
β’ (π΄ β β β (β
D (π₯ β β β¦
(expβπ₯))) = (β
D exp)) |
51 | 45, 50, 49 | 3eqtr4a 2802 |
. . . . 5
β’ (π΄ β β β (β
D (π₯ β β β¦
(expβπ₯))) = (π₯ β β β¦
(expβπ₯))) |
52 | | fveq2 6804 |
. . . . 5
β’ (π₯ = (π΄ Β· π¦) β (expβπ₯) = (expβ(π΄ Β· π¦))) |
53 | 33, 33, 8, 34, 36, 36, 44, 51, 52, 52 | dvmptco 25181 |
. . . 4
β’ (π΄ β β β (β
D (π¦ β β β¦
(expβ(π΄ Β·
π¦)))) = (π¦ β β β¦ ((expβ(π΄ Β· π¦)) Β· π΄))) |
54 | 23, 2, 26, 30, 10, 31, 53 | dvmptres3 25165 |
. . 3
β’ (π΄ β β β (β
D (π¦ β β β¦
(expβ(π΄ Β·
π¦)))) = (π¦ β β β¦ ((expβ(π΄ Β· π¦)) Β· π΄))) |
55 | | oveq2 7315 |
. . . 4
β’ (π¦ = (logβπ₯) β (π΄ Β· π¦) = (π΄ Β· (logβπ₯))) |
56 | 55 | fveq2d 6808 |
. . 3
β’ (π¦ = (logβπ₯) β (expβ(π΄ Β· π¦)) = (expβ(π΄ Β· (logβπ₯)))) |
57 | 56 | oveq1d 7322 |
. . 3
β’ (π¦ = (logβπ₯) β ((expβ(π΄ Β· π¦)) Β· π΄) = ((expβ(π΄ Β· (logβπ₯))) Β· π΄)) |
58 | 2, 2, 4, 6, 11, 12, 22, 54, 56, 57 | dvmptco 25181 |
. 2
β’ (π΄ β β β (β
D (π₯ β
β+ β¦ (expβ(π΄ Β· (logβπ₯))))) = (π₯ β β+ β¦
(((expβ(π΄ Β·
(logβπ₯))) Β·
π΄) Β· (1 / π₯)))) |
59 | | rpcn 12786 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
60 | 59 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β π₯ β
β) |
61 | | rpne0 12792 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
0) |
62 | 61 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β π₯ β
0) |
63 | | simpl 484 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β π΄ β
β) |
64 | 60, 62, 63 | cxpefd 25912 |
. . . 4
β’ ((π΄ β β β§ π₯ β β+)
β (π₯βππ΄) = (expβ(π΄ Β· (logβπ₯)))) |
65 | 64 | mpteq2dva 5181 |
. . 3
β’ (π΄ β β β (π₯ β β+
β¦ (π₯βππ΄)) = (π₯ β β+ β¦
(expβ(π΄ Β·
(logβπ₯))))) |
66 | 65 | oveq2d 7323 |
. 2
β’ (π΄ β β β (β
D (π₯ β
β+ β¦ (π₯βππ΄))) = (β D (π₯ β β+ β¦
(expβ(π΄ Β·
(logβπ₯)))))) |
67 | | 1cnd 11016 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β+)
β 1 β β) |
68 | 60, 62, 63, 67 | cxpsubd 25918 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β+)
β (π₯βπ(π΄ β 1)) = ((π₯βππ΄) / (π₯βπ1))) |
69 | 60 | cxp1d 25906 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β+)
β (π₯βπ1) = π₯) |
70 | 69 | oveq2d 7323 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β+)
β ((π₯βππ΄) / (π₯βπ1)) = ((π₯βππ΄) / π₯)) |
71 | 60, 63 | cxpcld 25908 |
. . . . . . 7
β’ ((π΄ β β β§ π₯ β β+)
β (π₯βππ΄) β β) |
72 | 71, 60, 62 | divrecd 11800 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β+)
β ((π₯βππ΄) / π₯) = ((π₯βππ΄) Β· (1 / π₯))) |
73 | 68, 70, 72 | 3eqtrd 2780 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β (π₯βπ(π΄ β 1)) = ((π₯βππ΄) Β· (1 / π₯))) |
74 | 73 | oveq2d 7323 |
. . . 4
β’ ((π΄ β β β§ π₯ β β+)
β (π΄ Β· (π₯βπ(π΄ β 1))) = (π΄ Β· ((π₯βππ΄) Β· (1 / π₯)))) |
75 | 6 | rpcnd 12820 |
. . . . . 6
β’ ((π΄ β β β§ π₯ β β+)
β (1 / π₯) β
β) |
76 | 63, 71, 75 | mul12d 11230 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β (π΄ Β· ((π₯βππ΄) Β· (1 / π₯))) = ((π₯βππ΄) Β· (π΄ Β· (1 / π₯)))) |
77 | 71, 63, 75 | mulassd 11044 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β (((π₯βππ΄) Β· π΄) Β· (1 / π₯)) = ((π₯βππ΄) Β· (π΄ Β· (1 / π₯)))) |
78 | 76, 77 | eqtr4d 2779 |
. . . 4
β’ ((π΄ β β β§ π₯ β β+)
β (π΄ Β· ((π₯βππ΄) Β· (1 / π₯))) = (((π₯βππ΄) Β· π΄) Β· (1 / π₯))) |
79 | 64 | oveq1d 7322 |
. . . . 5
β’ ((π΄ β β β§ π₯ β β+)
β ((π₯βππ΄) Β· π΄) = ((expβ(π΄ Β· (logβπ₯))) Β· π΄)) |
80 | 79 | oveq1d 7322 |
. . . 4
β’ ((π΄ β β β§ π₯ β β+)
β (((π₯βππ΄) Β· π΄) Β· (1 / π₯)) = (((expβ(π΄ Β· (logβπ₯))) Β· π΄) Β· (1 / π₯))) |
81 | 74, 78, 80 | 3eqtrd 2780 |
. . 3
β’ ((π΄ β β β§ π₯ β β+)
β (π΄ Β· (π₯βπ(π΄ β 1))) =
(((expβ(π΄ Β·
(logβπ₯))) Β·
π΄) Β· (1 / π₯))) |
82 | 81 | mpteq2dva 5181 |
. 2
β’ (π΄ β β β (π₯ β β+
β¦ (π΄ Β· (π₯βπ(π΄ β 1)))) = (π₯ β β+
β¦ (((expβ(π΄
Β· (logβπ₯)))
Β· π΄) Β· (1 /
π₯)))) |
83 | 58, 66, 82 | 3eqtr4d 2786 |
1
β’ (π΄ β β β (β
D (π₯ β
β+ β¦ (π₯βππ΄))) = (π₯ β β+ β¦ (π΄ Β· (π₯βπ(π΄ β 1))))) |