Step | Hyp | Ref
| Expression |
1 | | dvrelog2.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 | | rpssre 12927 |
. . . . . . . 8
β’
β+ β β |
7 | | ax-resscn 11113 |
. . . . . . . 8
β’ β
β β |
8 | 6, 7 | sstri 3954 |
. . . . . . 7
β’
β+ β β |
9 | 8 | sseli 3941 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β
β) |
11 | | rpne0 12936 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
0) |
12 | 11 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β π₯ β 0) |
13 | 10, 12 | logcld 25942 |
. . . 4
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
14 | | 1red 11161 |
. . . . . 6
β’ (π₯ β β+
β 1 β β) |
15 | 6 | sseli 3941 |
. . . . . 6
β’ (π₯ β β+
β π₯ β
β) |
16 | 14, 15, 11 | redivcld 11988 |
. . . . 5
β’ (π₯ β β+
β (1 / π₯) β
β) |
17 | 16 | adantl 483 |
. . . 4
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
18 | | logf1o 25936 |
. . . . . . . . . 10
β’
log:(β β {0})β1-1-ontoβran
log |
19 | | f1of 6785 |
. . . . . . . . . 10
β’
(log:(β β {0})β1-1-ontoβran
log β log:(β β {0})βΆran log) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . 9
β’
log:(β β {0})βΆran log |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ (π β log:(β β
{0})βΆran log) |
22 | | 0nrp 12955 |
. . . . . . . . . . . 12
β’ Β¬ 0
β β+ |
23 | | disjsn 4673 |
. . . . . . . . . . . 12
β’
((β+ β© {0}) = β
β Β¬ 0 β
β+) |
24 | 22, 23 | mpbir 230 |
. . . . . . . . . . 11
β’
(β+ β© {0}) = β
|
25 | | disjdif2 4440 |
. . . . . . . . . . 11
β’
((β+ β© {0}) = β
β (β+
β {0}) = β+) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . 10
β’
(β+ β {0}) = β+ |
27 | | ssdif 4100 |
. . . . . . . . . . 11
β’
(β+ β β β (β+ β
{0}) β (β β {0})) |
28 | 8, 27 | ax-mp 5 |
. . . . . . . . . 10
β’
(β+ β {0}) β (β β
{0}) |
29 | 26, 28 | eqsstrri 3980 |
. . . . . . . . 9
β’
β+ β (β β {0}) |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β (β β {0})) |
31 | 21, 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 | | dvrelog2.1 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
38 | | dvrelog2.2 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
39 | | elicc2 13335 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΅ β β) β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
40 | 37, 38, 39 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β (π¦ β (π΄[,]π΅) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅))) |
41 | 40 | biimpa 478 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β β β§ π΄ β€ π¦ β§ π¦ β€ π΅)) |
42 | 41 | simp1d 1143 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β β) |
43 | | 0red 11163 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β 0 β β) |
44 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β β) |
45 | | dvrelog2.3 |
. . . . . . . . . 10
β’ (π β 0 < π΄) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β 0 < π΄) |
47 | 41 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π΄[,]π΅)) β π΄ β€ π¦) |
48 | 43, 44, 42, 46, 47 | ltletrd 11320 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΄[,]π΅)) β 0 < π¦) |
49 | 42, 48 | jca 513 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄[,]π΅)) β (π¦ β β β§ 0 < π¦)) |
50 | | elrp 12922 |
. . . . . . 7
β’ (π¦ β β+
β (π¦ β β
β§ 0 < π¦)) |
51 | 49, 50 | sylibr 233 |
. . . . . 6
β’ ((π β§ π¦ β (π΄[,]π΅)) β π¦ β β+) |
52 | 51 | ex 414 |
. . . . 5
β’ (π β (π¦ β (π΄[,]π΅) β π¦ β
β+)) |
53 | 52 | ssrdv 3951 |
. . . 4
β’ (π β (π΄[,]π΅) β
β+) |
54 | | eqid 2733 |
. . . . 5
β’
(TopOpenββfld) =
(TopOpenββfld) |
55 | 54 | tgioo2 24182 |
. . . 4
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
56 | | iccntr 24200 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
57 | 37, 38, 56 | syl2anc 585 |
. . . 4
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
58 | 5, 13, 17, 36, 53, 55, 54, 57 | dvmptres2 25342 |
. . 3
β’ (π β (β D (π₯ β (π΄[,]π΅) β¦ (logβπ₯))) = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
59 | 3, 58 | eqtrd 2773 |
. 2
β’ (π β (β D πΉ) = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
60 | | dvrelog2.6 |
. . . 4
β’ πΊ = (π₯ β (π΄(,)π΅) β¦ (1 / π₯)) |
61 | 60 | a1i 11 |
. . 3
β’ (π β πΊ = (π₯ β (π΄(,)π΅) β¦ (1 / π₯))) |
62 | 61 | eqcomd 2739 |
. 2
β’ (π β (π₯ β (π΄(,)π΅) β¦ (1 / π₯)) = πΊ) |
63 | 59, 62 | eqtrd 2773 |
1
β’ (π β (β D πΉ) = πΊ) |