Metamath Proof Explorer

Theorem aks4d1p1p7

Description: Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p7.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
aks4d1p1p7.2 ⊢ ( 𝜑 → 4 ≤ 𝐴 )
Assertion aks4d1p1p7 ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) / 𝐴 ) ) ) ≤ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p7.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 aks4d1p1p7.2 ⊢ ( 𝜑 → 4 ≤ 𝐴 )
3 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
5 4re ⊢ 4 ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
7 4pos ⊢ 0 < 4
8 7 a1i ⊢ ( 𝜑 → 0 < 4 )
9 4 6 1 8 2 ltletrd ⊢ ( 𝜑 → 0 < 𝐴 )
10 4 9 ltned ⊢ ( 𝜑 → 0 ≠ 𝐴 )
11 10 necomd ⊢ ( 𝜑 → 𝐴 ≠ 0 )
12 3 11 logcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
13 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
14 2pos ⊢ 0 < 2
15 14 a1i ⊢ ( 𝜑 → 0 < 2 )
16 4 15 ltned ⊢ ( 𝜑 → 0 ≠ 2 )
17 16 necomd ⊢ ( 𝜑 → 2 ≠ 0 )
18 13 17 logcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
19 1lt2 ⊢ 1 < 2
20 2rp ⊢ 2 ∈ ℝ+
21 loggt0b ⊢ ( 2 ∈ ℝ+ → ( 0 < ( log ‘ 2 ) ↔ 1 < 2 ) )
22 20 21 ax-mp ⊢ ( 0 < ( log ‘ 2 ) ↔ 1 < 2 )
23 19 22 mpbir ⊢ 0 < ( log ‘ 2 )
24 23 a1i ⊢ ( 𝜑 → 0 < ( log ‘ 2 ) )
25 4 24 ltned ⊢ ( 𝜑 → 0 ≠ ( log ‘ 2 ) )
26 25 necomd ⊢ ( 𝜑 → ( log ‘ 2 ) ≠ 0 )
27 5nn0 ⊢ 5 ∈ ℕ0
28 27 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
29 12 18 26 28 expdivd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) = ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) )
30 29 oveq1d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) = ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) )
31 30 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) = ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) )
32 31 oveq2d ⊢ ( 𝜑 → ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) = ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) )
33 32 oveq1d ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
34 33 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
35 34 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) = ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) )
36 2re ⊢ 2 ∈ ℝ
37 36 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
38 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
39 1 9 elrpd ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
40 39 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
41 40 28 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 5 ) ∈ ℝ )
42 20 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
43 42 relogcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
44 43 28 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) ∈ ℝ )
45 28 nn0zd ⊢ ( 𝜑 → 5 ∈ ℤ )
46 18 26 45 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) ≠ 0 )
47 41 44 46 redivcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℝ )
48 47 38 readdcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) ∈ ℝ )
49 48 43 remulcld ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ∈ ℝ )
50 12 28 expcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 5 ) ∈ ℂ )
51 18 28 expcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) ∈ ℂ )
52 50 51 46 divcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℂ )
53 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
54 52 53 addcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) ∈ ℂ )
55 19 a1i ⊢ ( 𝜑 → 1 < 2 )
56 37 55 rplogcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ+ )
57 56 45 rpexpcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) ∈ ℝ+ )
58 1re ⊢ 1 ∈ ℝ
59 3nn0 ⊢ 3 ∈ ℕ0
60 58 59 nn0addge2i ⊢ 1 ≤ ( 3 + 1 )
61 60 a1i ⊢ ( 𝜑 → 1 ≤ ( 3 + 1 ) )
62 df-4 ⊢ 4 = ( 3 + 1 )
63 61 62 breqtrrdi ⊢ ( 𝜑 → 1 ≤ 4 )
64 38 6 1 63 2 letrd ⊢ ( 𝜑 → 1 ≤ 𝐴 )
65 1 64 logge0d ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝐴 ) )
66 40 28 65 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( log ‘ 𝐴 ) ↑ 5 ) )
67 41 57 66 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) )
68 47 ltp1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) < ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) )
69 4 47 48 67 68 lelttrd ⊢ ( 𝜑 → 0 < ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) )
70 4 69 ltned ⊢ ( 𝜑 → 0 ≠ ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) )
71 70 necomd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) ≠ 0 )
72 54 18 71 26 mulne0d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ≠ 0 )
73 38 49 72 redivcld ⊢ ( 𝜑 → ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) ∈ ℝ )
74 5re ⊢ 5 ∈ ℝ
75 74 a1i ⊢ ( 𝜑 → 5 ∈ ℝ )
76 4nn0 ⊢ 4 ∈ ℕ0
77 76 a1i ⊢ ( 𝜑 → 4 ∈ ℕ0 )
78 40 77 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 4 ) ∈ ℝ )
79 75 78 remulcld ⊢ ( 𝜑 → ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ∈ ℝ )
80 44 1 remulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ∈ ℝ )
81 51 3 46 11 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ≠ 0 )
82 79 80 81 redivcld ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ∈ ℝ )
83 73 82 remulcld ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ∈ ℝ )
84 37 83 remulcld ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) ∈ ℝ )
85 43 resqcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 2 ) ∈ ℝ )
86 2z ⊢ 2 ∈ ℤ
87 86 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
88 18 26 87 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 2 ) ≠ 0 )
89 37 85 88 redivcld ⊢ ( 𝜑 → ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
90 1nn0 ⊢ 1 ∈ ℕ0
91 90 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
92 40 91 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 1 ) ∈ ℝ )
93 92 1 11 redivcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ∈ ℝ )
94 89 93 remulcld ⊢ ( 𝜑 → ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ∈ ℝ )
95 84 94 readdcld ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ∈ ℝ )
96 47 43 remulcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ∈ ℝ )
97 1lt4 ⊢ 1 < 4
98 97 a1i ⊢ ( 𝜑 → 1 < 4 )
99 38 6 1 98 2 ltletrd ⊢ ( 𝜑 → 1 < 𝐴 )
100 loggt0b ⊢ ( 𝐴 ∈ ℝ+ → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) )
101 39 100 syl ⊢ ( 𝜑 → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) )
102 99 101 mpbird ⊢ ( 𝜑 → 0 < ( log ‘ 𝐴 ) )
103 4 102 ltned ⊢ ( 𝜑 → 0 ≠ ( log ‘ 𝐴 ) )
104 103 necomd ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ≠ 0 )
105 12 104 45 expne0d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 5 ) ≠ 0 )
106 50 51 105 46 divne0d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) ≠ 0 )
107 52 18 106 26 mulne0d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ≠ 0 )
108 38 96 107 redivcld ⊢ ( 𝜑 → ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) ∈ ℝ )
109 108 82 remulcld ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ∈ ℝ )
110 37 109 remulcld ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) ∈ ℝ )
111 110 94 readdcld ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ∈ ℝ )
112 59 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
113 40 112 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 3 ) ∈ ℝ )
114 6 113 remulcld ⊢ ( 𝜑 → ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) ∈ ℝ )
115 43 77 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) ∈ ℝ )
116 115 1 remulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ∈ ℝ )
117 18 77 expcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) ∈ ℂ )
118 4z ⊢ 4 ∈ ℤ
119 118 a1i ⊢ ( 𝜑 → 4 ∈ ℤ )
120 18 26 119 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) ≠ 0 )
121 117 3 120 11 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ≠ 0 )
122 114 116 121 redivcld ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ∈ ℝ )
123 0le2 ⊢ 0 ≤ 2
124 123 a1i ⊢ ( 𝜑 → 0 ≤ 2 )
125 57 39 rpmulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ∈ ℝ+ )
126 28 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 5 )
127 40 77 65 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( log ‘ 𝐴 ) ↑ 4 ) )
128 75 78 126 127 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) )
129 79 125 128 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) )
130 1 99 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ+ )
131 130 45 rpexpcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 5 ) ∈ ℝ+ )
132 131 57 rpdivcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℝ+ )
133 132 56 rpmulcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ∈ ℝ+ )
134 24 22 sylib ⊢ ( 𝜑 → 1 < 2 )
135 37 134 rplogcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ+ )
136 135 45 rpexpcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) ∈ ℝ+ )
137 41 136 66 divge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) )
138 47 137 ge0p1rpd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) ∈ ℝ+ )
139 138 135 rpmulcld ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ∈ ℝ+ )
140 0le1 ⊢ 0 ≤ 1
141 140 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
142 135 rpred ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
143 135 rpge0d ⊢ ( 𝜑 → 0 ≤ ( log ‘ 2 ) )
144 47 lep1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) ≤ ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) )
145 47 48 142 143 144 lemul1ad ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ≤ ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) )
146 133 139 38 141 145 lediv2ad ⊢ ( 𝜑 → ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) ≤ ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) )
147 73 108 82 129 146 lemul1ad ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ≤ ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
148 83 109 37 124 147 lemul2ad ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) ≤ ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
149 84 110 94 148 leadd1dd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ≤ ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) )
150 50 18 51 46 div23d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) = ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) )
151 150 eqcomd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) = ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) )
152 151 oveq2d ⊢ ( 𝜑 → ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) = ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) )
153 152 oveq1d ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
154 153 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
155 18 sqcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 2 ) ∈ ℂ )
156 12 91 expcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 1 ) ∈ ℂ )
157 13 155 156 3 88 11 divmuldivd ⊢ ( 𝜑 → ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) )
158 154 157 oveq12d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) = ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
159 50 18 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ∈ ℂ )
160 50 18 105 26 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ≠ 0 )
161 53 159 51 160 46 divdiv2d ⊢ ( 𝜑 → ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) = ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) )
162 161 oveq1d ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
163 162 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( 2 · ( ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
164 53 51 mulcld ⊢ ( 𝜑 → ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℂ )
165 164 159 160 divcld ⊢ ( 𝜑 → ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ∈ ℂ )
166 82 recnd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ∈ ℂ )
167 13 165 166 mulassd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( 2 · ( ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
168 167 eqcomd ⊢ ( 𝜑 → ( 2 · ( ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
169 163 168 eqtrd ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
170 169 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
171 13 164 159 160 divassd ⊢ ( 𝜑 → ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) = ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) )
172 171 eqcomd ⊢ ( 𝜑 → ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) = ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) )
173 172 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
174 173 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
175 13 53 51 mulassd ⊢ ( 𝜑 → ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) = ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) )
176 175 eqcomd ⊢ ( 𝜑 → ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) = ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) )
177 176 oveq1d ⊢ ( 𝜑 → ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) = ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) )
178 177 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
179 178 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
180 13 mulid1d ⊢ ( 𝜑 → ( 2 · 1 ) = 2 )
181 180 oveq1d ⊢ ( 𝜑 → ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) = ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) )
182 181 oveq1d ⊢ ( 𝜑 → ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) = ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) )
183 182 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
184 183 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
185 13 51 mulcld ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℂ )
186 79 recnd ⊢ ( 𝜑 → ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ∈ ℂ )
187 51 3 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ∈ ℂ )
188 185 159 186 187 160 81 divmuldivd ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
189 188 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
190 50 18 187 mulassd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
191 190 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
192 191 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
193 185 186 mulcomd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) = ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) )
194 18 51 3 mulassd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) = ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) )
195 194 eqcomd ⊢ ( 𝜑 → ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) )
196 195 oveq2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) )
197 193 196 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) )
198 197 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
199 18 51 mulcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) ∈ ℂ )
200 199 3 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ∈ ℂ )
201 18 51 26 46 mulne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) ≠ 0 )
202 199 3 201 11 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ≠ 0 )
203 186 50 185 200 105 202 divmuldivd ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) )
204 203 eqcomd ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) )
205 204 oveq1d ⊢ ( 𝜑 → ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
206 75 recnd ⊢ ( 𝜑 → 5 ∈ ℂ )
207 78 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 4 ) ∈ ℂ )
208 206 207 50 105 divassd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) = ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) )
209 194 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) = ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
210 208 209 oveq12d ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) = ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
211 210 oveq1d ⊢ ( 𝜑 → ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
212 77 nn0zd ⊢ ( 𝜑 → 4 ∈ ℤ )
213 12 104 45 212 expsubd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ ( 4 − 5 ) ) = ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) )
214 213 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) = ( ( log ‘ 𝐴 ) ↑ ( 4 − 5 ) ) )
215 4p1e5 ⊢ ( 4 + 1 ) = 5
216 74 recni ⊢ 5 ∈ ℂ
217 5 recni ⊢ 4 ∈ ℂ
218 ax-1cn ⊢ 1 ∈ ℂ
219 216 217 218 subaddi ⊢ ( ( 5 − 4 ) = 1 ↔ ( 4 + 1 ) = 5 )
220 215 219 mpbir ⊢ ( 5 − 4 ) = 1
221 220 a1i ⊢ ( 𝜑 → ( 5 − 4 ) = 1 )
222 53 subid1d ⊢ ( 𝜑 → ( 1 − 0 ) = 1 )
223 221 222 eqtr4d ⊢ ( 𝜑 → ( 5 − 4 ) = ( 1 − 0 ) )
224 206 217 jctir ⊢ ( 𝜑 → ( 5 ∈ ℂ ∧ 4 ∈ ℂ ) )
225 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
226 53 225 jca ⊢ ( 𝜑 → ( 1 ∈ ℂ ∧ 0 ∈ ℂ ) )
227 subeqrev ⊢ ( ( ( 5 ∈ ℂ ∧ 4 ∈ ℂ ) ∧ ( 1 ∈ ℂ ∧ 0 ∈ ℂ ) ) → ( ( 5 − 4 ) = ( 1 − 0 ) ↔ ( 4 − 5 ) = ( 0 − 1 ) ) )
228 224 226 227 syl2anc ⊢ ( 𝜑 → ( ( 5 − 4 ) = ( 1 − 0 ) ↔ ( 4 − 5 ) = ( 0 − 1 ) ) )
229 223 228 mpbid ⊢ ( 𝜑 → ( 4 − 5 ) = ( 0 − 1 ) )
230 df-neg ⊢ - 1 = ( 0 − 1 )
231 229 230 eqtr4di ⊢ ( 𝜑 → ( 4 − 5 ) = - 1 )
232 231 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ ( 4 − 5 ) ) = ( ( log ‘ 𝐴 ) ↑ - 1 ) )
233 214 232 eqtrd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) = ( ( log ‘ 𝐴 ) ↑ - 1 ) )
234 233 oveq2d ⊢ ( 𝜑 → ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) = ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) )
235 13 18 51 187 26 81 divmuldivd ⊢ ( 𝜑 → ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
236 235 eqcomd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) )
237 234 236 oveq12d ⊢ ( 𝜑 → ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) )
238 237 oveq1d ⊢ ( 𝜑 → ( ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
239 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
240 12 104 239 expnegd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ - 1 ) = ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) )
241 240 oveq2d ⊢ ( 𝜑 → ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) = ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) )
242 51 51 3 46 11 divdiv1d ⊢ ( 𝜑 → ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) = ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) )
243 242 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) )
244 243 oveq2d ⊢ ( 𝜑 → ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) )
245 241 244 oveq12d ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) ) )
246 245 oveq1d ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
247 12 104 239 expne0d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 1 ) ≠ 0 )
248 206 53 156 247 divassd ⊢ ( 𝜑 → ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) = ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) )
249 248 eqcomd ⊢ ( 𝜑 → ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) = ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) )
250 51 46 dividd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) = 1 )
251 250 oveq1d ⊢ ( 𝜑 → ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) = ( 1 / 𝐴 ) )
252 251 oveq2d ⊢ ( 𝜑 → ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) = ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) )
253 249 252 oveq12d ⊢ ( 𝜑 → ( ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) ) = ( ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) ) )
254 253 oveq1d ⊢ ( 𝜑 → ( ( ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
255 206 mulid1d ⊢ ( 𝜑 → ( 5 · 1 ) = 5 )
256 255 oveq1d ⊢ ( 𝜑 → ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) = ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) )
257 13 18 53 3 26 11 divmuldivd ⊢ ( 𝜑 → ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) = ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) )
258 256 257 oveq12d ⊢ ( 𝜑 → ( ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) ) = ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) )
259 258 oveq1d ⊢ ( 𝜑 → ( ( ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
260 180 13 eqeltrd ⊢ ( 𝜑 → ( 2 · 1 ) ∈ ℂ )
261 18 3 mulcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) · 𝐴 ) ∈ ℂ )
262 18 3 26 11 mulne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) · 𝐴 ) ≠ 0 )
263 206 156 260 261 247 262 divmuldivd ⊢ ( 𝜑 → ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) = ( ( 5 · ( 2 · 1 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) )
264 180 oveq2d ⊢ ( 𝜑 → ( 5 · ( 2 · 1 ) ) = ( 5 · 2 ) )
265 264 oveq1d ⊢ ( 𝜑 → ( ( 5 · ( 2 · 1 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) = ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) )
266 263 265 eqtrd ⊢ ( 𝜑 → ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) = ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) )
267 266 oveq1d ⊢ ( 𝜑 → ( ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
268 5t2e10 ⊢ ( 5 · 2 ) = 1 0
269 268 a1i ⊢ ( 𝜑 → ( 5 · 2 ) = 1 0 )
270 269 oveq1d ⊢ ( 𝜑 → ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) = ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) )
271 270 oveq1d ⊢ ( 𝜑 → ( ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
272 10nn0 ⊢ 1 0 ∈ ℕ0
273 272 nn0cni ⊢ 1 0 ∈ ℂ
274 273 a1i ⊢ ( 𝜑 → 1 0 ∈ ℂ )
275 274 mulid1d ⊢ ( 𝜑 → ( 1 0 · 1 ) = 1 0 )
276 275 oveq1d ⊢ ( 𝜑 → ( ( 1 0 · 1 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) )
277 13 156 mulcld ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) ∈ ℂ )
278 277 155 88 divcld ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ∈ ℂ )
279 278 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) )
280 276 279 oveq12d ⊢ ( 𝜑 → ( ( ( 1 0 · 1 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( 1 · ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) = ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
281 18 91 expcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 1 ) ∈ ℂ )
282 18 26 239 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 1 ) ≠ 0 )
283 277 281 282 divcld ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) ∈ ℂ )
284 283 mulid1d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
285 284 oveq2d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) )
286 10re ⊢ 1 0 ∈ ℝ
287 286 a1i ⊢ ( 𝜑 → 1 0 ∈ ℝ )
288 287 40 104 redivcld ⊢ ( 𝜑 → ( 1 0 / ( log ‘ 𝐴 ) ) ∈ ℝ )
289 40 43 26 redivcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ∈ ℝ )
290 289 91 reexpcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ∈ ℝ )
291 37 290 remulcld ⊢ ( 𝜑 → ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ∈ ℝ )
292 288 291 readdcld ⊢ ( 𝜑 → ( ( 1 0 / ( log ‘ 𝐴 ) ) + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) ∈ ℝ )
293 287 291 readdcld ⊢ ( 𝜑 → ( 1 0 + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) ∈ ℝ )
294 43 112 reexpcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 3 ) ∈ ℝ )
295 3z ⊢ 3 ∈ ℤ
296 295 a1i ⊢ ( 𝜑 → 3 ∈ ℤ )
297 18 26 296 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 3 ) ≠ 0 )
298 113 294 297 redivcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ∈ ℝ )
299 6 298 remulcld ⊢ ( 𝜑 → ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) ∈ ℝ )
300 ere ⊢ e ∈ ℝ
301 300 a1i ⊢ ( 𝜑 → e ∈ ℝ )
302 112 nn0red ⊢ ( 𝜑 → 3 ∈ ℝ )
303 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
304 303 simpri ⊢ e < 3
305 304 a1i ⊢ ( 𝜑 → e < 3 )
306 3lt4 ⊢ 3 < 4
307 306 a1i ⊢ ( 𝜑 → 3 < 4 )
308 302 6 1 307 2 ltletrd ⊢ ( 𝜑 → 3 < 𝐴 )
309 301 302 1 305 308 lttrd ⊢ ( 𝜑 → e < 𝐴 )
310 301 1 309 ltled ⊢ ( 𝜑 → e ≤ 𝐴 )
311 301 1 lenltd ⊢ ( 𝜑 → ( e ≤ 𝐴 ↔ ¬ 𝐴 < e ) )
312 310 311 mpbid ⊢ ( 𝜑 → ¬ 𝐴 < e )
313 loglt1b ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) < 1 ↔ 𝐴 < e ) )
314 39 313 syl ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) < 1 ↔ 𝐴 < e ) )
315 312 314 mtbird ⊢ ( 𝜑 → ¬ ( log ‘ 𝐴 ) < 1 )
316 38 40 lenltd ⊢ ( 𝜑 → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ¬ ( log ‘ 𝐴 ) < 1 ) )
317 315 316 mpbird ⊢ ( 𝜑 → 1 ≤ ( log ‘ 𝐴 ) )
318 10nn ⊢ 1 0 ∈ ℕ
319 318 a1i ⊢ ( 𝜑 → 1 0 ∈ ℕ )
320 nnledivrp ⊢ ( ( 1 0 ∈ ℕ ∧ ( log ‘ 𝐴 ) ∈ ℝ+ ) → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( 1 0 / ( log ‘ 𝐴 ) ) ≤ 1 0 ) )
321 319 130 320 syl2anc ⊢ ( 𝜑 → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( 1 0 / ( log ‘ 𝐴 ) ) ≤ 1 0 ) )
322 317 321 mpbid ⊢ ( 𝜑 → ( 1 0 / ( log ‘ 𝐴 ) ) ≤ 1 0 )
323 288 287 291 322 leadd1dd ⊢ ( 𝜑 → ( ( 1 0 / ( log ‘ 𝐴 ) ) + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) ≤ ( 1 0 + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) )
324 38 55 gtned ⊢ ( 𝜑 → 2 ≠ 1 )
325 37 15 1 9 324 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐴 ) ∈ ℝ )
326 325 91 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) ∈ ℝ )
327 42 55 jca ⊢ ( 𝜑 → ( 2 ∈ ℝ+ ∧ 1 < 2 ) )
328 logbgt0b ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 < 2 ) ) → ( 0 < ( 2 logb 𝐴 ) ↔ 1 < 𝐴 ) )
329 39 327 328 syl2anc ⊢ ( 𝜑 → ( 0 < ( 2 logb 𝐴 ) ↔ 1 < 𝐴 ) )
330 99 329 mpbird ⊢ ( 𝜑 → 0 < ( 2 logb 𝐴 ) )
331 325 330 elrpd ⊢ ( 𝜑 → ( 2 logb 𝐴 ) ∈ ℝ+ )
332 331 239 rpexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) ∈ ℝ+ )
333 332 rpne0d ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) ≠ 0 )
334 287 326 333 redivcld ⊢ ( 𝜑 → ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ∈ ℝ )
335 334 37 readdcld ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) ∈ ℝ )
336 sq2 ⊢ ( 2 ↑ 2 ) = 4
337 336 a1i ⊢ ( 𝜑 → ( 2 ↑ 2 ) = 4 )
338 337 6 eqeltrd ⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℝ )
339 6 338 remulcld ⊢ ( 𝜑 → ( 4 · ( 2 ↑ 2 ) ) ∈ ℝ )
340 325 resqcld ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 2 ) ∈ ℝ )
341 6 340 remulcld ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) ∈ ℝ )
342 325 recnd ⊢ ( 𝜑 → ( 2 logb 𝐴 ) ∈ ℂ )
343 342 exp1d ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) = ( 2 logb 𝐴 ) )
344 343 oveq2d ⊢ ( 𝜑 → ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( 1 0 / ( 2 logb 𝐴 ) ) )
345 344 oveq1d ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) = ( ( 1 0 / ( 2 logb 𝐴 ) ) + 2 ) )
346 345 335 eqeltrrd ⊢ ( 𝜑 → ( ( 1 0 / ( 2 logb 𝐴 ) ) + 2 ) ∈ ℝ )
347 287 rehalfcld ⊢ ( 𝜑 → ( 1 0 / 2 ) ∈ ℝ )
348 347 37 readdcld ⊢ ( 𝜑 → ( ( 1 0 / 2 ) + 2 ) ∈ ℝ )
349 344 334 eqeltrrd ⊢ ( 𝜑 → ( 1 0 / ( 2 logb 𝐴 ) ) ∈ ℝ )
350 287 37 17 redivcld ⊢ ( 𝜑 → ( 1 0 / 2 ) ∈ ℝ )
351 272 nn0ge0i ⊢ 0 ≤ 1 0
352 351 a1i ⊢ ( 𝜑 → 0 ≤ 1 0 )
353 42 324 87 relogbexpd ⊢ ( 𝜑 → ( 2 logb ( 2 ↑ 2 ) ) = 2 )
354 353 eqcomd ⊢ ( 𝜑 → 2 = ( 2 logb ( 2 ↑ 2 ) ) )
355 337 oveq2d ⊢ ( 𝜑 → ( 2 logb ( 2 ↑ 2 ) ) = ( 2 logb 4 ) )
356 354 355 eqtrd ⊢ ( 𝜑 → 2 = ( 2 logb 4 ) )
357 37 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
358 87 357 6 8 1 9 2 logblebd ⊢ ( 𝜑 → ( 2 logb 4 ) ≤ ( 2 logb 𝐴 ) )
359 356 358 eqbrtrd ⊢ ( 𝜑 → 2 ≤ ( 2 logb 𝐴 ) )
360 42 331 287 352 359 lediv2ad ⊢ ( 𝜑 → ( 1 0 / ( 2 logb 𝐴 ) ) ≤ ( 1 0 / 2 ) )
361 349 350 37 360 leadd1dd ⊢ ( 𝜑 → ( ( 1 0 / ( 2 logb 𝐴 ) ) + 2 ) ≤ ( ( 1 0 / 2 ) + 2 ) )
362 1nn ⊢ 1 ∈ ℕ
363 6nn0 ⊢ 6 ∈ ℕ0
364 2nn0 ⊢ 2 ∈ ℕ0
365 27 364 nn0addcli ⊢ ( 5 + 2 ) ∈ ℕ0
366 5p2e7 ⊢ ( 5 + 2 ) = 7
367 7re ⊢ 7 ∈ ℝ
368 367 364 nn0addge1i ⊢ 7 ≤ ( 7 + 2 )
369 7p2e9 ⊢ ( 7 + 2 ) = 9
370 368 369 breqtri ⊢ 7 ≤ 9
371 366 370 eqbrtri ⊢ ( 5 + 2 ) ≤ 9
372 362 363 365 371 declei ⊢ ( 5 + 2 ) ≤ 1 6
373 372 a1i ⊢ ( 𝜑 → ( 5 + 2 ) ≤ 1 6 )
374 206 13 274 17 ldiv ⊢ ( 𝜑 → ( ( 5 · 2 ) = 1 0 ↔ 5 = ( 1 0 / 2 ) ) )
375 269 374 mpbid ⊢ ( 𝜑 → 5 = ( 1 0 / 2 ) )
376 375 oveq1d ⊢ ( 𝜑 → ( 5 + 2 ) = ( ( 1 0 / 2 ) + 2 ) )
377 4t4e16 ⊢ ( 4 · 4 ) = 1 6
378 377 eqcomi ⊢ 1 6 = ( 4 · 4 )
379 378 a1i ⊢ ( 𝜑 → 1 6 = ( 4 · 4 ) )
380 337 eqcomd ⊢ ( 𝜑 → 4 = ( 2 ↑ 2 ) )
381 380 oveq2d ⊢ ( 𝜑 → ( 4 · 4 ) = ( 4 · ( 2 ↑ 2 ) ) )
382 379 381 eqtrd ⊢ ( 𝜑 → 1 6 = ( 4 · ( 2 ↑ 2 ) ) )
383 373 376 382 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 / 2 ) + 2 ) ≤ ( 4 · ( 2 ↑ 2 ) ) )
384 346 348 339 361 383 letrd ⊢ ( 𝜑 → ( ( 1 0 / ( 2 logb 𝐴 ) ) + 2 ) ≤ ( 4 · ( 2 ↑ 2 ) ) )
385 345 384 eqbrtrd ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) ≤ ( 4 · ( 2 ↑ 2 ) ) )
386 4 6 8 ltled ⊢ ( 𝜑 → 0 ≤ 4 )
387 364 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
388 37 325 387 124 359 leexp1ad ⊢ ( 𝜑 → ( 2 ↑ 2 ) ≤ ( ( 2 logb 𝐴 ) ↑ 2 ) )
389 338 340 6 386 388 lemul2ad ⊢ ( 𝜑 → ( 4 · ( 2 ↑ 2 ) ) ≤ ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) )
390 335 339 341 385 389 letrd ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) ≤ ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) )
391 37 326 remulcld ⊢ ( 𝜑 → ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ∈ ℝ )
392 391 recnd ⊢ ( 𝜑 → ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ∈ ℂ )
393 326 recnd ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) ∈ ℂ )
394 274 392 393 333 divdird ⊢ ( 𝜑 → ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
395 13 393 393 333 divassd ⊢ ( 𝜑 → ( ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( 2 · ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
396 395 oveq2d ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + ( 2 · ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) ) )
397 393 333 dividd ⊢ ( 𝜑 → ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = 1 )
398 397 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = ( 2 · 1 ) )
399 398 180 eqtrd ⊢ ( 𝜑 → ( 2 · ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = 2 )
400 399 oveq2d ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + ( 2 · ( ( ( 2 logb 𝐴 ) ↑ 1 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) ) = ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) )
401 396 400 eqtrd ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) )
402 394 401 eqtrd ⊢ ( 𝜑 → ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) )
403 402 eqcomd ⊢ ( 𝜑 → ( ( 1 0 / ( ( 2 logb 𝐴 ) ↑ 1 ) ) + 2 ) = ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) )
404 2p1e3 ⊢ ( 2 + 1 ) = 3
405 404 a1i ⊢ ( 𝜑 → ( 2 + 1 ) = 3 )
406 302 recnd ⊢ ( 𝜑 → 3 ∈ ℂ )
407 406 53 13 subadd2d ⊢ ( 𝜑 → ( ( 3 − 1 ) = 2 ↔ ( 2 + 1 ) = 3 ) )
408 405 407 mpbird ⊢ ( 𝜑 → ( 3 − 1 ) = 2 )
409 408 eqcomd ⊢ ( 𝜑 → 2 = ( 3 − 1 ) )
410 409 oveq2d ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 2 ) = ( ( 2 logb 𝐴 ) ↑ ( 3 − 1 ) ) )
411 410 oveq2d ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) = ( 4 · ( ( 2 logb 𝐴 ) ↑ ( 3 − 1 ) ) ) )
412 4 330 gtned ⊢ ( 𝜑 → ( 2 logb 𝐴 ) ≠ 0 )
413 342 412 239 296 expsubd ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ ( 3 − 1 ) ) = ( ( ( 2 logb 𝐴 ) ↑ 3 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) )
414 413 oveq2d ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ ( 3 − 1 ) ) ) = ( 4 · ( ( ( 2 logb 𝐴 ) ↑ 3 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
415 411 414 eqtrd ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) = ( 4 · ( ( ( 2 logb 𝐴 ) ↑ 3 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
416 217 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
417 325 112 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 3 ) ∈ ℝ )
418 417 recnd ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 3 ) ∈ ℂ )
419 416 418 393 333 divassd ⊢ ( 𝜑 → ( ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( 4 · ( ( ( 2 logb 𝐴 ) ↑ 3 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
420 419 eqcomd ⊢ ( 𝜑 → ( 4 · ( ( ( 2 logb 𝐴 ) ↑ 3 ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = ( ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) )
421 415 420 eqtrd ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 2 ) ) = ( ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) )
422 390 403 421 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ≤ ( ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) )
423 287 391 readdcld ⊢ ( 𝜑 → ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) ∈ ℝ )
424 6 417 remulcld ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) ∈ ℝ )
425 423 424 332 lediv1d ⊢ ( 𝜑 → ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) ≤ ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) ↔ ( ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ≤ ( ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) / ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) )
426 422 425 mpbird ⊢ ( 𝜑 → ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) ≤ ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) )
427 87 uzidd ⊢ ( 𝜑 → 2 ∈ ( ℤ≥ ‘ 2 ) )
428 427 39 jca ⊢ ( 𝜑 → ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) )
429 relogbval ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ+ ) → ( 2 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) )
430 428 429 syl ⊢ ( 𝜑 → ( 2 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) )
431 430 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 1 ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) )
432 431 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) = ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) )
433 432 oveq2d ⊢ ( 𝜑 → ( 1 0 + ( 2 · ( ( 2 logb 𝐴 ) ↑ 1 ) ) ) = ( 1 0 + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) )
434 430 oveq1d ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 3 ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 3 ) )
435 12 18 26 112 expdivd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 3 ) = ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
436 434 435 eqtrd ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 3 ) = ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
437 436 oveq2d ⊢ ( 𝜑 → ( 4 · ( ( 2 logb 𝐴 ) ↑ 3 ) ) = ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) )
438 426 433 437 3brtr3d ⊢ ( 𝜑 → ( 1 0 + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) ≤ ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) )
439 292 293 299 323 438 letrd ⊢ ( 𝜑 → ( ( 1 0 / ( log ‘ 𝐴 ) ) + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) ≤ ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) )
440 12 exp1d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 1 ) = ( log ‘ 𝐴 ) )
441 440 eqcomd ⊢ ( 𝜑 → ( log ‘ 𝐴 ) = ( ( log ‘ 𝐴 ) ↑ 1 ) )
442 441 oveq2d ⊢ ( 𝜑 → ( 1 0 / ( log ‘ 𝐴 ) ) = ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) )
443 13 156 281 282 divassd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) = ( 2 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) )
444 12 18 26 91 expdivd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) = ( ( ( log ‘ 𝐴 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
445 444 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) )
446 445 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) = ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) )
447 443 446 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) = ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) )
448 447 eqcomd ⊢ ( 𝜑 → ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
449 442 448 oveq12d ⊢ ( 𝜑 → ( ( 1 0 / ( log ‘ 𝐴 ) ) + ( 2 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 1 ) ) ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) )
450 113 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 3 ) ∈ ℂ )
451 18 112 expcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 3 ) ∈ ℂ )
452 416 450 451 297 divassd ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) = ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) )
453 452 eqcomd ⊢ ( 𝜑 → ( 4 · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / ( ( log ‘ 2 ) ↑ 3 ) ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
454 439 449 453 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
455 285 454 eqbrtrd ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
456 281 282 dividd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) = 1 )
457 456 eqcomd ⊢ ( 𝜑 → 1 = ( ( ( log ‘ 2 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
458 457 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · ( ( ( log ‘ 2 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) )
459 277 281 281 281 282 282 divmuldivd ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · ( ( ( log ‘ 2 ) ↑ 1 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) )
460 458 459 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) )
461 460 oveq2d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 1 ) ) · 1 ) ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) ) )
462 416 450 mulcld ⊢ ( 𝜑 → ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) ∈ ℂ )
463 462 451 297 divcld ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) ∈ ℂ )
464 463 mulid1d ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · 1 ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) )
465 464 eqcomd ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · 1 ) )
466 455 461 465 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · 1 ) )
467 274 156 247 divcld ⊢ ( 𝜑 → ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ∈ ℂ )
468 467 mulid1d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · 1 ) = ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) )
469 468 eqcomd ⊢ ( 𝜑 → ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · 1 ) )
470 18 26 dividd ⊢ ( 𝜑 → ( ( log ‘ 2 ) / ( log ‘ 2 ) ) = 1 )
471 470 eqcomd ⊢ ( 𝜑 → 1 = ( ( log ‘ 2 ) / ( log ‘ 2 ) ) )
472 471 oveq2d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · 1 ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) / ( log ‘ 2 ) ) ) )
473 469 472 eqtrd ⊢ ( 𝜑 → ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) = ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) / ( log ‘ 2 ) ) ) )
474 274 156 18 18 247 26 divmuldivd ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) / ( log ‘ 2 ) ) ) = ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) )
475 473 474 eqtrd ⊢ ( 𝜑 → ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) = ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) )
476 18 exp1d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 1 ) = ( log ‘ 2 ) )
477 476 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) )
478 df-2 ⊢ 2 = ( 1 + 1 )
479 478 a1i ⊢ ( 𝜑 → 2 = ( 1 + 1 ) )
480 479 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 2 ) = ( ( log ‘ 2 ) ↑ ( 1 + 1 ) ) )
481 18 91 91 expaddd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ ( 1 + 1 ) ) = ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
482 480 481 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 2 ) = ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
483 482 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) = ( ( log ‘ 2 ) ↑ 2 ) )
484 477 483 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) )
485 475 484 oveq12d ⊢ ( 𝜑 → ( ( 1 0 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( log ‘ 2 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 1 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) ) = ( ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
486 476 eqcomd ⊢ ( 𝜑 → ( log ‘ 2 ) = ( ( log ‘ 2 ) ↑ 1 ) )
487 486 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 2 ) / ( log ‘ 2 ) ) = ( ( log ‘ 2 ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
488 471 487 eqtrd ⊢ ( 𝜑 → 1 = ( ( log ‘ 2 ) / ( ( log ‘ 2 ) ↑ 1 ) ) )
489 488 oveq2d ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · 1 ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · ( ( log ‘ 2 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) )
490 476 18 eqeltrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 1 ) ∈ ℂ )
491 476 26 eqnetrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 1 ) ≠ 0 )
492 462 451 18 490 297 491 divmuldivd ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · ( ( log ‘ 2 ) / ( ( log ‘ 2 ) ↑ 1 ) ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) )
493 489 492 eqtrd ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 3 ) ) · 1 ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) )
494 466 485 493 3brtr3d ⊢ ( 𝜑 → ( ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) )
495 156 18 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ∈ ℂ )
496 156 18 247 26 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ≠ 0 )
497 274 18 495 496 div23d ⊢ ( 𝜑 → ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) · ( log ‘ 2 ) ) )
498 277 18 155 88 div23d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) · ( log ‘ 2 ) ) )
499 497 498 oveq12d ⊢ ( 𝜑 → ( ( ( 1 0 · ( log ‘ 2 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) · ( log ‘ 2 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) · ( log ‘ 2 ) ) ) )
500 62 a1i ⊢ ( 𝜑 → 4 = ( 3 + 1 ) )
501 500 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) = ( ( log ‘ 2 ) ↑ ( 3 + 1 ) ) )
502 18 91 112 expaddd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ ( 3 + 1 ) ) = ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
503 501 502 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) = ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
504 503 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) = ( ( log ‘ 2 ) ↑ 4 ) )
505 504 oveq2d ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( ( log ‘ 2 ) ↑ 3 ) · ( ( log ‘ 2 ) ↑ 1 ) ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
506 494 499 505 3brtr3d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) · ( log ‘ 2 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) · ( log ‘ 2 ) ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
507 92 43 remulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ∈ ℝ )
508 287 507 496 redivcld ⊢ ( 𝜑 → ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ∈ ℝ )
509 508 recnd ⊢ ( 𝜑 → ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ∈ ℂ )
510 509 278 18 adddird ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) · ( log ‘ 2 ) ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) · ( log ‘ 2 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) · ( log ‘ 2 ) ) ) )
511 510 eqcomd ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) · ( log ‘ 2 ) ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) · ( log ‘ 2 ) ) ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) · ( log ‘ 2 ) ) )
512 18 26 212 expne0d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 4 ) ≠ 0 )
513 462 18 117 512 div23d ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( log ‘ 2 ) ) )
514 506 511 513 3brtr3d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) · ( log ‘ 2 ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( log ‘ 2 ) ) )
515 37 92 remulcld ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) ∈ ℝ )
516 515 85 88 redivcld ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ∈ ℝ )
517 508 516 readdcld ⊢ ( 𝜑 → ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ∈ ℝ )
518 114 115 120 redivcld ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) ∈ ℝ )
519 517 518 135 lemul1d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) ↔ ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) · ( log ‘ 2 ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( log ‘ 2 ) ) ) )
520 514 519 mpbird ⊢ ( 𝜑 → ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
521 280 520 eqbrtrd ⊢ ( 𝜑 → ( ( ( 1 0 · 1 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( 1 · ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
522 274 53 495 496 divassd ⊢ ( 𝜑 → ( ( 1 0 · 1 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( 1 0 · ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) )
523 53 277 155 88 div12d ⊢ ( 𝜑 → ( 1 · ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
524 522 523 oveq12d ⊢ ( 𝜑 → ( ( ( 1 0 · 1 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) + ( 1 · ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) = ( ( 1 0 · ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) )
525 462 mulid1d ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · 1 ) = ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) )
526 525 eqcomd ⊢ ( 𝜑 → ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · 1 ) )
527 526 oveq1d ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · 1 ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
528 521 524 527 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 · ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · 1 ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
529 3 11 dividd ⊢ ( 𝜑 → ( 𝐴 / 𝐴 ) = 1 )
530 529 eqcomd ⊢ ( 𝜑 → 1 = ( 𝐴 / 𝐴 ) )
531 530 oveq1d ⊢ ( 𝜑 → ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( ( 𝐴 / 𝐴 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) )
532 3 3 495 11 496 divdiv1d ⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) )
533 531 532 eqtrd ⊢ ( 𝜑 → ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) )
534 533 oveq2d ⊢ ( 𝜑 → ( 1 0 · ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) = ( 1 0 · ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) ) )
535 eqidd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
536 530 oveq1d ⊢ ( 𝜑 → ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) = ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) )
537 536 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
538 535 537 eqtrd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) )
539 534 538 oveq12d ⊢ ( 𝜑 → ( ( 1 0 · ( 1 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) = ( ( 1 0 · ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) )
540 462 53 117 512 divassd ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · 1 ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) ) )
541 528 539 540 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 · ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) ) )
542 3 495 mulcomd ⊢ ( 𝜑 → ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) · 𝐴 ) )
543 156 18 3 mulassd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) · 𝐴 ) = ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) )
544 542 543 eqtrd ⊢ ( 𝜑 → ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) = ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) )
545 544 oveq2d ⊢ ( 𝜑 → ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) = ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) )
546 545 oveq2d ⊢ ( 𝜑 → ( 1 0 · ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) ) = ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) )
547 3 3 155 11 88 divdiv1d ⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) = ( 𝐴 / ( 𝐴 · ( ( log ‘ 2 ) ↑ 2 ) ) ) )
548 3 155 mulcomd ⊢ ( 𝜑 → ( 𝐴 · ( ( log ‘ 2 ) ↑ 2 ) ) = ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) )
549 548 oveq2d ⊢ ( 𝜑 → ( 𝐴 / ( 𝐴 · ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) )
550 547 549 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) = ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) )
551 550 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
552 546 551 oveq12d ⊢ ( 𝜑 → ( ( 1 0 · ( 𝐴 / ( 𝐴 · ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( log ‘ 2 ) ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 2 ) ) ) ) = ( ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ) )
553 eqidd ⊢ ( 𝜑 → ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) = ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) )
554 530 oveq1d ⊢ ( 𝜑 → ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
555 553 554 eqtrd ⊢ ( 𝜑 → ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
556 555 oveq2d ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 1 / ( ( log ‘ 2 ) ↑ 4 ) ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) )
557 541 552 556 3brtr3d ⊢ ( 𝜑 → ( ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) )
558 156 261 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ∈ ℂ )
559 156 261 247 262 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ≠ 0 )
560 274 558 3 559 div32d ⊢ ( 𝜑 → ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) = ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) )
561 560 eqcomd ⊢ ( 𝜑 → ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) = ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) )
562 155 3 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ∈ ℂ )
563 155 3 88 11 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ≠ 0 )
564 277 562 3 563 div32d ⊢ ( 𝜑 → ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) = ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) )
565 564 eqcomd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) = ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) )
566 561 565 oveq12d ⊢ ( 𝜑 → ( ( 1 0 · ( 𝐴 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) ) )
567 3 3 117 11 512 divdiv1d ⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( 𝐴 / ( 𝐴 · ( ( log ‘ 2 ) ↑ 4 ) ) ) )
568 3 117 mulcomd ⊢ ( 𝜑 → ( 𝐴 · ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) )
569 568 oveq2d ⊢ ( 𝜑 → ( 𝐴 / ( 𝐴 · ( ( log ‘ 2 ) ↑ 4 ) ) ) = ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
570 567 569 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
571 570 oveq2d ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( ( 𝐴 / 𝐴 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ) )
572 557 566 571 3brtr3d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ) )
573 43 1 remulcld ⊢ ( 𝜑 → ( ( log ‘ 2 ) · 𝐴 ) ∈ ℝ )
574 92 573 remulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ∈ ℝ )
575 287 574 559 redivcld ⊢ ( 𝜑 → ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ∈ ℝ )
576 575 recnd ⊢ ( 𝜑 → ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) ∈ ℂ )
577 157 94 eqeltrrd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ∈ ℝ )
578 577 recnd ⊢ ( 𝜑 → ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ∈ ℂ )
579 576 578 3 adddird ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) · 𝐴 ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) ) )
580 579 eqcomd ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) · 𝐴 ) + ( ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) · 𝐴 ) ) = ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) · 𝐴 ) )
581 12 112 expcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 3 ) ∈ ℂ )
582 416 581 mulcld ⊢ ( 𝜑 → ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) ∈ ℂ )
583 117 3 mulcld ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ∈ ℂ )
584 117 3 512 11 mulne0d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ≠ 0 )
585 582 583 3 584 div32d ⊢ ( 𝜑 → ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) · 𝐴 ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ) )
586 585 eqcomd ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) · ( 𝐴 / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ) = ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) · 𝐴 ) )
587 572 580 586 3brtr3d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) · 𝐴 ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) · 𝐴 ) )
588 575 577 readdcld ⊢ ( 𝜑 → ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ∈ ℝ )
589 588 122 39 lemul1d ⊢ ( 𝜑 → ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) ↔ ( ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) · 𝐴 ) ≤ ( ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) · 𝐴 ) ) )
590 587 589 mpbird ⊢ ( 𝜑 → ( ( 1 0 / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
591 271 590 eqbrtrd ⊢ ( 𝜑 → ( ( ( 5 · 2 ) / ( ( ( log ‘ 𝐴 ) ↑ 1 ) · ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
592 267 591 eqbrtrd ⊢ ( 𝜑 → ( ( ( 5 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 · 1 ) / ( ( log ‘ 2 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
593 259 592 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 5 · 1 ) / ( ( log ‘ 𝐴 ) ↑ 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( 1 / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
594 254 593 eqbrtrd ⊢ ( 𝜑 → ( ( ( 5 · ( 1 / ( ( log ‘ 𝐴 ) ↑ 1 ) ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) / 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
595 246 594 eqbrtrd ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ - 1 ) ) · ( ( 2 / ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
596 238 595 eqbrtrd ⊢ ( 𝜑 → ( ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
597 211 596 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 𝐴 ) ↑ 5 ) ) · ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
598 205 597 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( ( log ‘ 2 ) · ( ( log ‘ 2 ) ↑ 5 ) ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
599 198 598 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( ( log ‘ 2 ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
600 192 599 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) · ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ) / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) · ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
601 189 600 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 2 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
602 184 601 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( ( 2 · 1 ) · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
603 179 602 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 2 · ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
604 174 603 eqbrtrd ⊢ ( 𝜑 → ( ( ( 2 · ( ( 1 · ( ( log ‘ 2 ) ↑ 5 ) ) / ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
605 170 604 eqbrtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) · ( log ‘ 2 ) ) / ( ( log ‘ 2 ) ↑ 5 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 · ( ( log ‘ 𝐴 ) ↑ 1 ) ) / ( ( ( log ‘ 2 ) ↑ 2 ) · 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
606 158 605 eqbrtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
607 95 111 122 149 606 letrd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) ↑ 5 ) / ( ( log ‘ 2 ) ↑ 5 ) ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
608 35 607 eqbrtrd ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) ≤ ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
609 427 39 429 syl2anc ⊢ ( 𝜑 → ( 2 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) )
610 609 eqcomd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) = ( 2 logb 𝐴 ) )
611 610 oveq1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) = ( ( 2 logb 𝐴 ) ↑ 5 ) )
612 611 oveq1d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) = ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) )
613 612 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) = ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) )
614 613 oveq2d ⊢ ( 𝜑 → ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) = ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) )
615 5cn ⊢ 5 ∈ ℂ
616 615 a1i ⊢ ( 𝜑 → 5 ∈ ℂ )
617 616 207 mulcld ⊢ ( 𝜑 → ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) ∈ ℂ )
618 617 mulid1d ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · 1 ) = ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) )
619 618 eqcomd ⊢ ( 𝜑 → ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) = ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · 1 ) )
620 eqidd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) = ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) )
621 df-5 ⊢ 5 = ( 4 + 1 )
622 621 a1i ⊢ ( 𝜑 → 5 = ( 4 + 1 ) )
623 622 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) = ( ( log ‘ 2 ) ↑ ( 4 + 1 ) ) )
624 18 91 77 expaddd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ ( 4 + 1 ) ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
625 623 624 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) ↑ 1 ) ) )
626 476 oveq2d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) ↑ 1 ) ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( log ‘ 2 ) ) )
627 625 626 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 2 ) ↑ 5 ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( log ‘ 2 ) ) )
628 627 oveq1d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) = ( ( ( ( log ‘ 2 ) ↑ 4 ) · ( log ‘ 2 ) ) · 𝐴 ) )
629 620 628 eqtrd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) = ( ( ( ( log ‘ 2 ) ↑ 4 ) · ( log ‘ 2 ) ) · 𝐴 ) )
630 117 18 3 mulassd ⊢ ( 𝜑 → ( ( ( ( log ‘ 2 ) ↑ 4 ) · ( log ‘ 2 ) ) · 𝐴 ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) · 𝐴 ) ) )
631 629 630 eqtrd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) · 𝐴 ) ) )
632 18 3 mulcomd ⊢ ( 𝜑 → ( ( log ‘ 2 ) · 𝐴 ) = ( 𝐴 · ( log ‘ 2 ) ) )
633 632 oveq2d ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 4 ) · ( ( log ‘ 2 ) · 𝐴 ) ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( 𝐴 · ( log ‘ 2 ) ) ) )
634 631 633 eqtrd ⊢ ( 𝜑 → ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) = ( ( ( log ‘ 2 ) ↑ 4 ) · ( 𝐴 · ( log ‘ 2 ) ) ) )
635 619 634 oveq12d ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · 1 ) / ( ( ( log ‘ 2 ) ↑ 4 ) · ( 𝐴 · ( log ‘ 2 ) ) ) ) )
636 3 18 mulcld ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 2 ) ) ∈ ℂ )
637 3 18 11 26 mulne0d ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 2 ) ) ≠ 0 )
638 186 117 53 636 120 637 divmuldivd ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · 1 ) / ( ( ( log ‘ 2 ) ↑ 4 ) · ( 𝐴 · ( log ‘ 2 ) ) ) ) )
639 638 eqcomd ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) · 1 ) / ( ( ( log ‘ 2 ) ↑ 4 ) · ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
640 635 639 eqtrd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
641 206 207 117 120 divassd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) )
642 641 oveq1d ⊢ ( 𝜑 → ( ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( log ‘ 2 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
643 640 642 eqtrd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
644 12 18 26 77 expdivd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) = ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) )
645 644 eqcomd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) = ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) )
646 645 oveq2d ⊢ ( 𝜑 → ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) = ( 5 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) ) )
647 646 oveq1d ⊢ ( 𝜑 → ( ( 5 · ( ( ( log ‘ 𝐴 ) ↑ 4 ) / ( ( log ‘ 2 ) ↑ 4 ) ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( 5 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
648 643 647 eqtrd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( 5 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
649 610 oveq1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) = ( ( 2 logb 𝐴 ) ↑ 4 ) )
650 649 oveq2d ⊢ ( 𝜑 → ( 5 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) ) = ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) )
651 650 oveq1d ⊢ ( 𝜑 → ( ( 5 · ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
652 648 651 eqtrd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
653 342 77 expcld ⊢ ( 𝜑 → ( ( 2 logb 𝐴 ) ↑ 4 ) ∈ ℂ )
654 616 653 mulcld ⊢ ( 𝜑 → ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) ∈ ℂ )
655 39 rpne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
656 3 18 655 26 mulne0d ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 2 ) ) ≠ 0 )
657 636 656 reccld ⊢ ( 𝜑 → ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ∈ ℂ )
658 654 657 mulcld ⊢ ( 𝜑 → ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) ∈ ℂ )
659 658 addid1d ⊢ ( 𝜑 → ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) = ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) )
660 659 eqcomd ⊢ ( 𝜑 → ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) = ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) )
661 652 660 eqtrd ⊢ ( 𝜑 → ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) = ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) )
662 614 661 oveq12d ⊢ ( 𝜑 → ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) = ( ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) ) )
663 662 oveq2d ⊢ ( 𝜑 → ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) = ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) )
664 1e2m1 ⊢ 1 = ( 2 − 1 )
665 664 a1i ⊢ ( 𝜑 → 1 = ( 2 − 1 ) )
666 665 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 1 ) = ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) )
667 666 oveq1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) = ( ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) / 𝐴 ) )
668 667 oveq2d ⊢ ( 𝜑 → ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) = ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) / 𝐴 ) ) )
669 663 668 oveq12d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 2 ) ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( 5 · ( ( log ‘ 𝐴 ) ↑ 4 ) ) / ( ( ( log ‘ 2 ) ↑ 5 ) · 𝐴 ) ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 1 ) / 𝐴 ) ) ) = ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) / 𝐴 ) ) ) )
670 4cn ⊢ 4 ∈ ℂ
671 670 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
672 671 117 581 3 120 655 divmuldivd ⊢ ( 𝜑 → ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / 𝐴 ) ) = ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) )
673 672 eqcomd ⊢ ( 𝜑 → ( ( 4 · ( ( log ‘ 𝐴 ) ↑ 3 ) ) / ( ( ( log ‘ 2 ) ↑ 4 ) · 𝐴 ) ) = ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / 𝐴 ) ) )
674 608 669 673 3brtr3d ⊢ ( 𝜑 → ( ( 2 · ( ( 1 / ( ( ( ( 2 logb 𝐴 ) ↑ 5 ) + 1 ) · ( log ‘ 2 ) ) ) · ( ( ( 5 · ( ( 2 logb 𝐴 ) ↑ 4 ) ) · ( 1 / ( 𝐴 · ( log ‘ 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ‘ 2 ) ↑ 2 ) ) · ( ( ( log ‘ 𝐴 ) ↑ ( 2 − 1 ) ) / 𝐴 ) ) ) ≤ ( ( 4 / ( ( log ‘ 2 ) ↑ 4 ) ) · ( ( ( log ‘ 𝐴 ) ↑ 3 ) / 𝐴 ) ) )