Theorem dvrelog2b

Description: Derivative of the binary logarithm. (Contributed by metakunt, 11-Aug-2024)

	Ref	Expression
Hypotheses	dvrelog2b.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	dvrelog2b.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	dvrelog2b.3	⊢ ( 𝜑 → 0 ≤ 𝐴 )
	dvrelog2b.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	dvrelog2b.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) )
	dvrelog2b.6	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
Assertion	dvrelog2b	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		dvrelog2b.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		dvrelog2b.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		dvrelog2b.3	⊢ ( 𝜑 → 0 ≤ 𝐴 )
4		dvrelog2b.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		dvrelog2b.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) )
6		dvrelog2b.6	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
7	5	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) )
8		2cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ℂ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 0 )
11		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ∈ ℝ )
12		1lt2	⊢ 1 < 2
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 < 2 )
14	11 13	ltned	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 1 ≠ 2 )
15	14	necomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ≠ 1 )
16	10 15	nelprd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 2 ∈ { 0 , 1 } )
17	8 16	eldifd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 2 ∈ ( ℂ ∖ { 0 , 1 } ) )
18		elioore	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℝ )
19		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
20	18 19	syl	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ℂ )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℂ )
22		elsni	⊢ ( 𝑥 ∈ { 0 } → 𝑥 = 0 )
23		0xr	⊢ 0 ∈ ℝ*
24	23	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
25		xrlenlt	⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
26	24 1 25	syl2anc	⊢ ( 𝜑 → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
27	3 26	mpbid	⊢ ( 𝜑 → ¬ 𝐴 < 0 )
28	27	orcd	⊢ ( 𝜑 → ( ¬ 𝐴 < 0 ∨ ¬ 0 < 𝐵 ) )
29		ianor	⊢ ( ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ↔ ( ¬ 𝐴 < 0 ∨ ¬ 0 < 𝐵 ) )
30	28 29	sylibr	⊢ ( 𝜑 → ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) )
31		elioo5	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
32	1 2 24 31	syl3anc	⊢ ( 𝜑 → ( 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
33	32	notbid	⊢ ( 𝜑 → ( ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) ↔ ¬ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
34	30 33	mpbird	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
35	34	a1d	⊢ ( 𝜑 → ( 0 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
36	35	imp	⊢ ( ( 𝜑 ∧ 0 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
37	36	pm2.01da	⊢ ( 𝜑 → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ¬ 0 ∈ ( 𝐴 (,) 𝐵 ) )
39		eleq1	⊢ ( 𝑥 = 0 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
40	39	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↔ 0 ∈ ( 𝐴 (,) 𝐵 ) ) )
41	38 40	mtbird	⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
42	22 41	sylan2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 0 } ) → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
43	42	ex	⊢ ( 𝜑 → ( 𝑥 ∈ { 0 } → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
44	43	con2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 ∈ { 0 } ) )
45	44	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ¬ 𝑥 ∈ { 0 } )
46	21 45	eldifd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
47		logbval	⊢ ( ( 2 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
48	17 46 47	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 2 logb 𝑥 ) = ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) )
49	48	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 2 logb 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) )
50	7 49	eqtrd	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) )
51	50	oveq2d	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) )
52		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
53	52	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
54	41	ex	⊢ ( 𝜑 → ( 𝑥 = 0 → ¬ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
55	54	con2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 0 ) )
56		biidd	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝑥 = 0 ↔ 𝑥 = 0 ) )
57	56	necon3bbid	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ¬ 𝑥 = 0 ↔ 𝑥 ≠ 0 ) )
58	57	pm5.74i	⊢ ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ¬ 𝑥 = 0 ) ↔ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 0 ) )
59	55 58	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ≠ 0 ) )
60	59	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ≠ 0 )
61	21 60	logcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
62	18	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ℝ )
63	11 62 60	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 1 / 𝑥 ) ∈ ℝ )
64		eqid	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) )
65		eqid	⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) )
66	1 2 3 4 64 65	dvrelog3	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / 𝑥 ) ) )
67		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
68	9	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
69	67 68	logcld	⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
70		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
71		2rp	⊢ 2 ∈ ℝ+
72		loggt0b	⊢ ( 2 ∈ ℝ+ → ( 0 < ( log ‘ 2 ) ↔ 1 < 2 ) )
73	71 72	ax-mp	⊢ ( 0 < ( log ‘ 2 ) ↔ 1 < 2 )
74	12 73	mpbir	⊢ 0 < ( log ‘ 2 )
75	74	a1i	⊢ ( 𝜑 → 0 < ( log ‘ 2 ) )
76	70 75	ltned	⊢ ( 𝜑 → 0 ≠ ( log ‘ 2 ) )
77	76	necomd	⊢ ( 𝜑 → ( log ‘ 2 ) ≠ 0 )
78	53 61 63 66 69 77	dvmptdivc	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) )
79	8 10	logcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ∈ ℂ )
80	77	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( log ‘ 2 ) ≠ 0 )
81	21 79 60 80	recdiv2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) = ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) )
82	81	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
83	6	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) )
84	83	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) = 𝐺 )
85	82 84	eqtrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 1 / 𝑥 ) / ( log ‘ 2 ) ) ) = 𝐺 )
86	78 85	eqtrd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 2 ) ) ) ) = 𝐺 )
87	51 86	eqtrd	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )