Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks4d1p1p7 Structured version   Visualization version   GIF version

Theorem aks4d1p1p7 40427
Description: Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024.)
Hypotheses
Ref Expression
aks4d1p1p7.1 (𝜑𝐴 ∈ ℝ)
aks4d1p1p7.2 (𝜑 → 4 ≤ 𝐴)
Assertion
Ref Expression
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 of Theorem aks4d1p1p7
StepHypRef Expression
1 aks4d1p1p7.1 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ)
21recnd 11117 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
3 0red 11092 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4 4re 12171 . . . . . . . . . . . . . . 15 4 ∈ ℝ
54a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
6 4pos 12194 . . . . . . . . . . . . . . 15 0 < 4
76a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 4)
8 aks4d1p1p7.2 . . . . . . . . . . . . . 14 (𝜑 → 4 ≤ 𝐴)
93, 5, 1, 7, 8ltletrd 11249 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝐴)
103, 9ltned 11225 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 𝐴)
1110necomd 2998 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
122, 11logcld 25849 . . . . . . . . . 10 (𝜑 → (log‘𝐴) ∈ ℂ)
13 2cnd 12165 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
14 2pos 12190 . . . . . . . . . . . . . 14 0 < 2
1514a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 < 2)
163, 15ltned 11225 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 2)
1716necomd 2998 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
1813, 17logcld 25849 . . . . . . . . . 10 (𝜑 → (log‘2) ∈ ℂ)
19 1lt2 12258 . . . . . . . . . . . . . 14 1 < 2
20 2rp 12849 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
21 loggt0b 25910 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
2220, 21ax-mp 5 . . . . . . . . . . . . . 14 (0 < (log‘2) ↔ 1 < 2)
2319, 22mpbir 230 . . . . . . . . . . . . 13 0 < (log‘2)
2423a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < (log‘2))
253, 24ltned 11225 . . . . . . . . . . 11 (𝜑 → 0 ≠ (log‘2))
2625necomd 2998 . . . . . . . . . 10 (𝜑 → (log‘2) ≠ 0)
27 5nn0 12367 . . . . . . . . . . 11 5 ∈ ℕ0
2827a1i 11 . . . . . . . . . 10 (𝜑 → 5 ∈ ℕ0)
2912, 18, 26, 28expdivd 13992 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
3029oveq1d 7365 . . . . . . . 8 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
3130oveq1d 7365 . . . . . . 7 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
3231oveq2d 7366 . . . . . 6 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
3332oveq1d 7365 . . . . 5 (𝜑 → ((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) · 𝐴))))
3433oveq2d 7366 . . . 4 (𝜑 → (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) · 𝐴)))))
3534oveq1d 7365 . . 3 (𝜑 → ((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 12161 . . . . . . 7 2 ∈ ℝ
3736a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
38 1red 11090 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
391, 9elrpd 12883 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
4039relogcld 25901 . . . . . . . . . . . 12 (𝜑 → (log‘𝐴) ∈ ℝ)
4140, 28reexpcld 13995 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
4220a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ+)
4342relogcld 25901 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ)
4443, 28reexpcld 13995 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ)
4528nn0zd 12538 . . . . . . . . . . . 12 (𝜑 → 5 ∈ ℤ)
4618, 26, 45expne0d 13984 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ≠ 0)
4741, 44, 46redivcld 11917 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
4847, 38readdcld 11118 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
4948, 43remulcld 11119 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
5012, 28expcld 13978 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
5118, 28expcld 13978 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℂ)
5250, 51, 46divcld 11865 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53 1cnd 11084 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
5452, 53addcld 11108 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
5519a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 2)
5637, 55rplogcld 25907 . . . . . . . . . . . . . 14 (𝜑 → (log‘2) ∈ ℝ+)
5756, 45rpexpcld 14076 . . . . . . . . . . . . 13 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58 1re 11089 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
59 3nn0 12365 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℕ0
6058, 59nn0addge2i 12396 . . . . . . . . . . . . . . . . . 18 1 ≤ (3 + 1)
6160a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≤ (3 + 1))
62 df-4 12152 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
6361, 62breqtrrdi 5146 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 4)
6438, 5, 1, 63, 8letrd 11246 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝐴)
651, 64logge0d 25908 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (log‘𝐴))
6640, 28, 65expge0d 13996 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ ((log‘𝐴)↑5))
6741, 57, 66divge0d 12926 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
6847ltp1d 12019 . . . . . . . . . . . 12 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
693, 47, 48, 67, 68lelttrd 11247 . . . . . . . . . . 11 (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
703, 69ltned 11225 . . . . . . . . . 10 (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
7170necomd 2998 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
7254, 18, 71, 26mulne0d 11741 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
7338, 49, 72redivcld 11917 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74 5re 12174 . . . . . . . . . 10 5 ∈ ℝ
7574a1i 11 . . . . . . . . 9 (𝜑 → 5 ∈ ℝ)
76 4nn0 12366 . . . . . . . . . . 11 4 ∈ ℕ0
7776a1i 11 . . . . . . . . . 10 (𝜑 → 4 ∈ ℕ0)
7840, 77reexpcld 13995 . . . . . . . . 9 (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
7975, 78remulcld 11119 . . . . . . . 8 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
8044, 1remulcld 11119 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
8151, 2, 46, 11mulne0d 11741 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
8279, 80, 81redivcld 11917 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
8373, 82remulcld 11119 . . . . . 6 (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
8437, 83remulcld 11119 . . . . 5 (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
8543resqcld 14079 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℝ)
86 2z 12466 . . . . . . . . 9 2 ∈ ℤ
8786a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
8818, 26, 87expne0d 13984 . . . . . . 7 (𝜑 → ((log‘2)↑2) ≠ 0)
8937, 85, 88redivcld 11917 . . . . . 6 (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90 1nn0 12363 . . . . . . . . 9 1 ∈ ℕ0
9190a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℕ0)
9240, 91reexpcld 13995 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
9392, 1, 11redivcld 11917 . . . . . 6 (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
9489, 93remulcld 11119 . . . . 5 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
9584, 94readdcld 11118 . . . 4 (𝜑 → ((2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ∈ ℝ)
9647, 43remulcld 11119 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97 1lt4 12263 . . . . . . . . . . . . . . . 16 1 < 4
9897a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 4)
9938, 5, 1, 98, 8ltletrd 11249 . . . . . . . . . . . . . 14 (𝜑 → 1 < 𝐴)
100 loggt0b 25910 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10139, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10299, 101mpbird 257 . . . . . . . . . . . . 13 (𝜑 → 0 < (log‘𝐴))
1033, 102ltned 11225 . . . . . . . . . . . 12 (𝜑 → 0 ≠ (log‘𝐴))
104103necomd 2998 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ≠ 0)
10512, 104, 45expne0d 13984 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ≠ 0)
10650, 51, 105, 46divne0d 11881 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
10752, 18, 106, 26mulne0d 11741 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
10838, 96, 107redivcld 11917 . . . . . . 7 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109108, 82remulcld 11119 . . . . . 6 (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
11037, 109remulcld 11119 . . . . 5 (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111110, 94readdcld 11118 . . . 4 (𝜑 → ((2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ∈ ℝ)
11259a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
11340, 112reexpcld 13995 . . . . . 6 (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
1145, 113remulcld 11119 . . . . 5 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
11543, 77reexpcld 13995 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℝ)
116115, 1remulcld 11119 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
11718, 77expcld 13978 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℂ)
118 4z 12468 . . . . . . . 8 4 ∈ ℤ
119118a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℤ)
12018, 26, 119expne0d 13984 . . . . . 6 (𝜑 → ((log‘2)↑4) ≠ 0)
121117, 2, 120, 11mulne0d 11741 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122114, 116, 121redivcld 11917 . . . 4 (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123 0le2 12189 . . . . . . 7 0 ≤ 2
124123a1i 11 . . . . . 6 (𝜑 → 0 ≤ 2)
12557, 39rpmulcld 12902 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
12628nn0ge0d 12410 . . . . . . . . 9 (𝜑 → 0 ≤ 5)
12740, 77, 65expge0d 13996 . . . . . . . . 9 (𝜑 → 0 ≤ ((log‘𝐴)↑4))
12875, 78, 126, 127mulge0d 11666 . . . . . . . 8 (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
12979, 125, 128divge0d 12926 . . . . . . 7 (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
1301, 99rplogcld 25907 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ∈ ℝ+)
131130, 45rpexpcld 14076 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132131, 57rpdivcld 12903 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133132, 56rpmulcld 12902 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
13424, 22sylib 217 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
13537, 134rplogcld 25907 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ+)
136135, 45rpexpcld 14076 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
13741, 136, 66divge0d 12926 . . . . . . . . . 10 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
13847, 137ge0p1rpd 12916 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139138, 135rpmulcld 12902 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140 0le1 11612 . . . . . . . . 9 0 ≤ 1
141140a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ 1)
142135rpred 12886 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℝ)
143135rpge0d 12890 . . . . . . . . 9 (𝜑 → 0 ≤ (log‘2))
14447lep1d 12020 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
14547, 48, 142, 143, 144lemul1ad 12028 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146133, 139, 38, 141, 145lediv2ad 12908 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ≤ (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))))
14773, 108, 82, 129, 146lemul1ad 12028 . . . . . 6 (𝜑 → ((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) · 𝐴))))
14883, 109, 37, 124, 147lemul2ad 12029 . . . . 5 (𝜑 → (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) · 𝐴)))))
14984, 110, 94, 148leadd1dd 11703 . . . 4 (𝜑 → ((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) / 𝐴))))
15050, 18, 51, 46div23d 11902 . . . . . . . . . 10 (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151150eqcomd 2744 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152151oveq2d 7366 . . . . . . . 8 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153152oveq1d 7365 . . . . . . 7 (𝜑 → ((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) · 𝐴))))
154153oveq2d 7366 . . . . . 6 (𝜑 → (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) · 𝐴)))))
15518sqcld 13976 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℂ)
15612, 91expcld 13978 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
15713, 155, 156, 2, 88, 11divmuldivd 11906 . . . . . 6 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158154, 157oveq12d 7368 . . . . 5 (𝜑 → ((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) · 𝐴))))
15950, 18mulcld 11109 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
16050, 18, 105, 26mulne0d 11741 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
16153, 159, 51, 160, 46divdiv2d 11897 . . . . . . . . . 10 (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162161oveq1d 7365 . . . . . . . . 9 (𝜑 → ((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) · 𝐴))))
163162oveq2d 7366 . . . . . . . 8 (𝜑 → (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) · 𝐴)))))
16453, 51mulcld 11109 . . . . . . . . . . 11 (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165164, 159, 160divcld 11865 . . . . . . . . . 10 (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
16682recnd 11117 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
16713, 165, 166mulassd 11112 . . . . . . . . 9 (𝜑 → ((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) · 𝐴)))))
168167eqcomd 2744 . . . . . . . 8 (𝜑 → (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) · 𝐴))))
169163, 168eqtrd 2778 . . . . . . 7 (𝜑 → (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) · 𝐴))))
170169oveq1d 7365 . . . . . 6 (𝜑 → ((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) · 𝐴))))
17113, 164, 159, 160divassd 11900 . . . . . . . . . 10 (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172171eqcomd 2744 . . . . . . . . 9 (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173172oveq1d 7365 . . . . . . . 8 (𝜑 → ((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) · 𝐴))))
174173oveq1d 7365 . . . . . . 7 (𝜑 → (((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) · 𝐴))))
17513, 53, 51mulassd 11112 . . . . . . . . . . . 12 (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176175eqcomd 2744 . . . . . . . . . . 11 (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177176oveq1d 7365 . . . . . . . . . 10 (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178177oveq1d 7365 . . . . . . . . 9 (𝜑 → (((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) · 𝐴))))
179178oveq1d 7365 . . . . . . . 8 (𝜑 → ((((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) · 𝐴))))
18013mulid1d 11106 . . . . . . . . . . . . 13 (𝜑 → (2 · 1) = 2)
181180oveq1d 7365 . . . . . . . . . . . 12 (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182181oveq1d 7365 . . . . . . . . . . 11 (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183182oveq1d 7365 . . . . . . . . . 10 (𝜑 → ((((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) · 𝐴))))
184183oveq1d 7365 . . . . . . . . 9 (𝜑 → (((((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) · 𝐴))))
18513, 51mulcld 11109 . . . . . . . . . . . 12 (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
18679recnd 11117 . . . . . . . . . . . 12 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
18751, 2mulcld 11109 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188185, 159, 186, 187, 160, 81divmuldivd 11906 . . . . . . . . . . 11 (𝜑 → (((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) · 𝐴))))
189188oveq1d 7365 . . . . . . . . . 10 (𝜑 → ((((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) · 𝐴))))
19050, 18, 187mulassd 11112 . . . . . . . . . . . . 13 (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191190oveq2d 7366 . . . . . . . . . . . 12 (𝜑 → (((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) · 𝐴)))))
192191oveq1d 7365 . . . . . . . . . . 11 (𝜑 → ((((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) · 𝐴))))
193185, 186mulcomd 11110 . . . . . . . . . . . . . 14 (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
19418, 51, 2mulassd 11112 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195194eqcomd 2744 . . . . . . . . . . . . . . 15 (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196195oveq2d 7366 . . . . . . . . . . . . . 14 (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197193, 196oveq12d 7368 . . . . . . . . . . . . 13 (𝜑 → (((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)) · 𝐴))))
198197oveq1d 7365 . . . . . . . . . . . 12 (𝜑 → ((((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) · 𝐴))))
19918, 51mulcld 11109 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200199, 2mulcld 11109 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
20118, 51, 26, 46mulne0d 11741 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202199, 2, 201, 11mulne0d 11741 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203186, 50, 185, 200, 105, 202divmuldivd 11906 . . . . . . . . . . . . . . 15 (𝜑 → (((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)) · 𝐴))))
204203eqcomd 2744 . . . . . . . . . . . . . 14 (𝜑 → (((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)) · 𝐴))))
205204oveq1d 7365 . . . . . . . . . . . . 13 (𝜑 → ((((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) · 𝐴))))
20675recnd 11117 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℂ)
20778recnd 11117 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208206, 207, 50, 105divassd 11900 . . . . . . . . . . . . . . . 16 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209194oveq2d 7366 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210208, 209oveq12d 7368 . . . . . . . . . . . . . . 15 (𝜑 → (((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) · 𝐴)))))
211210oveq1d 7365 . . . . . . . . . . . . . 14 (𝜑 → ((((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) · 𝐴))))
21277nn0zd 12538 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 4 ∈ ℤ)
21312, 104, 45, 212expsubd 13989 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214213eqcomd 2744 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215 4p1e5 12233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (4 + 1) = 5
21674recni 11103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 5 ∈ ℂ
2174recni 11103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 4 ∈ ℂ
218 ax-1cn 11043 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
219216, 217, 218subaddi 11422 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((5 − 4) = 1 ↔ (4 + 1) = 5)
220215, 219mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . 24 (5 − 4) = 1
221220a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 − 4) = 1)
22253subid1d 11435 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 − 0) = 1)
223221, 222eqtr4d 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 − 4) = (1 − 0))
224206, 217jctir 522 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225 0cnd 11082 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 ∈ ℂ)
22653, 225jca 513 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227 subeqrev 11511 . . . . . . . . . . . . . . . . . . . . . . 23 (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228224, 226, 227syl2anc 585 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229223, 228mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (4 − 5) = (0 − 1))
230 df-neg 11322 . . . . . . . . . . . . . . . . . . . . 21 -1 = (0 − 1)
231229, 230eqtr4di 2796 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (4 − 5) = -1)
232231oveq2d 7366 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233214, 232eqtrd 2778 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234233oveq2d 7366 . . . . . . . . . . . . . . . . 17 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
23513, 18, 51, 187, 26, 81divmuldivd 11906 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236235eqcomd 2744 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237234, 236oveq12d 7368 . . . . . . . . . . . . . . . 16 (𝜑 → ((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) · 𝐴)))))
238237oveq1d 7365 . . . . . . . . . . . . . . 15 (𝜑 → (((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 12465 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℤ)
24012, 104, 239expnegd 13985 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241240oveq2d 7366 . . . . . . . . . . . . . . . . . 18 (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
24251, 51, 2, 46, 11divdiv1d 11896 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243242eqcomd 2744 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244243oveq2d 7366 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245241, 244oveq12d 7368 . . . . . . . . . . . . . . . . 17 (𝜑 → ((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)) / 𝐴))))
246245oveq1d 7365 . . . . . . . . . . . . . . . 16 (𝜑 → (((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) · 𝐴))))
24712, 104, 239expne0d 13984 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248206, 53, 156, 247divassd 11900 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249248eqcomd 2744 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
25051, 46dividd 11863 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251250oveq1d 7365 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252251oveq2d 7366 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253249, 252oveq12d 7368 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) = (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))))
254253oveq1d 7365 . . . . . . . . . . . . . . . . 17 (𝜑 → (((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) · 𝐴))))
255206mulid1d 11106 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (5 · 1) = 5)
256255oveq1d 7365 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
25713, 18, 53, 2, 26, 11divmuldivd 11906 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258256, 257oveq12d 7368 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259258oveq1d 7365 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((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) · 𝐴))))
260180, 13eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (2 · 1) ∈ ℂ)
26118, 2mulcld 11109 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
26218, 2, 26, 11mulne0d 11741 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263206, 156, 260, 261, 247, 262divmuldivd 11906 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264180oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · (2 · 1)) = (5 · 2))
265264oveq1d 7365 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266263, 265eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267266oveq1d 7365 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((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 12651 . . . . . . . . . . . . . . . . . . . . . . 23 (5 · 2) = 10
269268a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · 2) = 10)
270269oveq1d 7365 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271270oveq1d 7365 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
272 10nn0 12569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 10 ∈ ℕ0
273272nn0cni 12359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 10 ∈ ℂ
274273a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑10 ∈ ℂ)
275274mulid1d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (10 · 1) = 10)
276275oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 / (((log‘𝐴)↑1) · (log‘2))))
27713, 156mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278277, 155, 88divcld 11865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279278mulid2d 11107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280276, 279oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))))
28118, 91expcld 13978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ∈ ℂ)
28218, 26, 239expne0d 13984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ≠ 0)
283277, 281, 282divcld 11865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284283mulid1d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285284oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286 10re 12570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 10 ∈ ℝ
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑10 ∈ ℝ)
288287, 40, 104redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ∈ ℝ)
28940, 43, 26redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290289, 91reexpcld 13995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
29137, 290remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292288, 291readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293287, 291readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
29443, 112reexpcld 13995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ∈ ℝ)
295 3z 12467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3 ∈ ℤ
296295a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → 3 ∈ ℤ)
29718, 26, 296expne0d 13984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ≠ 0)
298113, 294, 297redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
2995, 298remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300 ere 15906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 e ∈ ℝ
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e ∈ ℝ)
302112nn0red 12408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 ∈ ℝ)
303 egt2lt3 16023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (2 < e ∧ e < 3)
304303simpri 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 e < 3
305304a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → e < 3)
306 3lt4 12261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3 < 4
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 3 < 4)
308302, 5, 1, 307, 8ltletrd 11249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 < 𝐴)
309301, 302, 1, 305, 308lttrd 11250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e < 𝐴)
310301, 1, 309ltled 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → e ≤ 𝐴)
311301, 1lenltd 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312310, 311mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ¬ 𝐴 < e)
313 loglt1b 25912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
31439, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315312, 314mtbird 325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ¬ (log‘𝐴) < 1)
31638, 40lenltd 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317315, 316mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → 1 ≤ (log‘𝐴))
318 10nn 12567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 10 ∈ ℕ
319318a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑10 ∈ ℕ)
320 nnledivrp 12956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
321319, 130, 320syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
322317, 321mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ≤ 10)
323288, 287, 291, 322leadd1dd 11703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
32438, 55gtned 11224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≠ 1)
32537, 15, 1, 9, 324relogbcld 40326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ∈ ℝ)
326325, 91reexpcld 13995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
32742, 55jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328 logbgt0b 26066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
32939, 327, 328syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
33099, 329mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 0 < (2 logb 𝐴))
331325, 330elrpd 12883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332331, 239rpexpcld 14076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333332rpne0d 12891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334287, 326, 333redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335334, 37readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336 sq2 14028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (2↑2) = 4
337336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2↑2) = 4)
338337, 5eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ∈ ℝ)
3395, 338remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ∈ ℝ)
340325resqcld 14079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
3415, 340remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342325recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℂ)
343342exp1d 13973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344343oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (10 / ((2 logb 𝐴)↑1)) = (10 / (2 logb 𝐴)))
345344oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) = ((10 / (2 logb 𝐴)) + 2))
346345, 335eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347287rehalfcld 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
348347, 37readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ∈ ℝ)
349344, 334eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ∈ ℝ)
350287, 37, 17redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
351272nn0ge0i 12374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 0 ≤ 10
352351a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 0 ≤ 10)
35342, 324, 87relogbexpd 40327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 logb (2↑2)) = 2)
354353eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 = (2 logb (2↑2)))
355337oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356354, 355eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 2 = (2 logb 4))
35737leidd 11655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 ≤ 2)
35887, 357, 5, 7, 1, 9, 8logblebd 40329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359356, 358eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≤ (2 logb 𝐴))
36042, 331, 287, 352, 359lediv2ad 12908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ≤ (10 / 2))
361349, 350, 37, 360leadd1dd 11703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ ((10 / 2) + 2))
362 1nn 12098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 1 ∈ ℕ
363 6nn0 12368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6 ∈ ℕ0
364 2nn0 12364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2 ∈ ℕ0
36527, 364nn0addcli 12384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ∈ ℕ0
366 5p2e7 12243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (5 + 2) = 7
367 7re 12180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 7 ∈ ℝ
368367, 364nn0addge1i 12395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 7 ≤ (7 + 2)
369 7p2e9 12248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (7 + 2) = 9
370368, 369breqtri 5129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7 ≤ 9
371366, 370eqbrtri 5125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ≤ 9
372362, 363, 365, 371declei 12587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (5 + 2) ≤ 16
373372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) ≤ 16)
374206, 13, 274, 17ldiv 11923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((5 · 2) = 10 ↔ 5 = (10 / 2)))
375269, 374mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 5 = (10 / 2))
376375oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) = ((10 / 2) + 2))
377 4t4e16 12650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (4 · 4) = 16
378377eqcomi 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 16 = (4 · 4)
379378a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑16 = (4 · 4))
380337eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 4 = (2↑2))
381380oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (4 · 4) = (4 · (2↑2)))
382379, 381eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑16 = (4 · (2↑2)))
383373, 376, 3823brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ≤ (4 · (2↑2)))
384346, 348, 339, 361, 383letrd 11246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385345, 384eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
3863, 5, 7ltled 11237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → 0 ≤ 4)
387364a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ ℕ0)
38837, 325, 387, 124, 359leexp1ad 40325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389338, 340, 5, 386, 388lemul2ad 12029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390335, 339, 341, 385, 389letrd 11246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
39137, 326remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392391recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393326recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394274, 392, 393, 333divdird 11903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))))
39513, 393, 393, 333divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396395oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))))
397393, 333dividd 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398397oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399398, 180eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400399oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
401396, 400eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
402394, 401eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((10 / ((2 logb 𝐴)↑1)) + 2))
403402eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) = ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404 2p1e3 12229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 + 1) = 3
405404a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 + 1) = 3)
406302recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 3 ∈ ℂ)
407406, 53, 13subadd2d 11465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408405, 407mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (3 − 1) = 2)
409408eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 2 = (3 − 1))
410409oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411410oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
4123, 330gtned 11224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ≠ 0)
413342, 412, 239, 296expsubd 13989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414413oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415411, 414eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 4 ∈ ℂ)
417325, 112reexpcld 13995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418417recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419416, 418, 393, 333divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420419eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421415, 420eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422390, 403, 4213brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423287, 391readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
4245, 417remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425423, 424, 332lediv1d 12932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)) ↔ ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1))))
426422, 425mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
42787uzidd 12712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ (ℤ‘2))
428427, 39jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+))
429 relogbval 26045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431430oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432431oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433432oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) = (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434430oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
43512, 18, 26, 112expdivd 13992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436434, 435eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437436oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438426, 433, 4373brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439292, 293, 299, 323, 438letrd 11246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
44012exp1d 13973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441440eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442441oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 / (log‘𝐴)) = (10 / ((log‘𝐴)↑1)))
44313, 156, 281, 282divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
44412, 18, 26, 91expdivd 13992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445444eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446445oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447443, 446eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448447eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449442, 448oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450113recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
45118, 112expcld 13978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑3) ∈ ℂ)
452416, 450, 451, 297divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453452eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454439, 449, 4533brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455285, 454eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456281, 282dividd 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457456eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458457oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · (((log‘2)↑1) / ((log‘2)↑1))))
459277, 281, 281, 281, 282, 282divmuldivd 11906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · (((log‘2)↑1) / ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
460458, 459eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461460oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1)))))
462416, 450mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463462, 451, 297divcld 11865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464463mulid1d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465464eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466455, 461, 4653brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1)))) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
467274, 156, 247divcld 11865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / ((log‘𝐴)↑1)) ∈ ℂ)
468467mulid1d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = (10 / ((log‘𝐴)↑1)))
469468eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · 1))
47018, 26dividd 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2) / (log‘2)) = 1)
471470eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = ((log‘2) / (log‘2)))
472471oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473469, 472eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474274, 156, 18, 18, 247, 26divmuldivd 11906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475473, 474eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
47618exp1d 13973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑1) = (log‘2))
477476oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478 df-2 12150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2 = (1 + 1)
479478a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → 2 = (1 + 1))
480479oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
48118, 91, 91expaddd 13980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482480, 481eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483482eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484477, 483oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)))
485475, 484oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1)))) = (((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2))))
486476eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (log‘2) = ((log‘2)↑1))
487486oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488471, 487eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489488oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490476, 18eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ∈ ℂ)
491476, 26eqnetrd 3010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ≠ 0)
492462, 451, 18, 490, 297, 491divmuldivd 11906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
493489, 492eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494466, 485, 4933brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((10 · (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))))
495156, 18mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496156, 18, 247, 26mulne0d 11741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497274, 18, 495, 496div23d 11902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498277, 18, 155, 88div23d 11902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499497, 498oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2))) = (((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))))
50062a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → 4 = (3 + 1))
501500oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
50218, 91, 112expaddd 13980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503501, 502eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504503eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505504oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)))
506494, 499, 5053brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))) ≤ (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)))
50792, 43remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508287, 507, 496redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509508recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510509, 278, 18adddird 11114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) = (((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))))
511510eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))) = (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)))
51218, 26, 212expne0d 13984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((log‘2)↑4) ≠ 0)
513462, 18, 117, 512div23d 11902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514506, 511, 5133brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
51537, 92remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516515, 85, 88redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517508, 516readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518114, 115, 120redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519517, 518, 135lemul1d 12929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ↔ (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2))))
520514, 519mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521280, 520eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
522274, 53, 495, 496divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
52353, 277, 155, 88div12d 11901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524522, 523oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))))
525462mulid1d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526525eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527526oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528521, 524, 5273brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))) ≤ (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
5292, 11dividd 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴 / 𝐴) = 1)
530529eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 1 = (𝐴 / 𝐴))
531530oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
5322, 2, 495, 11, 496divdiv1d 11896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533531, 532eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534533oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536530oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537536oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538535, 537eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539534, 538oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))) = ((10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))))
540462, 53, 117, 512divassd 11900 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541528, 539, 5403brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
5422, 495mulcomd 11110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543156, 18, 2mulassd 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544542, 543eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545544oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546545oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
5472, 2, 155, 11, 88divdiv1d 11896 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
5482, 155mulcomd 11110 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549548oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550547, 549eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551550oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552546, 551oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) = ((10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))))
553 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554530oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555553, 554eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556555oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557541, 552, 5563brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558156, 261mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559156, 261, 247, 262mulne0d 11741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560274, 558, 2, 559div32d 11888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561560eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562155, 2mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563155, 2, 88, 11mulne0d 11741 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564277, 562, 2, 563div32d 11888 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565564eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566561, 565oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) = (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)))
5672, 2, 117, 11, 512divdiv1d 11896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
5682, 117mulcomd 11110 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569568oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570567, 569eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571570oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572557, 566, 5713brtr3d 5135 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
57343, 1remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
57492, 573remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575287, 574, 559redivcld 11917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576575recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577157, 94eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578577recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579576, 578, 2adddird 11114 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) = (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)))
580579eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) = (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴))
58112, 112expcld 13978 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582416, 581mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583117, 2mulcld 11109 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584117, 2, 512, 11mulne0d 11741 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585582, 583, 2, 584div32d 11888 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586585eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587572, 580, 5863brtr3d 5135 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588575, 577readdcld 11118 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589588, 122, 39lemul1d 12929 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ↔ (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴)))
590587, 589mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591271, 590eqbrtrd 5126 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592267, 591eqbrtrd 5126 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593259, 592eqbrtrd 5126 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
594254, 593eqbrtrd 5126 . . . . . . . . . . . . . . . 16 (𝜑 → (((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) · 𝐴)))
595246, 594eqbrtrd 5126 . . . . . . . . . . . . . . 15 (𝜑 → (((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
596238, 595eqbrtrd 5126 . . . . . . . . . . . . . 14 (𝜑 → (((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) · 𝐴)))
597211, 596eqbrtrd 5126 . . . . . . . . . . . . 13 (𝜑 → ((((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) · 𝐴)))
598205, 597eqbrtrd 5126 . . . . . . . . . . . 12 (𝜑 → ((((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) · 𝐴)))
599198, 598eqbrtrd 5126 . . . . . . . . . . 11 (𝜑 → ((((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) · 𝐴)))
600192, 599eqbrtrd 5126 . . . . . . . . . 10 (𝜑 → ((((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) · 𝐴)))
601189, 600eqbrtrd 5126 . . . . . . . . 9 (𝜑 → ((((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) · 𝐴)))
602184, 601eqbrtrd 5126 . . . . . . . 8 (𝜑 → (((((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) · 𝐴)))
603179, 602eqbrtrd 5126 . . . . . . 7 (𝜑 → ((((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) · 𝐴)))
604174, 603eqbrtrd 5126 . . . . . 6 (𝜑 → (((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) · 𝐴)))
605170, 604eqbrtrd 5126 . . . . 5 (𝜑 → ((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) · 𝐴)))
606158, 605eqbrtrd 5126 . . . 4 (𝜑 → ((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) · 𝐴)))
60795, 111, 122, 149, 606letrd 11246 . . 3 (𝜑 → ((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) · 𝐴)))
60835, 607eqbrtrd 5126 . 2 (𝜑 → ((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) · 𝐴)))
609427, 39, 429syl2anc 585 . . . . . . . . . 10 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610609eqcomd 2744 . . . . . . . . 9 (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611610oveq1d 7365 . . . . . . . 8 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612611oveq1d 7365 . . . . . . 7 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613612oveq1d 7365 . . . . . 6 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614613oveq2d 7366 . . . . 5 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615 5cn 12175 . . . . . . . . . . . . . . 15 5 ∈ ℂ
616615a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 5 ∈ ℂ)
617616, 207mulcld 11109 . . . . . . . . . . . . 13 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618617mulid1d 11106 . . . . . . . . . . . 12 (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619618eqcomd 2744 . . . . . . . . . . 11 (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620 eqidd 2739 . . . . . . . . . . . . . 14 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621 df-5 12153 . . . . . . . . . . . . . . . . . . 19 5 = (4 + 1)
622621a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 5 = (4 + 1))
623622oveq2d 7366 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
62418, 91, 77expaddd 13980 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625623, 624eqtrd 2778 . . . . . . . . . . . . . . . 16 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626476oveq2d 7366 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627625, 626eqtrd 2778 . . . . . . . . . . . . . . 15 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628627oveq1d 7365 . . . . . . . . . . . . . 14 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629620, 628eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630117, 18, 2mulassd 11112 . . . . . . . . . . . . 13 (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631629, 630eqtrd 2778 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
63218, 2mulcomd 11110 . . . . . . . . . . . . 13 (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633632oveq2d 7366 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634631, 633eqtrd 2778 . . . . . . . . . . 11 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635619, 634oveq12d 7368 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
6362, 18mulcld 11109 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
6372, 18, 11, 26mulne0d 11741 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638186, 117, 53, 636, 120, 637divmuldivd 11906 . . . . . . . . . . 11 (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639638eqcomd 2744 . . . . . . . . . 10 (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640635, 639eqtrd 2778 . . . . . . . . 9 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641206, 207, 117, 120divassd 11900 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642641oveq1d 7365 . . . . . . . . 9 (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643640, 642eqtrd 2778 . . . . . . . 8 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
64412, 18, 26, 77expdivd 13992 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645644eqcomd 2744 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646645oveq2d 7366 . . . . . . . . 9 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647646oveq1d 7365 . . . . . . . 8 (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648643, 647eqtrd 2778 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649610oveq1d 7365 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650649oveq2d 7366 . . . . . . . 8 (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651650oveq1d 7365 . . . . . . 7 (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652648, 651eqtrd 2778 . . . . . 6 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653342, 77expcld 13978 . . . . . . . . . 10 (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654616, 653mulcld 11109 . . . . . . . . 9 (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
65539rpne0d 12891 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
6562, 18, 655, 26mulne0d 11741 . . . . . . . . . 10 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657636, 656reccld 11858 . . . . . . . . 9 (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658654, 657mulcld 11109 . . . . . . . 8 (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659658addid1d 11289 . . . . . . 7 (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660659eqcomd 2744 . . . . . 6 (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661652, 660eqtrd 2778 . . . . 5 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662614, 661oveq12d 7368 . . . 4 (𝜑 → ((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)))
663662oveq2d 7366 . . 3 (𝜑 → (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 12214 . . . . . . 7 1 = (2 − 1)
665664a1i 11 . . . . . 6 (𝜑 → 1 = (2 − 1))
666665oveq2d 7366 . . . . 5 (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667666oveq1d 7365 . . . 4 (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668667oveq2d 7366 . . 3 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669663, 668oveq12d 7368 . 2 (𝜑 → ((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 12172 . . . . 5 4 ∈ ℂ
671670a1i 11 . . . 4 (𝜑 → 4 ∈ ℂ)
672671, 117, 581, 2, 120, 655divmuldivd 11906 . . 3 (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673672eqcomd 2744 . 2 (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674608, 669, 6733brtr3d 5135 1 (𝜑 → ((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) / 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107   class class class wbr 5104  cfv 6492  (class class class)co 7350  cc 10983  cr 10984  0cc0 10985  1c1 10986   + caddc 10988   · cmul 10990   < clt 11123  cle 11124  cmin 11319  -cneg 11320   / cdiv 11746  cn 12087  2c2 12142  3c3 12143  4c4 12144  5c5 12145  6c6 12146  7c7 12147  9c9 12149  0cn0 12347  cz 12433  cdc 12551  cuz 12696  +crp 12844  cexp 13896  eceu 15880  logclog 25833   logb clogb 26037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064  ax-mulf 11065
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-om 7794  df-1st 7912  df-2nd 7913  df-supp 8061  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-ixp 8770  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fsupp 9240  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155  df-8 12156  df-9 12157  df-n0 12348  df-z 12434  df-dec 12552  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ioc 13198  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-mod 13704  df-seq 13836  df-exp 13897  df-fac 14102  df-bc 14131  df-hash 14159  df-shft 14886  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-limsup 15288  df-clim 15305  df-rlim 15306  df-sum 15506  df-ef 15885  df-e 15886  df-sin 15887  df-cos 15888  df-pi 15890  df-struct 16954  df-sets 16971  df-slot 16989  df-ndx 17001  df-base 17019  df-ress 17048  df-plusg 17081  df-mulr 17082  df-starv 17083  df-sca 17084  df-vsca 17085  df-ip 17086  df-tset 17087  df-ple 17088  df-ds 17090  df-unif 17091  df-hom 17092  df-cco 17093  df-rest 17239  df-topn 17240  df-0g 17258  df-gsum 17259  df-topgen 17260  df-pt 17261  df-prds 17264  df-xrs 17319  df-qtop 17324  df-imas 17325  df-xps 17327  df-mre 17401  df-mrc 17402  df-acs 17404  df-mgm 18432  df-sgrp 18481  df-mnd 18492  df-submnd 18537  df-mulg 18807  df-cntz 19030  df-cmn 19494  df-psmet 20712  df-xmet 20713  df-met 20714  df-bl 20715  df-mopn 20716  df-fbas 20717  df-fg 20718  df-cnfld 20721  df-top 22166  df-topon 22183  df-topsp 22205  df-bases 22219  df-cld 22293  df-ntr 22294  df-cls 22295  df-nei 22372  df-lp 22410  df-perf 22411  df-cn 22501  df-cnp 22502  df-haus 22589  df-tx 22836  df-hmeo 23029  df-fil 23120  df-fm 23212  df-flim 23213  df-flf 23214  df-xms 23596  df-ms 23597  df-tms 23598  df-cncf 24164  df-limc 25153  df-dv 25154  df-log 25835  df-cxp 25836  df-logb 26038
This theorem is referenced by:  aks4d1p1p5  40428
  Copyright terms: Public domain W3C validator