Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
aks4d1p1p6.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
aks4d1p1p6.3 ⊢ ( 𝜑 → 3 ≤ 𝐴 )
aks4d1p1p6.4 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion aks4d1p1p6 ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( 2 logb ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) ) ) + ( ( 2 logb 𝑥 ) ↑ 2 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝑥 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝑥 ) ↑ 4 ) ) · ( 1 / ( 𝑥 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝑥 ) ↑ ( 2 − 1 ) ) / 𝑥 ) ) ) ) )

Proof

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