Theorem dvrelogpow2b

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

	Ref	Expression
Hypotheses	dvrelogpow2b.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	dvrelogpow2b.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	dvrelogpow2b.3	⊢ ( 𝜑 → 0 < 𝐴 )
	dvrelogpow2b.4	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	dvrelogpow2b.5	⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 logb 𝑥 ) ↑ 𝑁 ) )
	dvrelogpow2b.6	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐶 · ( ( ( log ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) / 𝑥 ) ) )
	dvrelogpow2b.7	⊢ 𝐶 = ( 𝑁 / ( ( log ‘ 2 ) ↑ 𝑁 ) )
	dvrelogpow2b.8	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	dvrelogpow2b	⊢ ( 𝜑 → ( ℝ D 𝐹 ) = 𝐺 )

Proof

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