This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem advlog

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

Ref Expression
Assertion advlog ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
2 1 a1i ⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
3 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
4 3 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
5 4 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
6 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
7 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
8 7 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
9 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℝ )
10 2 dvmptid ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
11 rpssre ⊢ ℝ+ ⊆ ℝ
12 11 a1i ⊢ ( ⊤ → ℝ+ ⊆ ℝ )
13 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
14 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( 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 13 14 18 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ 1 ) )
20 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
21 20 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
22 peano2rem ⊢ ( ( log ‘ 𝑥 ) ∈ ℝ → ( ( log ‘ 𝑥 ) − 1 ) ∈ ℝ )
23 21 22 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) − 1 ) ∈ ℝ )
24 23 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) − 1 ) ∈ ℂ )
25 rpreccl ⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
26 25 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
27 26 rpcnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℂ )
28 21 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
29 relogf1o ⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
30 f1of ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
31 29 30 mp1i ⊢ ( ⊤ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
32 31 feqmptd ⊢ ( ⊤ → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) )
33 fvres ⊢ ( 𝑥 ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
34 33 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( log ↾ ℝ+ ) ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )
35 32 34 eqtrdi ⊢ ( ⊤ → ( log ↾ ℝ+ ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
36 35 oveq2d ⊢ ( ⊤ → ( ℝ D ( log ↾ ℝ+ ) ) = ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) )
37 dvrelog ⊢ ( ℝ D ( log ↾ ℝ+ ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) )
38 36 37 eqtr3di ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
39 0cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 0 ∈ ℂ )
40 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ )
41 0cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℂ )
42 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
43 2 42 dvmptc ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ ↦ 1 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
44 2 40 41 43 12 13 14 18 dvmptres ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ 1 ) ) = ( 𝑥 ∈ ℝ+ ↦ 0 ) )
45 2 28 27 38 6 39 44 dvmptsub ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 𝑥 ) − 0 ) ) )
46 27 subid1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 / 𝑥 ) − 0 ) = ( 1 / 𝑥 ) )
47 46 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 / 𝑥 ) − 0 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
48 45 47 eqtrd ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ 𝑥 ) − 1 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
49 2 5 6 19 24 27 48 dvmptmul ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 1 · ( ( log ‘ 𝑥 ) − 1 ) ) + ( ( 1 / 𝑥 ) · 𝑥 ) ) ) )
50 24 mullidd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 · ( ( log ‘ 𝑥 ) − 1 ) ) = ( ( log ‘ 𝑥 ) − 1 ) )
51 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
52 51 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
53 5 52 recid2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
54 50 53 oveq12d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 · ( ( log ‘ 𝑥 ) − 1 ) ) + ( ( 1 / 𝑥 ) · 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) − 1 ) + 1 ) )
55 ax-1cn ⊢ 1 ∈ ℂ
56 npcan ⊢ ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( log ‘ 𝑥 ) − 1 ) + 1 ) = ( log ‘ 𝑥 ) )
57 28 55 56 sylancl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) − 1 ) + 1 ) = ( log ‘ 𝑥 ) )
58 54 57 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 · ( ( log ‘ 𝑥 ) − 1 ) ) + ( ( 1 / 𝑥 ) · 𝑥 ) ) = ( log ‘ 𝑥 ) )
59 58 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 · ( ( log ‘ 𝑥 ) − 1 ) ) + ( ( 1 / 𝑥 ) · 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
60 49 59 eqtrd ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) )
61 60 mptru ⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · ( ( log ‘ 𝑥 ) − 1 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) )