dvrelog2b

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

	Ref	Expression
Hypotheses	dvrelog2b.1	$⊢ φ \to A \in ℝ^{*}$
	dvrelog2b.2	$⊢ φ \to B \in ℝ^{*}$
	dvrelog2b.3	$⊢ φ \to 0 \leq A$
	dvrelog2b.4	$⊢ φ \to A \leq B$
	dvrelog2b.5	$⊢ F = (x \in (A, B) ⟼ \log_{2} x)$
	dvrelog2b.6	$⊢ G = (x \in (A, B) ⟼ \frac{1}{x \log 2})$
Assertion	dvrelog2b	$⊢ φ \to ℝ D F = G$

Proof

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

Metamath Proof Explorer

Theorem dvrelog2b

Proof