aks4d1p1p6

Description: Inequality lift to differentiable functions for a term in AKS inequality lemma. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p6.1	$⊢ φ \to A \in ℝ$
	aks4d1p1p6.2	$⊢ φ \to B \in ℝ$
	aks4d1p1p6.3	$⊢ φ \to 3 \leq A$
	aks4d1p1p6.4	$⊢ φ \to A \leq B$
Assertion	aks4d1p1p6	$⊢ φ \to \frac{d (x \in (A, B)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (x \in (A, B) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p6.1	$⊢ φ \to A \in ℝ$
2		aks4d1p1p6.2	$⊢ φ \to B \in ℝ$
3		aks4d1p1p6.3	$⊢ φ \to 3 \leq A$
4		aks4d1p1p6.4	$⊢ φ \to A \leq B$
5		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
6	5	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
7		2cnd	$⊢ (φ \land x \in (A, B)) \to 2 \in ℂ$
8		2re	$⊢ 2 \in ℝ$
9	8	a1i	$⊢ (φ \land x \in (A, B)) \to 2 \in ℝ$
10		2pos	$⊢ 0 < 2$
11	10	a1i	$⊢ (φ \land x \in (A, B)) \to 0 < 2$
12		elioore	$⊢ x \in (A, B) \to x \in ℝ$
13	12	adantl	$⊢ (φ \land x \in (A, B)) \to x \in ℝ$
14		0red	$⊢ (φ \land x \in (A, B)) \to 0 \in ℝ$
15	1	adantr	$⊢ (φ \land x \in (A, B)) \to A \in ℝ$
16		3re	$⊢ 3 \in ℝ$
17	16	a1i	$⊢ (φ \land x \in (A, B)) \to 3 \in ℝ$
18		3pos	$⊢ 0 < 3$
19	18	a1i	$⊢ (φ \land x \in (A, B)) \to 0 < 3$
20	3	adantr	$⊢ (φ \land x \in (A, B)) \to 3 \leq A$
21	14 17 15 19 20	ltletrd	$⊢ (φ \land x \in (A, B)) \to 0 < A$
22		simpr	$⊢ (φ \land x \in (A, B)) \to x \in (A, B)$
23	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
24	23	adantr	$⊢ (φ \land x \in (A, B)) \to A \in ℝ^{*}$
25	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
26	25	adantr	$⊢ (φ \land x \in (A, B)) \to B \in ℝ^{*}$
27	13	rexrd	$⊢ (φ \land x \in (A, B)) \to x \in ℝ^{*}$
28		elioo5	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \to (x \in (A, B) \leftrightarrow (A < x \land x < B))$
29	24 26 27 28	syl3anc	$⊢ (φ \land x \in (A, B)) \to (x \in (A, B) \leftrightarrow (A < x \land x < B))$
30	22 29	mpbid	$⊢ (φ \land x \in (A, B)) \to (A < x \land x < B)$
31	30	simpld	$⊢ (φ \land x \in (A, B)) \to A < x$
32	14 15 13 21 31	lttrd	$⊢ (φ \land x \in (A, B)) \to 0 < x$
33		1red	$⊢ (φ \land x \in (A, B)) \to 1 \in ℝ$
34		1lt2	$⊢ 1 < 2$
35	34	a1i	$⊢ (φ \land x \in (A, B)) \to 1 < 2$
36	33 35	ltned	$⊢ (φ \land x \in (A, B)) \to 1 \neq 2$
37	36	necomd	$⊢ (φ \land x \in (A, B)) \to 2 \neq 1$
38	9 11 13 32 37	relogbcld	$⊢ (φ \land x \in (A, B)) \to \log_{2} x \in ℝ$
39		5nn0	$⊢ 5 \in ℕ_{0}$
40	39	a1i	$⊢ (φ \land x \in (A, B)) \to 5 \in ℕ_{0}$
41	38 40	reexpcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} \in ℝ$
42	41 33	readdcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} + 1 \in ℝ$
43	14 33	readdcld	$⊢ (φ \land x \in (A, B)) \to 0 + 1 \in ℝ$
44	14	ltp1d	$⊢ (φ \land x \in (A, B)) \to 0 < 0 + 1$
45	40	nn0zd	$⊢ (φ \land x \in (A, B)) \to 5 \in ℤ$
46		2cnd	$⊢ ⊤ \to 2 \in ℂ$
47		0red	$⊢ ⊤ \to 0 \in ℝ$
48	10	a1i	$⊢ ⊤ \to 0 < 2$
49	47 48	ltned	$⊢ ⊤ \to 0 \neq 2$
50	49	necomd	$⊢ ⊤ \to 2 \neq 0$
51		1red	$⊢ ⊤ \to 1 \in ℝ$
52	34	a1i	$⊢ ⊤ \to 1 < 2$
53	51 52	ltned	$⊢ ⊤ \to 1 \neq 2$
54	53	necomd	$⊢ ⊤ \to 2 \neq 1$
55		logb1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 1 = 0$
56	46 50 54 55	syl3anc	$⊢ ⊤ \to \log_{2} 1 = 0$
57	56	mptru	$⊢ \log_{2} 1 = 0$
58		2lt3	$⊢ 2 < 3$
59	58	a1i	$⊢ (φ \land x \in (A, B)) \to 2 < 3$
60	33 9 17 35 59	lttrd	$⊢ (φ \land x \in (A, B)) \to 1 < 3$
61	33 17 15 60 20	ltletrd	$⊢ (φ \land x \in (A, B)) \to 1 < A$
62	33 15 13 61 31	lttrd	$⊢ (φ \land x \in (A, B)) \to 1 < x$
63		2z	$⊢ 2 \in ℤ$
64	63	a1i	$⊢ (φ \land x \in (A, B)) \to 2 \in ℤ$
65	64	uzidd	$⊢ (φ \land x \in (A, B)) \to 2 \in ℤ_{\geq 2}$
66		1rp	$⊢ 1 \in ℝ^{+}$
67	66	a1i	$⊢ (φ \land x \in (A, B)) \to 1 \in ℝ^{+}$
68	13 32	elrpd	$⊢ (φ \land x \in (A, B)) \to x \in ℝ^{+}$
69		logblt	$⊢ (2 \in ℤ_{\geq 2} \land 1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 < x \leftrightarrow \log_{2} 1 < \log_{2} x)$
70	65 67 68 69	syl3anc	$⊢ (φ \land x \in (A, B)) \to (1 < x \leftrightarrow \log_{2} 1 < \log_{2} x)$
71	62 70	mpbid	$⊢ (φ \land x \in (A, B)) \to \log_{2} 1 < \log_{2} x$
72	57 71	eqbrtrrid	$⊢ (φ \land x \in (A, B)) \to 0 < \log_{2} x$
73		expgt0	$⊢ (\log_{2} x \in ℝ \land 5 \in ℤ \land 0 < \log_{2} x) \to 0 < {\log_{2} x}^{5}$
74	38 45 72 73	syl3anc	$⊢ (φ \land x \in (A, B)) \to 0 < {\log_{2} x}^{5}$
75	14 41 33 74	ltadd1dd	$⊢ (φ \land x \in (A, B)) \to 0 + 1 < {\log_{2} x}^{5} + 1$
76	14 43 42 44 75	lttrd	$⊢ (φ \land x \in (A, B)) \to 0 < {\log_{2} x}^{5} + 1$
77	9 11 42 76 37	relogbcld	$⊢ (φ \land x \in (A, B)) \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℝ$
78		recn	$⊢ \log_{2} ({\log_{2} x}^{5} + 1) \in ℝ \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℂ$
79	77 78	syl	$⊢ (φ \land x \in (A, B)) \to \log_{2} ({\log_{2} x}^{5} + 1) \in ℂ$
80	7 79	mulcld	$⊢ (φ \land x \in (A, B)) \to 2 \log_{2} ({\log_{2} x}^{5} + 1) \in ℂ$
81		2rp	$⊢ 2 \in ℝ^{+}$
82	81	a1i	$⊢ (φ \land x \in (A, B)) \to 2 \in ℝ^{+}$
83	82	relogcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℝ$
84	42 83	remulcld	$⊢ (φ \land x \in (A, B)) \to ({\log_{2} x}^{5} + 1) \log 2 \in ℝ$
85	41	recnd	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} \in ℂ$
86		1cnd	$⊢ (φ \land x \in (A, B)) \to 1 \in ℂ$
87	85 86	addcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} + 1 \in ℂ$
88	11	gt0ne0d	$⊢ (φ \land x \in (A, B)) \to 2 \neq 0$
89	7 88	logcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℂ$
90	76	gt0ne0d	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} + 1 \neq 0$
91		0red	$⊢ φ \to 0 \in ℝ$
92		loggt0b	$⊢ 2 \in ℝ^{+} \to (0 < \log 2 \leftrightarrow 1 < 2)$
93	81 92	ax-mp	$⊢ 0 < \log 2 \leftrightarrow 1 < 2$
94	34 93	mpbir	$⊢ 0 < \log 2$
95	94	a1i	$⊢ φ \to 0 < \log 2$
96	91 95	ltned	$⊢ φ \to 0 \neq \log 2$
97	96	necomd	$⊢ φ \to \log 2 \neq 0$
98	97	adantr	$⊢ (φ \land x \in (A, B)) \to \log 2 \neq 0$
99	87 89 90 98	mulne0d	$⊢ (φ \land x \in (A, B)) \to ({\log_{2} x}^{5} + 1) \log 2 \neq 0$
100	33 84 99	redivcld	$⊢ (φ \land x \in (A, B)) \to \frac{1}{({\log_{2} x}^{5} + 1) \log 2} \in ℝ$
101		5re	$⊢ 5 \in ℝ$
102	101	a1i	$⊢ (φ \land x \in (A, B)) \to 5 \in ℝ$
103		4nn0	$⊢ 4 \in ℕ_{0}$
104	103	a1i	$⊢ (φ \land x \in (A, B)) \to 4 \in ℕ_{0}$
105	38 104	reexpcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{4} \in ℝ$
106	102 105	remulcld	$⊢ (φ \land x \in (A, B)) \to 5 {\log_{2} x}^{4} \in ℝ$
107	13 83	remulcld	$⊢ (φ \land x \in (A, B)) \to x \log 2 \in ℝ$
108	13	recnd	$⊢ (φ \land x \in (A, B)) \to x \in ℂ$
109	14 32	gtned	$⊢ (φ \land x \in (A, B)) \to x \neq 0$
110	108 89 109 98	mulne0d	$⊢ (φ \land x \in (A, B)) \to x \log 2 \neq 0$
111	33 107 110	redivcld	$⊢ (φ \land x \in (A, B)) \to \frac{1}{x \log 2} \in ℝ$
112	106 111	remulcld	$⊢ (φ \land x \in (A, B)) \to 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) \in ℝ$
113	112 14	readdcld	$⊢ (φ \land x \in (A, B)) \to 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0 \in ℝ$
114	100 113	remulcld	$⊢ (φ \land x \in (A, B)) \to (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) \in ℝ$
115	9 114	remulcld	$⊢ (φ \land x \in (A, B)) \to 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) \in ℝ$
116	42 76	elrpd	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{5} + 1 \in ℝ^{+}$
117	8	a1i	$⊢ (φ \land y \in ℝ^{+}) \to 2 \in ℝ$
118	10	a1i	$⊢ (φ \land y \in ℝ^{+}) \to 0 < 2$
119		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
120	119	adantl	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ$
121		rpgt0	$⊢ y \in ℝ^{+} \to 0 < y$
122	121	adantl	$⊢ (φ \land y \in ℝ^{+}) \to 0 < y$
123		1red	$⊢ (φ \land y \in ℝ^{+}) \to 1 \in ℝ$
124	34	a1i	$⊢ (φ \land y \in ℝ^{+}) \to 1 < 2$
125	123 124	ltned	$⊢ (φ \land y \in ℝ^{+}) \to 1 \neq 2$
126	125	necomd	$⊢ (φ \land y \in ℝ^{+}) \to 2 \neq 1$
127	117 118 120 122 126	relogbcld	$⊢ (φ \land y \in ℝ^{+}) \to \log_{2} y \in ℝ$
128	127	recnd	$⊢ (φ \land y \in ℝ^{+}) \to \log_{2} y \in ℂ$
129	81	a1i	$⊢ (φ \land y \in ℝ^{+}) \to 2 \in ℝ^{+}$
130	129	relogcld	$⊢ (φ \land y \in ℝ^{+}) \to \log 2 \in ℝ$
131	120 130	remulcld	$⊢ (φ \land y \in ℝ^{+}) \to y \log 2 \in ℝ$
132	120	recnd	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℂ$
133		2cnd	$⊢ (φ \land y \in ℝ^{+}) \to 2 \in ℂ$
134	129	rpne0d	$⊢ (φ \land y \in ℝ^{+}) \to 2 \neq 0$
135	133 134	logcld	$⊢ (φ \land y \in ℝ^{+}) \to \log 2 \in ℂ$
136		rpne0	$⊢ y \in ℝ^{+} \to y \neq 0$
137	136	adantl	$⊢ (φ \land y \in ℝ^{+}) \to y \neq 0$
138	97	necomd	$⊢ φ \to 0 \neq \log 2$
139	138	adantr	$⊢ (φ \land y \in ℝ^{+}) \to 0 \neq \log 2$
140	139	necomd	$⊢ (φ \land y \in ℝ^{+}) \to \log 2 \neq 0$
141	132 135 137 140	mulne0d	$⊢ (φ \land y \in ℝ^{+}) \to y \log 2 \neq 0$
142	123 131 141	redivcld	$⊢ (φ \land y \in ℝ^{+}) \to \frac{1}{y \log 2} \in ℝ$
143		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
144	143	a1i	$⊢ φ \to ℂ \in \{ℝ, ℂ\}$
145	38	recnd	$⊢ (φ \land x \in (A, B)) \to \log_{2} x \in ℂ$
146		simpr	$⊢ (φ \land z \in ℂ) \to z \in ℂ$
147	39	a1i	$⊢ (φ \land z \in ℂ) \to 5 \in ℕ_{0}$
148	146 147	expcld	$⊢ (φ \land z \in ℂ) \to z^{5} \in ℂ$
149		5cn	$⊢ 5 \in ℂ$
150	149	a1i	$⊢ (φ \land z \in ℂ) \to 5 \in ℂ$
151	103	a1i	$⊢ (φ \land z \in ℂ) \to 4 \in ℕ_{0}$
152	146 151	expcld	$⊢ (φ \land z \in ℂ) \to z^{4} \in ℂ$
153	150 152	mulcld	$⊢ (φ \land z \in ℂ) \to 5 z^{4} \in ℂ$
154	16	a1i	$⊢ φ \to 3 \in ℝ$
155	18	a1i	$⊢ φ \to 0 < 3$
156	91 154 1 155 3	ltletrd	$⊢ φ \to 0 < A$
157	91 1 156	ltled	$⊢ φ \to 0 \leq A$
158		eqid	$⊢ (x \in (A, B) ⟼ \log_{2} x) = (x \in (A, B) ⟼ \log_{2} x)$
159		eqid	$⊢ (x \in (A, B) ⟼ \frac{1}{x \log 2}) = (x \in (A, B) ⟼ \frac{1}{x \log 2})$
160	23 25 157 4 158 159	dvrelog2b	$⊢ φ \to \frac{d (x \in (A, B)⟼ \log_{2} x)}{d_{ℝ} x} = (x \in (A, B) ⟼ \frac{1}{x \log 2})$
161		5nn	$⊢ 5 \in ℕ$
162		dvexp	$⊢ 5 \in ℕ \to \frac{d (z \in ℂ⟼ z^{5})}{d_{ℂ} z} = (z \in ℂ ⟼ 5 z^{5 - 1})$
163	161 162	ax-mp	$⊢ \frac{d (z \in ℂ⟼ z^{5})}{d_{ℂ} z} = (z \in ℂ ⟼ 5 z^{5 - 1})$
164		5m1e4	$⊢ 5 - 1 = 4$
165	164	a1i	$⊢ (φ \land z \in ℂ) \to 5 - 1 = 4$
166	165	oveq2d	$⊢ (φ \land z \in ℂ) \to z^{5 - 1} = z^{4}$
167	166	oveq2d	$⊢ (φ \land z \in ℂ) \to 5 z^{5 - 1} = 5 z^{4}$
168	167	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ 5 z^{5 - 1}) = (z \in ℂ ⟼ 5 z^{4})$
169	163 168	eqtrid	$⊢ φ \to \frac{d (z \in ℂ⟼ z^{5})}{d_{ℂ} z} = (z \in ℂ ⟼ 5 z^{4})$
170		oveq1	$⊢ z = \log_{2} x \to z^{5} = {\log_{2} x}^{5}$
171		oveq1	$⊢ z = \log_{2} x \to z^{4} = {\log_{2} x}^{4}$
172	171	oveq2d	$⊢ z = \log_{2} x \to 5 z^{4} = 5 {\log_{2} x}^{4}$
173	6 144 145 111 148 153 160 169 170 172	dvmptco	$⊢ φ \to \frac{d (x \in (A, B)⟼ {\log_{2} x}^{5})}{d_{ℝ} x} = (x \in (A, B) ⟼ 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}))$
174		1cnd	$⊢ φ \to 1 \in ℂ$
175	174	adantr	$⊢ (φ \land x \in ℝ) \to 1 \in ℂ$
176		0red	$⊢ (φ \land x \in ℝ) \to 0 \in ℝ$
177	6 174	dvmptc	$⊢ φ \to \frac{d (x \in ℝ⟼ 1)}{d_{ℝ} x} = (x \in ℝ ⟼ 0)$
178		ioossre	$⊢ (A, B) \subseteq ℝ$
179	178	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
180		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
181	180	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
182		iooretop	$⊢ (A, B) \in topGen (ran (.))$
183	182	a1i	$⊢ φ \to (A, B) \in topGen (ran (.))$
184	6 175 176 177 179 181 180 183	dvmptres	$⊢ φ \to \frac{d (x \in (A, B)⟼ 1)}{d_{ℝ} x} = (x \in (A, B) ⟼ 0)$
185	6 85 112 173 86 14 184	dvmptadd	$⊢ φ \to \frac{d (x \in (A, B)⟼ {\log_{2} x}^{5} + 1)}{d_{ℝ} x} = (x \in (A, B) ⟼ 5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0)$
186		dfrp2	$⊢ ℝ^{+} = (0, +∞)$
187	186	a1i	$⊢ φ \to ℝ^{+} = (0, +∞)$
188	187	mpteq1d	$⊢ φ \to (y \in ℝ^{+} ⟼ \log_{2} y) = (y \in (0, +∞) ⟼ \log_{2} y)$
189	188	oveq2d	$⊢ φ \to \frac{d (y \in ℝ^{+}⟼ \log_{2} y)}{d_{ℝ} y} = \frac{d (y \in (0, +∞)⟼ \log_{2} y)}{d_{ℝ} y}$
190	91	rexrd	$⊢ φ \to 0 \in ℝ^{*}$
191		pnfxr	$⊢ +∞ \in ℝ^{*}$
192	191	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
193	91	leidd	$⊢ φ \to 0 \leq 0$
194		0lepnf	$⊢ 0 \leq +∞$
195	194	a1i	$⊢ φ \to 0 \leq +∞$
196		eqid	$⊢ (y \in (0, +∞) ⟼ \log_{2} y) = (y \in (0, +∞) ⟼ \log_{2} y)$
197		eqid	$⊢ (y \in (0, +∞) ⟼ \frac{1}{y \log 2}) = (y \in (0, +∞) ⟼ \frac{1}{y \log 2})$
198	190 192 193 195 196 197	dvrelog2b	$⊢ φ \to \frac{d (y \in (0, +∞)⟼ \log_{2} y)}{d_{ℝ} y} = (y \in (0, +∞) ⟼ \frac{1}{y \log 2})$
199	187	eqcomd	$⊢ φ \to (0, +∞) = ℝ^{+}$
200	199	mpteq1d	$⊢ φ \to (y \in (0, +∞) ⟼ \frac{1}{y \log 2}) = (y \in ℝ^{+} ⟼ \frac{1}{y \log 2})$
201	198 200	eqtrd	$⊢ φ \to \frac{d (y \in (0, +∞)⟼ \log_{2} y)}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{1}{y \log 2})$
202	189 201	eqtrd	$⊢ φ \to \frac{d (y \in ℝ^{+}⟼ \log_{2} y)}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{1}{y \log 2})$
203		oveq2	$⊢ y = {\log_{2} x}^{5} + 1 \to \log_{2} y = \log_{2} ({\log_{2} x}^{5} + 1)$
204		oveq1	$⊢ y = {\log_{2} x}^{5} + 1 \to y \log 2 = ({\log_{2} x}^{5} + 1) \log 2$
205	204	oveq2d	$⊢ y = {\log_{2} x}^{5} + 1 \to \frac{1}{y \log 2} = \frac{1}{({\log_{2} x}^{5} + 1) \log 2}$
206	6 6 116 113 128 142 185 202 203 205	dvmptco	$⊢ φ \to \frac{d (x \in (A, B)⟼ \log_{2} ({\log_{2} x}^{5} + 1))}{d_{ℝ} x} = (x \in (A, B) ⟼ (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0))$
207	8	a1i	$⊢ φ \to 2 \in ℝ$
208	207	recnd	$⊢ φ \to 2 \in ℂ$
209	6 79 114 206 208	dvmptcmul	$⊢ φ \to \frac{d (x \in (A, B)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1))}{d_{ℝ} x} = (x \in (A, B) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0))$
210	145	sqcld	$⊢ (φ \land x \in (A, B)) \to {\log_{2} x}^{2} \in ℂ$
211	83	resqcld	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{2} \in ℝ$
212	82	rpne0d	$⊢ (φ \land x \in (A, B)) \to 2 \neq 0$
213	7 212	logcld	$⊢ (φ \land x \in (A, B)) \to \log 2 \in ℂ$
214	213 98 64	expne0d	$⊢ (φ \land x \in (A, B)) \to {\log 2}^{2} \neq 0$
215	9 211 214	redivcld	$⊢ (φ \land x \in (A, B)) \to \frac{2}{{\log 2}^{2}} \in ℝ$
216	68	relogcld	$⊢ (φ \land x \in (A, B)) \to \log x \in ℝ$
217		2m1e1	$⊢ 2 - 1 = 1$
218		1nn0	$⊢ 1 \in ℕ_{0}$
219	217 218	eqeltri	$⊢ 2 - 1 \in ℕ_{0}$
220	219	a1i	$⊢ (φ \land x \in (A, B)) \to 2 - 1 \in ℕ_{0}$
221	216 220	reexpcld	$⊢ (φ \land x \in (A, B)) \to {\log x}^{2 - 1} \in ℝ$
222	68	rpne0d	$⊢ (φ \land x \in (A, B)) \to x \neq 0$
223	221 13 222	redivcld	$⊢ (φ \land x \in (A, B)) \to \frac{{\log x}^{2 - 1}}{x} \in ℝ$
224	215 223	remulcld	$⊢ (φ \land x \in (A, B)) \to (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}) \in ℝ$
225		eqid	$⊢ (x \in (A, B) ⟼ {\log_{2} x}^{2}) = (x \in (A, B) ⟼ {\log_{2} x}^{2})$
226		eqid	$⊢ (x \in (A, B) ⟼ (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x})) = (x \in (A, B) ⟼ (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$
227		eqid	$⊢ \frac{2}{{\log 2}^{2}} = \frac{2}{{\log 2}^{2}}$
228		2nn	$⊢ 2 \in ℕ$
229	228	a1i	$⊢ φ \to 2 \in ℕ$
230	1 2 156 4 225 226 227 229	dvrelogpow2b	$⊢ φ \to \frac{d (x \in (A, B)⟼ {\log_{2} x}^{2})}{d_{ℝ} x} = (x \in (A, B) ⟼ (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$
231	6 80 115 209 210 224 230	dvmptadd	$⊢ φ \to \frac{d (x \in (A, B)⟼ 2 \log_{2} ({\log_{2} x}^{5} + 1) + {\log_{2} x}^{2})}{d_{ℝ} x} = (x \in (A, B) ⟼ 2 (\frac{1}{({\log_{2} x}^{5} + 1) \log 2}) (5 {\log_{2} x}^{4} (\frac{1}{x \log 2}) + 0) + (\frac{2}{{\log 2}^{2}}) (\frac{{\log x}^{2 - 1}}{x}))$

Metamath Proof Explorer

Theorem aks4d1p1p6

Proof