Metamath Proof Explorer

Theorem advlog

Description: The antiderivative of the logarithm. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion advlog 
|- ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) )

Proof

Step Hyp Ref Expression
1 reelprrecn 
 |-  RR e. { RR , CC }
2 1 a1i 
 |-  ( T. -> RR e. { RR , CC } )
3 rpre 
 |-  ( x e. RR+ -> x e. RR )
4 3 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR )
5 4 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> x e. CC )
6 1cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. CC )
7 recn 
 |-  ( x e. RR -> x e. CC )
8 7 adantl 
 |-  ( ( T. /\ x e. RR ) -> x e. CC )
9 1red 
 |-  ( ( T. /\ x e. RR ) -> 1 e. RR )
10 2 dvmptid 
 |-  ( T. -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
11 rpssre 
 |-  RR+ C_ RR
12 11 a1i 
 |-  ( T. -> RR+ C_ RR )
13 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
14 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
15 ioorp 
 |-  ( 0 (,) +oo ) = RR+
16 iooretop 
 |-  ( 0 (,) +oo ) e. ( topGen ` ran (,) )
17 15 16 eqeltrri 
 |-  RR+ e. ( topGen ` ran (,) )
18 17 a1i 
 |-  ( T. -> RR+ e. ( topGen ` ran (,) ) )
19 2 8 9 10 12 13 14 18 dvmptres 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> x ) ) = ( x e. RR+ |-> 1 ) )
20 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
21 20 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. RR )
22 peano2rem 
 |-  ( ( log ` x ) e. RR -> ( ( log ` x ) - 1 ) e. RR )
23 21 22 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) - 1 ) e. RR )
24 23 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) - 1 ) e. CC )
25 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
26 25 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
27 26 rpcnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. CC )
28 21 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. CC )
29 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
30 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
31 29 30 mp1i 
 |-  ( T. -> ( log |` RR+ ) : RR+ --> RR )
32 31 feqmptd 
 |-  ( T. -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
33 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
34 33 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
35 32 34 eqtrdi 
 |-  ( T. -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
36 35 oveq2d 
 |-  ( T. -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
37 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
38 36 37 eqtr3di 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
39 0cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 0 e. CC )
40 1cnd 
 |-  ( ( T. /\ x e. RR ) -> 1 e. CC )
41 0cnd 
 |-  ( ( T. /\ x e. RR ) -> 0 e. CC )
42 1cnd 
 |-  ( T. -> 1 e. CC )
43 2 42 dvmptc 
 |-  ( T. -> ( RR _D ( x e. RR |-> 1 ) ) = ( x e. RR |-> 0 ) )
44 2 40 41 43 12 13 14 18 dvmptres 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> 1 ) ) = ( x e. RR+ |-> 0 ) )
45 2 28 27 38 6 39 44 dvmptsub 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) - 1 ) ) ) = ( x e. RR+ |-> ( ( 1 / x ) - 0 ) ) )
46 27 subid1d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 1 / x ) - 0 ) = ( 1 / x ) )
47 46 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( 1 / x ) - 0 ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
48 45 47 eqtrd 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( ( log ` x ) - 1 ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
49 2 5 6 19 24 27 48 dvmptmul 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( ( 1 x. ( ( log ` x ) - 1 ) ) + ( ( 1 / x ) x. x ) ) ) )
50 24 mullidd 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 x. ( ( log ` x ) - 1 ) ) = ( ( log ` x ) - 1 ) )
51 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
52 51 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> x =/= 0 )
53 5 52 recid2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 1 / x ) x. x ) = 1 )
54 50 53 oveq12d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 1 x. ( ( log ` x ) - 1 ) ) + ( ( 1 / x ) x. x ) ) = ( ( ( log ` x ) - 1 ) + 1 ) )
55 ax-1cn 
 |-  1 e. CC
56 npcan 
 |-  ( ( ( log ` x ) e. CC /\ 1 e. CC ) -> ( ( ( log ` x ) - 1 ) + 1 ) = ( log ` x ) )
57 28 55 56 sylancl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( log ` x ) - 1 ) + 1 ) = ( log ` x ) )
58 54 57 eqtrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( 1 x. ( ( log ` x ) - 1 ) ) + ( ( 1 / x ) x. x ) ) = ( log ` x ) )
59 58 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( 1 x. ( ( log ` x ) - 1 ) ) + ( ( 1 / x ) x. x ) ) ) = ( x e. RR+ |-> ( log ` x ) ) )
60 49 59 eqtrd 
 |-  ( T. -> ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) ) )
61 60 mptru 
 |-  ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) )