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		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
14	13	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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	⊢ ( ⊤ → ( ℝ 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 14 13 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	mulid2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 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 ‘ 𝑥 ) )