Step | Hyp | Ref
| Expression |
1 | | dvrelog3.5 |
. . . . 5
β’ πΉ = (π₯ β (π΄(,)π΅) β¦ (logβπ₯)) |
2 | 1 | a1i 11 |
. . . 4
β’ (π β πΉ = (π₯ β (π΄(,)π΅) β¦ (logβπ₯))) |
3 | 2 | oveq2d 7374 |
. . 3
β’ (π β (β D πΉ) = (β D (π₯ β (π΄(,)π΅) β¦ (logβπ₯)))) |
4 | | reelprrecn 11148 |
. . . . 5
β’ β
β {β, β} |
5 | 4 | a1i 11 |
. . . 4
β’ (π β β β {β,
β}) |
6 | | rpcn 12930 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
7 | 6 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β
β) |
8 | | rpne0 12936 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
0) |
9 | 8 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β 0) |
10 | 7, 9 | logcld 25942 |
. . . 4
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
11 | | 1red 11161 |
. . . . 5
β’ ((π β§ π₯ β β+) β 1 β
β) |
12 | | rpre 12928 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
13 | 12 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β
β) |
14 | 11, 13, 9 | redivcld 11988 |
. . . 4
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
15 | | logf1o 25936 |
. . . . . . . . . 10
β’
log:(β β {0})β1-1-ontoβran
log |
16 | | f1of 6785 |
. . . . . . . . . 10
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
β’
log:(β β {0})βΆran log |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ (π β log:(β β
{0})βΆran log) |
19 | | 0nrp 12955 |
. . . . . . . . . . . 12
β’ Β¬ 0
β β+ |
20 | | disjsn 4673 |
. . . . . . . . . . . 12
β’
((β+ β© {0}) = β
β Β¬ 0 β
β+) |
21 | 19, 20 | mpbir 230 |
. . . . . . . . . . 11
β’
(β+ β© {0}) = β
|
22 | | disjdif2 4440 |
. . . . . . . . . . 11
β’
((β+ β© {0}) = β
β (β+
β {0}) = β+) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . 10
β’
(β+ β {0}) = β+ |
24 | | rpssre 12927 |
. . . . . . . . . . . 12
β’
β+ β β |
25 | | ax-resscn 11113 |
. . . . . . . . . . . 12
β’ β
β β |
26 | 24, 25 | sstri 3954 |
. . . . . . . . . . 11
β’
β+ β β |
27 | | ssdif 4100 |
. . . . . . . . . . 11
β’
(β+ β β β (β+ β
{0}) β (β β {0})) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . 10
β’
(β+ β {0}) β (β β
{0}) |
29 | 23, 28 | eqsstrri 3980 |
. . . . . . . . 9
β’
β+ β (β β {0}) |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β (β β {0})) |
31 | 18, 30 | feqresmpt 6912 |
. . . . . . 7
β’ (π β (log βΎ
β+) = (π₯
β β+ β¦ (logβπ₯))) |
32 | 31 | eqcomd 2739 |
. . . . . 6
β’ (π β (π₯ β β+ β¦
(logβπ₯)) = (log
βΎ β+)) |
33 | 32 | oveq2d 7374 |
. . . . 5
β’ (π β (β D (π₯ β β+
β¦ (logβπ₯))) =
(β D (log βΎ β+))) |
34 | | dvrelog 26008 |
. . . . . 6
β’ (β
D (log βΎ β+)) = (π₯ β β+ β¦ (1 /
π₯)) |
35 | 34 | a1i 11 |
. . . . 5
β’ (π β (β D (log βΎ
β+)) = (π₯
β β+ β¦ (1 / π₯))) |
36 | 33, 35 | eqtrd 2773 |
. . . 4
β’ (π β (β D (π₯ β β+
β¦ (logβπ₯))) =
(π₯ β
β+ β¦ (1 / π₯))) |
37 | | dvrelog3.1 |
. . . . . . . . . . 11
β’ (π β π΄ β
β*) |
38 | | dvrelog3.2 |
. . . . . . . . . . 11
β’ (π β π΅ β
β*) |
39 | | elioo2 13311 |
. . . . . . . . . . 11
β’ ((π΄ β β*
β§ π΅ β
β*) β (π¦ β (π΄(,)π΅) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅))) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π¦ β (π΄(,)π΅) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅))) |
41 | 40 | biimpa 478 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦ β β β§ π΄ < π¦ β§ π¦ < π΅)) |
42 | 41 | simp1d 1143 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β) |
43 | | 0red 11163 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β β) |
44 | 43 | rexrd 11210 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β
β*) |
45 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β
β*) |
46 | 42 | rexrd 11210 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β*) |
47 | | dvrelog3.3 |
. . . . . . . . . 10
β’ (π β 0 β€ π΄) |
48 | 47 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 β€ π΄) |
49 | 41 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ < π¦) |
50 | 44, 45, 46, 48, 49 | xrlelttrd 13085 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄(,)π΅)) β 0 < π¦) |
51 | 42, 50 | jca 513 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π¦ β β β§ 0 < π¦)) |
52 | | elrp 12922 |
. . . . . . 7
β’ (π¦ β β+
β (π¦ β β
β§ 0 < π¦)) |
53 | 51, 52 | sylibr 233 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β β+) |
54 | 53 | ex 414 |
. . . . 5
β’ (π β (π¦ β (π΄(,)π΅) β π¦ β
β+)) |
55 | 54 | ssrdv 3951 |
. . . 4
β’ (π β (π΄(,)π΅) β
β+) |
56 | | eqid 2733 |
. . . . 5
β’
(TopOpenββfld) =
(TopOpenββfld) |
57 | 56 | tgioo2 24182 |
. . . 4
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
58 | | retop 24141 |
. . . . . 6
β’
(topGenβran (,)) β Top |
59 | 58 | a1i 11 |
. . . . 5
β’ (π β (topGenβran (,))
β Top) |
60 | | iooretop 24145 |
. . . . . 6
β’ (π΄(,)π΅) β (topGenβran
(,)) |
61 | 60 | a1i 11 |
. . . . 5
β’ (π β (π΄(,)π΅) β (topGenβran
(,))) |
62 | | isopn3i 22449 |
. . . . 5
β’
(((topGenβran (,)) β Top β§ (π΄(,)π΅) β (topGenβran (,))) β
((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅)) |
63 | 59, 61, 62 | syl2anc 585 |
. . . 4
β’ (π β
((intβ(topGenβran (,)))β(π΄(,)π΅)) = (π΄(,)π΅)) |
64 | 5, 10, 14, 36, 55, 57, 56, 63 | dvmptres2 25342 |
. . 3
β’ (π β (β D (π₯ β (π΄(,)π΅) β¦ (logβπ₯))) = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
65 | 3, 64 | eqtrd 2773 |
. 2
β’ (π β (β D πΉ) = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
66 | | dvrelog3.6 |
. . . 4
β’ πΊ = (π₯ β (π΄(,)π΅) β¦ (1 / π₯)) |
67 | 66 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
68 | 67 | eqcomd 2739 |
. 2
β’ (π β (π₯ β (π΄(,)π΅) β¦ (1 / π₯)) = πΊ) |
69 | 65, 68 | eqtrd 2773 |
1
β’ (π β (β D πΉ) = πΊ) |