Metamath Proof Explorer


Theorem advlog

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

Ref Expression
Assertion advlog dx + x log x 1 d x = x + log x

Proof

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