dvrelogpow2b

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

	Ref	Expression
Hypotheses	dvrelogpow2b.1	$⊢ φ \to A \in ℝ$
	dvrelogpow2b.2	$⊢ φ \to B \in ℝ$
	dvrelogpow2b.3	$⊢ φ \to 0 < A$
	dvrelogpow2b.4	$⊢ φ \to A \leq B$
	dvrelogpow2b.5	$⊢ F = (x \in (A, B) ⟼ {\log_{2} x}^{N})$
	dvrelogpow2b.6	$⊢ G = (x \in (A, B) ⟼ C (\frac{{\log x}^{N - 1}}{x}))$
	dvrelogpow2b.7	$⊢ C = \frac{N}{{\log 2}^{N}}$
	dvrelogpow2b.8	$⊢ φ \to N \in ℕ$
Assertion	dvrelogpow2b	$⊢ φ \to ℝ D F = G$

Proof

Step	Hyp	Ref	Expression
1		dvrelogpow2b.1	$⊢ φ \to A \in ℝ$
2		dvrelogpow2b.2	$⊢ φ \to B \in ℝ$
3		dvrelogpow2b.3	$⊢ φ \to 0 < A$
4		dvrelogpow2b.4	$⊢ φ \to A \leq B$
5		dvrelogpow2b.5	$⊢ F = (x \in (A, B) ⟼ {\log_{2} x}^{N})$
6		dvrelogpow2b.6	$⊢ G = (x \in (A, B) ⟼ C (\frac{{\log x}^{N - 1}}{x}))$
7		dvrelogpow2b.7	$⊢ C = \frac{N}{{\log 2}^{N}}$
8		dvrelogpow2b.8	$⊢ φ \to N \in ℕ$
9	5	a1i	$⊢ φ \to F = (x \in (A, B) ⟼ {\log_{2} x}^{N})$
10	9	oveq2d	$⊢ φ \to ℝ D F = \frac{d (x \in (A, B)⟼ {\log_{2} x}^{N})}{d_{ℝ} x}$
11		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
12	11	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
13		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
14	13	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
15		elioore	$⊢ x \in (A, B) \to x \in ℝ$
16	15	adantl	$⊢ (φ \land x \in (A, B)) \to x \in ℝ$
17	16	recnd	$⊢ (φ \land x \in (A, B)) \to x \in ℂ$
18	1	adantr	$⊢ (φ \land x \in (A, B)) \to A \in ℝ$
19	2	adantr	$⊢ (φ \land x \in (A, B)) \to B \in ℝ$
20	3	adantr	$⊢ (φ \land x \in (A, B)) \to 0 < A$
21	4	adantr	$⊢ (φ \land x \in (A, B)) \to A \leq B$
22		simpr	$⊢ (φ \land x \in (A, B)) \to x \in (A, B)$
23	18 19 20 21 22	0nonelalab	$⊢ (φ \land x \in (A, B)) \to 0 \neq x$
24	23	necomd	$⊢ (φ \land x \in (A, B)) \to x \neq 0$
25	17 24	logcld	$⊢ (φ \land x \in (A, B)) \to \log x \in ℂ$
26		2cnd	$⊢ (φ \land x \in (A, B)) \to 2 \in ℂ$
27		0ne2	$⊢ 0 \neq 2$
28	27	a1i	$⊢ (φ \land x \in (A, B)) \to 0 \neq 2$
29	28	necomd	$⊢ (φ \land x \in (A, B)) \to 2 \neq 0$
30	26 29	logcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℂ$
31		0red	$⊢ (φ \land x \in (A, B)) \to 0 \in ℝ$
32		1lt2	$⊢ 1 < 2$
33	32	a1i	$⊢ (φ \land x \in (A, B)) \to 1 < 2$
34		2rp	$⊢ 2 \in ℝ^{+}$
35		loggt0b	$⊢ 2 \in ℝ^{+} \to (0 < \log 2 \leftrightarrow 1 < 2)$
36	34 35	ax-mp	$⊢ 0 < \log 2 \leftrightarrow 1 < 2$
37	33 36	sylibr	$⊢ (φ \land x \in (A, B)) \to 0 < \log 2$
38	31 37	ltned	$⊢ (φ \land x \in (A, B)) \to 0 \neq \log 2$
39	38	necomd	$⊢ (φ \land x \in (A, B)) \to \log 2 \neq 0$
40	25 30 39	divcld	$⊢ (φ \land x \in (A, B)) \to \frac{\log x}{\log 2} \in ℂ$
41		1red	$⊢ (φ \land x \in (A, B)) \to 1 \in ℝ$
42	41 33	ltned	$⊢ (φ \land x \in (A, B)) \to 1 \neq 2$
43	42	necomd	$⊢ (φ \land x \in (A, B)) \to 2 \neq 1$
44	29 43	nelprd	$⊢ (φ \land x \in (A, B)) \to \neg 2 \in \{0, 1\}$
45	26 44	eldifd	$⊢ (φ \land x \in (A, B)) \to 2 \in (ℂ ∖ \{0, 1\})$
46		necom	$⊢ 0 \neq x \leftrightarrow x \neq 0$
47	46	imbi2i	$⊢ ((φ \land x \in (A, B)) \to 0 \neq x) \leftrightarrow ((φ \land x \in (A, B)) \to x \neq 0)$
48	23 47	mpbi	$⊢ (φ \land x \in (A, B)) \to x \neq 0$
49	48	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = 0$
50		velsn	$⊢ x \in \{0\} \leftrightarrow x = 0$
51	49 50	sylnibr	$⊢ (φ \land x \in (A, B)) \to \neg x \in \{0\}$
52	17 51	eldifd	$⊢ (φ \land x \in (A, B)) \to x \in (ℂ ∖ \{0\})$
53		logbval	$⊢ (2 \in (ℂ ∖ \{0, 1\}) \land x \in (ℂ ∖ \{0\})) \to \log_{2} x = \frac{\log x}{\log 2}$
54	45 52 53	syl2anc	$⊢ (φ \land x \in (A, B)) \to \log_{2} x = \frac{\log x}{\log 2}$
55	54	eleq1d	$⊢ (φ \land x \in (A, B)) \to (\log_{2} x \in ℂ \leftrightarrow \frac{\log x}{\log 2} \in ℂ)$
56	40 55	mpbird	$⊢ (φ \land x \in (A, B)) \to \log_{2} x \in ℂ$
57	34	a1i	$⊢ (φ \land x \in (A, B)) \to 2 \in ℝ^{+}$
58	57	relogcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℝ$
59	16 58	remulcld	$⊢ (φ \land x \in (A, B)) \to x \log 2 \in ℝ$
60	57	rpne0d	$⊢ (φ \land x \in (A, B)) \to 2 \neq 0$
61	26 60	logcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℂ$
62	17 61 24 39	mulne0d	$⊢ (φ \land x \in (A, B)) \to x \log 2 \neq 0$
63	41 59 62	redivcld	$⊢ (φ \land x \in (A, B)) \to \frac{1}{x \log 2} \in ℝ$
64		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
65	8	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
66	65	adantr	$⊢ (φ \land y \in ℂ) \to N \in ℕ_{0}$
67	64 66	expcld	$⊢ (φ \land y \in ℂ) \to y^{N} \in ℂ$
68	8	nncnd	$⊢ φ \to N \in ℂ$
69	68	adantr	$⊢ (φ \land y \in ℂ) \to N \in ℂ$
70		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
71	8 70	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
72	71	adantr	$⊢ (φ \land y \in ℂ) \to N - 1 \in ℕ_{0}$
73	64 72	expcld	$⊢ (φ \land y \in ℂ) \to y^{N - 1} \in ℂ$
74	69 73	mulcld	$⊢ (φ \land y \in ℂ) \to N y^{N - 1} \in ℂ$
75	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
76	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
77		0red	$⊢ φ \to 0 \in ℝ$
78	77 1 3	ltled	$⊢ φ \to 0 \leq A$
79		eqid	$⊢ (x \in (A, B) ⟼ \log_{2} x) = (x \in (A, B) ⟼ \log_{2} x)$
80		eqid	$⊢ (x \in (A, B) ⟼ \frac{1}{x \log 2}) = (x \in (A, B) ⟼ \frac{1}{x \log 2})$
81	75 76 78 4 79 80	dvrelog2b	$⊢ φ \to \frac{d (x \in (A, B)⟼ \log_{2} x)}{d_{ℝ} x} = (x \in (A, B) ⟼ \frac{1}{x \log 2})$
82		dvexp	$⊢ N \in ℕ \to \frac{d (y \in ℂ⟼ y^{N})}{d_{ℂ} y} = (y \in ℂ ⟼ N y^{N - 1})$
83	8 82	syl	$⊢ φ \to \frac{d (y \in ℂ⟼ y^{N})}{d_{ℂ} y} = (y \in ℂ ⟼ N y^{N - 1})$
84		oveq1	$⊢ y = \log_{2} x \to y^{N} = {\log_{2} x}^{N}$
85		oveq1	$⊢ y = \log_{2} x \to y^{N - 1} = {\log_{2} x}^{N - 1}$
86	85	oveq2d	$⊢ y = \log_{2} x \to N y^{N - 1} = N {\log_{2} x}^{N - 1}$
87	12 14 56 63 67 74 81 83 84 86	dvmptco	$⊢ φ \to \frac{d (x \in (A, B)⟼ {\log_{2} x}^{N})}{d_{ℝ} x} = (x \in (A, B) ⟼ N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2}))$
88	6	a1i	$⊢ φ \to G = (x \in (A, B) ⟼ C (\frac{{\log x}^{N - 1}}{x}))$
89	7	a1i	$⊢ (φ \land x \in (A, B)) \to C = \frac{N}{{\log 2}^{N}}$
90	89	oveq1d	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = (\frac{N}{{\log 2}^{N}}) (\frac{{\log x}^{N - 1}}{x})$
91	68	adantr	$⊢ (φ \land x \in (A, B)) \to N \in ℂ$
92	65	nn0zd	$⊢ φ \to N \in ℤ$
93	92	adantr	$⊢ (φ \land x \in (A, B)) \to N \in ℤ$
94	30 39 93	expclzd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} \in ℂ$
95	71	adantr	$⊢ (φ \land x \in (A, B)) \to N - 1 \in ℕ_{0}$
96	25 95	expcld	$⊢ (φ \land x \in (A, B)) \to {\log x}^{N - 1} \in ℂ$
97	30 39 93	expne0d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} \neq 0$
98	91 94 96 17 97 24	divmuldivd	$⊢ (φ \land x \in (A, B)) \to (\frac{N}{{\log 2}^{N}}) (\frac{{\log x}^{N - 1}}{x}) = \frac{N {\log x}^{N - 1}}{{\log 2}^{N} x}$
99	94 17	mulcomd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} x = x {\log 2}^{N}$
100		1cnd	$⊢ φ \to 1 \in ℂ$
101	100 68	pncan3d	$⊢ φ \to 1 + N - 1 = N$
102	101	eqcomd	$⊢ φ \to N = 1 + N - 1$
103	102	adantr	$⊢ (φ \land x \in (A, B)) \to N = 1 + N - 1$
104	103	oveq2d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} = {\log 2}^{1 + N - 1}$
105		1nn0	$⊢ 1 \in ℕ_{0}$
106	105	a1i	$⊢ (φ \land x \in (A, B)) \to 1 \in ℕ_{0}$
107	30 95 106	expaddd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{1 + N - 1} = {\log 2}^{1} {\log 2}^{N - 1}$
108	104 107	eqtrd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} = {\log 2}^{1} {\log 2}^{N - 1}$
109	30	exp1d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{1} = \log 2$
110	109	oveq1d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{1} {\log 2}^{N - 1} = \log 2 {\log 2}^{N - 1}$
111	108 110	eqtrd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} = \log 2 {\log 2}^{N - 1}$
112	111	oveq2d	$⊢ (φ \land x \in (A, B)) \to x {\log 2}^{N} = x \log 2 {\log 2}^{N - 1}$
113	99 112	eqtrd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} x = x \log 2 {\log 2}^{N - 1}$
114	30 95	expcld	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N - 1} \in ℂ$
115	17 30 114	mulassd	$⊢ (φ \land x \in (A, B)) \to x \log 2 {\log 2}^{N - 1} = x \log 2 {\log 2}^{N - 1}$
116	115	eqcomd	$⊢ (φ \land x \in (A, B)) \to x \log 2 {\log 2}^{N - 1} = x \log 2 {\log 2}^{N - 1}$
117	113 116	eqtrd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} x = x \log 2 {\log 2}^{N - 1}$
118	17 30	mulcld	$⊢ (φ \land x \in (A, B)) \to x \log 2 \in ℂ$
119	118 114	mulcomd	$⊢ (φ \land x \in (A, B)) \to x \log 2 {\log 2}^{N - 1} = {\log 2}^{N - 1} x \log 2$
120	117 119	eqtrd	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N} x = {\log 2}^{N - 1} x \log 2$
121	120	oveq2d	$⊢ (φ \land x \in (A, B)) \to \frac{N {\log x}^{N - 1}}{{\log 2}^{N} x} = \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1} x \log 2}$
122	98 121	eqtrd	$⊢ (φ \land x \in (A, B)) \to (\frac{N}{{\log 2}^{N}}) (\frac{{\log x}^{N - 1}}{x}) = \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1} x \log 2}$
123	90 122	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1} x \log 2}$
124	91 96	mulcld	$⊢ (φ \land x \in (A, B)) \to N {\log x}^{N - 1} \in ℂ$
125		1zzd	$⊢ (φ \land x \in (A, B)) \to 1 \in ℤ$
126	93 125	zsubcld	$⊢ (φ \land x \in (A, B)) \to N - 1 \in ℤ$
127	30 39 126	expne0d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{N - 1} \neq 0$
128	124 114 118 127 62	divdiv1d	$⊢ (φ \land x \in (A, B)) \to \frac{\frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1}}}{x \log 2} = \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1} x \log 2}$
129	128	eqcomd	$⊢ (φ \land x \in (A, B)) \to \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1} x \log 2} = \frac{\frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1}}}{x \log 2}$
130	123 129	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = \frac{\frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1}}}{x \log 2}$
131	91 96 114 127	divassd	$⊢ (φ \land x \in (A, B)) \to \frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1}} = N (\frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}})$
132	131	oveq1d	$⊢ (φ \land x \in (A, B)) \to \frac{\frac{N {\log x}^{N - 1}}{{\log 2}^{N - 1}}}{x \log 2} = \frac{N (\frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}})}{x \log 2}$
133	130 132	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = \frac{N (\frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}})}{x \log 2}$
134	25 30 39 95	expdivd	$⊢ (φ \land x \in (A, B)) \to {(\frac{\log x}{\log 2})}^{N - 1} = \frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}}$
135	134	eqcomd	$⊢ (φ \land x \in (A, B)) \to \frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}} = {(\frac{\log x}{\log 2})}^{N - 1}$
136	135	oveq2d	$⊢ (φ \land x \in (A, B)) \to N (\frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}}) = N {(\frac{\log x}{\log 2})}^{N - 1}$
137	136	oveq1d	$⊢ (φ \land x \in (A, B)) \to \frac{N (\frac{{\log x}^{N - 1}}{{\log 2}^{N - 1}})}{x \log 2} = \frac{N {(\frac{\log x}{\log 2})}^{N - 1}}{x \log 2}$
138	133 137	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = \frac{N {(\frac{\log x}{\log 2})}^{N - 1}}{x \log 2}$
139	54	oveq1d	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{N - 1} = {(\frac{\log x}{\log 2})}^{N - 1}$
140	139	oveq2d	$⊢ (φ \land x \in (A, B)) \to N {\log_{2} x}^{N - 1} = N {(\frac{\log x}{\log 2})}^{N - 1}$
141	140	oveq1d	$⊢ (φ \land x \in (A, B)) \to \frac{N {\log_{2} x}^{N - 1}}{x \log 2} = \frac{N {(\frac{\log x}{\log 2})}^{N - 1}}{x \log 2}$
142	141	eqcomd	$⊢ (φ \land x \in (A, B)) \to \frac{N {(\frac{\log x}{\log 2})}^{N - 1}}{x \log 2} = \frac{N {\log_{2} x}^{N - 1}}{x \log 2}$
143	138 142	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = \frac{N {\log_{2} x}^{N - 1}}{x \log 2}$
144	56 95	expcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{N - 1} \in ℂ$
145	91 144	mulcld	$⊢ (φ \land x \in (A, B)) \to N {\log_{2} x}^{N - 1} \in ℂ$
146	145 118 62	divrecd	$⊢ (φ \land x \in (A, B)) \to \frac{N {\log_{2} x}^{N - 1}}{x \log 2} = N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2})$
147	143 146	eqtrd	$⊢ (φ \land x \in (A, B)) \to C (\frac{{\log x}^{N - 1}}{x}) = N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2})$
148	147	mpteq2dva	$⊢ φ \to (x \in (A, B) ⟼ C (\frac{{\log x}^{N - 1}}{x})) = (x \in (A, B) ⟼ N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2}))$
149	88 148	eqtrd	$⊢ φ \to G = (x \in (A, B) ⟼ N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2}))$
150	149	eqcomd	$⊢ φ \to (x \in (A, B) ⟼ N {\log_{2} x}^{N - 1} (\frac{1}{x \log 2})) = G$
151	87 150	eqtrd	$⊢ φ \to \frac{d (x \in (A, B)⟼ {\log_{2} x}^{N})}{d_{ℝ} x} = G$
152	10 151	eqtrd	$⊢ φ \to ℝ D F = G$

Metamath Proof Explorer

Theorem dvrelogpow2b

Proof