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 39721
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 10747 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
3 0red 10722 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4 4re 11800 . . . . . . . . . . . . . . 15 4 ∈ ℝ
54a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
6 4pos 11823 . . . . . . . . . . . . . . 15 0 < 4
76a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 4)
8 aks4d1p1p7.2 . . . . . . . . . . . . . 14 (𝜑 → 4 ≤ 𝐴)
93, 5, 1, 7, 8ltletrd 10878 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝐴)
103, 9ltned 10854 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 𝐴)
1110necomd 2989 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
122, 11logcld 25314 . . . . . . . . . 10 (𝜑 → (log‘𝐴) ∈ ℂ)
13 2cnd 11794 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
14 2pos 11819 . . . . . . . . . . . . . 14 0 < 2
1514a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 < 2)
163, 15ltned 10854 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 2)
1716necomd 2989 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
1813, 17logcld 25314 . . . . . . . . . 10 (𝜑 → (log‘2) ∈ ℂ)
19 1lt2 11887 . . . . . . . . . . . . . 14 1 < 2
20 2rp 12477 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
21 loggt0b 25375 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
2220, 21ax-mp 5 . . . . . . . . . . . . . 14 (0 < (log‘2) ↔ 1 < 2)
2319, 22mpbir 234 . . . . . . . . . . . . 13 0 < (log‘2)
2423a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < (log‘2))
253, 24ltned 10854 . . . . . . . . . . 11 (𝜑 → 0 ≠ (log‘2))
2625necomd 2989 . . . . . . . . . 10 (𝜑 → (log‘2) ≠ 0)
27 5nn0 11996 . . . . . . . . . . 11 5 ∈ ℕ0
2827a1i 11 . . . . . . . . . 10 (𝜑 → 5 ∈ ℕ0)
2912, 18, 26, 28expdivd 13616 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
3029oveq1d 7185 . . . . . . . 8 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
3130oveq1d 7185 . . . . . . 7 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
3231oveq2d 7186 . . . . . 6 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
3332oveq1d 7185 . . . . 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 7186 . . . 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 7185 . . 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 11790 . . . . . . 7 2 ∈ ℝ
3736a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
38 1red 10720 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
391, 9elrpd 12511 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
4039relogcld 25366 . . . . . . . . . . . 12 (𝜑 → (log‘𝐴) ∈ ℝ)
4140, 28reexpcld 13619 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
4220a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ+)
4342relogcld 25366 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ)
4443, 28reexpcld 13619 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ)
4528nn0zd 12166 . . . . . . . . . . . 12 (𝜑 → 5 ∈ ℤ)
4618, 26, 45expne0d 13608 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ≠ 0)
4741, 44, 46redivcld 11546 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
4847, 38readdcld 10748 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
4948, 43remulcld 10749 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
5012, 28expcld 13602 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
5118, 28expcld 13602 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℂ)
5250, 51, 46divcld 11494 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53 1cnd 10714 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
5452, 53addcld 10738 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
5519a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 2)
5637, 55rplogcld 25372 . . . . . . . . . . . . . 14 (𝜑 → (log‘2) ∈ ℝ+)
5756, 45rpexpcld 13700 . . . . . . . . . . . . 13 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58 1re 10719 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
59 3nn0 11994 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℕ0
6058, 59nn0addge2i 12025 . . . . . . . . . . . . . . . . . 18 1 ≤ (3 + 1)
6160a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≤ (3 + 1))
62 df-4 11781 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
6361, 62breqtrrdi 5072 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 4)
6438, 5, 1, 63, 8letrd 10875 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝐴)
651, 64logge0d 25373 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (log‘𝐴))
6640, 28, 65expge0d 13620 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ ((log‘𝐴)↑5))
6741, 57, 66divge0d 12554 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
6847ltp1d 11648 . . . . . . . . . . . 12 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
693, 47, 48, 67, 68lelttrd 10876 . . . . . . . . . . 11 (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
703, 69ltned 10854 . . . . . . . . . 10 (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
7170necomd 2989 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
7254, 18, 71, 26mulne0d 11370 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
7338, 49, 72redivcld 11546 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74 5re 11803 . . . . . . . . . 10 5 ∈ ℝ
7574a1i 11 . . . . . . . . 9 (𝜑 → 5 ∈ ℝ)
76 4nn0 11995 . . . . . . . . . . 11 4 ∈ ℕ0
7776a1i 11 . . . . . . . . . 10 (𝜑 → 4 ∈ ℕ0)
7840, 77reexpcld 13619 . . . . . . . . 9 (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
7975, 78remulcld 10749 . . . . . . . 8 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
8044, 1remulcld 10749 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
8151, 2, 46, 11mulne0d 11370 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
8279, 80, 81redivcld 11546 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
8373, 82remulcld 10749 . . . . . 6 (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
8437, 83remulcld 10749 . . . . 5 (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
8543resqcld 13703 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℝ)
86 2z 12095 . . . . . . . . 9 2 ∈ ℤ
8786a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
8818, 26, 87expne0d 13608 . . . . . . 7 (𝜑 → ((log‘2)↑2) ≠ 0)
8937, 85, 88redivcld 11546 . . . . . 6 (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90 1nn0 11992 . . . . . . . . 9 1 ∈ ℕ0
9190a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℕ0)
9240, 91reexpcld 13619 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
9392, 1, 11redivcld 11546 . . . . . 6 (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
9489, 93remulcld 10749 . . . . 5 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
9584, 94readdcld 10748 . . . 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 10749 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97 1lt4 11892 . . . . . . . . . . . . . . . 16 1 < 4
9897a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 4)
9938, 5, 1, 98, 8ltletrd 10878 . . . . . . . . . . . . . 14 (𝜑 → 1 < 𝐴)
100 loggt0b 25375 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10139, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10299, 101mpbird 260 . . . . . . . . . . . . 13 (𝜑 → 0 < (log‘𝐴))
1033, 102ltned 10854 . . . . . . . . . . . 12 (𝜑 → 0 ≠ (log‘𝐴))
104103necomd 2989 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ≠ 0)
10512, 104, 45expne0d 13608 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ≠ 0)
10650, 51, 105, 46divne0d 11510 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
10752, 18, 106, 26mulne0d 11370 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
10838, 96, 107redivcld 11546 . . . . . . 7 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109108, 82remulcld 10749 . . . . . 6 (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
11037, 109remulcld 10749 . . . . 5 (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111110, 94readdcld 10748 . . . 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 13619 . . . . . 6 (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
1145, 113remulcld 10749 . . . . 5 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
11543, 77reexpcld 13619 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℝ)
116115, 1remulcld 10749 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
11718, 77expcld 13602 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℂ)
118 4z 12097 . . . . . . . 8 4 ∈ ℤ
119118a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℤ)
12018, 26, 119expne0d 13608 . . . . . 6 (𝜑 → ((log‘2)↑4) ≠ 0)
121117, 2, 120, 11mulne0d 11370 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122114, 116, 121redivcld 11546 . . . 4 (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123 0le2 11818 . . . . . . 7 0 ≤ 2
124123a1i 11 . . . . . 6 (𝜑 → 0 ≤ 2)
12557, 39rpmulcld 12530 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
12628nn0ge0d 12039 . . . . . . . . 9 (𝜑 → 0 ≤ 5)
12740, 77, 65expge0d 13620 . . . . . . . . 9 (𝜑 → 0 ≤ ((log‘𝐴)↑4))
12875, 78, 126, 127mulge0d 11295 . . . . . . . 8 (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
12979, 125, 128divge0d 12554 . . . . . . 7 (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
1301, 99rplogcld 25372 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ∈ ℝ+)
131130, 45rpexpcld 13700 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132131, 57rpdivcld 12531 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133132, 56rpmulcld 12530 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
13424, 22sylib 221 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
13537, 134rplogcld 25372 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ+)
136135, 45rpexpcld 13700 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
13741, 136, 66divge0d 12554 . . . . . . . . . 10 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
13847, 137ge0p1rpd 12544 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139138, 135rpmulcld 12530 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140 0le1 11241 . . . . . . . . 9 0 ≤ 1
141140a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ 1)
142135rpred 12514 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℝ)
143135rpge0d 12518 . . . . . . . . 9 (𝜑 → 0 ≤ (log‘2))
14447lep1d 11649 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
14547, 48, 142, 143, 144lemul1ad 11657 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146133, 139, 38, 141, 145lediv2ad 12536 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ≤ (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))))
14773, 108, 82, 129, 146lemul1ad 11657 . . . . . 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 11658 . . . . 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 11332 . . . 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 11531 . . . . . . . . . 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 7186 . . . . . . . 8 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153152oveq1d 7185 . . . . . . 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 7186 . . . . . 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 13600 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℂ)
15612, 91expcld 13602 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
15713, 155, 156, 2, 88, 11divmuldivd 11535 . . . . . 6 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158154, 157oveq12d 7188 . . . . 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 10739 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
16050, 18, 105, 26mulne0d 11370 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
16153, 159, 51, 160, 46divdiv2d 11526 . . . . . . . . . 10 (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162161oveq1d 7185 . . . . . . . . 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 7186 . . . . . . . 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 10739 . . . . . . . . . . 11 (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165164, 159, 160divcld 11494 . . . . . . . . . 10 (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
16682recnd 10747 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
16713, 165, 166mulassd 10742 . . . . . . . . 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 2773 . . . . . . 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 7185 . . . . . 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 11529 . . . . . . . . . 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 7185 . . . . . . . 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 7185 . . . . . . 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 10742 . . . . . . . . . . . 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 7185 . . . . . . . . . 10 (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178177oveq1d 7185 . . . . . . . . 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 7185 . . . . . . . 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 10736 . . . . . . . . . . . . 13 (𝜑 → (2 · 1) = 2)
181180oveq1d 7185 . . . . . . . . . . . 12 (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182181oveq1d 7185 . . . . . . . . . . 11 (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183182oveq1d 7185 . . . . . . . . . 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 7185 . . . . . . . . 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 10739 . . . . . . . . . . . 12 (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
18679recnd 10747 . . . . . . . . . . . 12 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
18751, 2mulcld 10739 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188185, 159, 186, 187, 160, 81divmuldivd 11535 . . . . . . . . . . 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 7185 . . . . . . . . . 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 10742 . . . . . . . . . . . . 13 (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191190oveq2d 7186 . . . . . . . . . . . 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 7185 . . . . . . . . . . 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 10740 . . . . . . . . . . . . . 14 (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
19418, 51, 2mulassd 10742 . . . . . . . . . . . . . . . 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 7186 . . . . . . . . . . . . . 14 (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197193, 196oveq12d 7188 . . . . . . . . . . . . 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 7185 . . . . . . . . . . . 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 10739 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200199, 2mulcld 10739 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
20118, 51, 26, 46mulne0d 11370 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202199, 2, 201, 11mulne0d 11370 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203186, 50, 185, 200, 105, 202divmuldivd 11535 . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . 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 10747 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℂ)
20778recnd 10747 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208206, 207, 50, 105divassd 11529 . . . . . . . . . . . . . . . 16 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209194oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210208, 209oveq12d 7188 . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . 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 12166 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 4 ∈ ℤ)
21312, 104, 45, 212expsubd 13613 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214213eqcomd 2744 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215 4p1e5 11862 . . . . . . . . . . . . . . . . . . . . . . . . 25 (4 + 1) = 5
21674recni 10733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 5 ∈ ℂ
2174recni 10733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 4 ∈ ℂ
218 ax-1cn 10673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
219216, 217, 218subaddi 11051 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((5 − 4) = 1 ↔ (4 + 1) = 5)
220215, 219mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . 24 (5 − 4) = 1
221220a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 − 4) = 1)
22253subid1d 11064 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 − 0) = 1)
223221, 222eqtr4d 2776 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 − 4) = (1 − 0))
224206, 217jctir 524 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225 0cnd 10712 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 ∈ ℂ)
22653, 225jca 515 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227 subeqrev 11140 . . . . . . . . . . . . . . . . . . . . . . 23 (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228224, 226, 227syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229223, 228mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (4 − 5) = (0 − 1))
230 df-neg 10951 . . . . . . . . . . . . . . . . . . . . 21 -1 = (0 − 1)
231229, 230eqtr4di 2791 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (4 − 5) = -1)
232231oveq2d 7186 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233214, 232eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234233oveq2d 7186 . . . . . . . . . . . . . . . . 17 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
23513, 18, 51, 187, 26, 81divmuldivd 11535 . . . . . . . . . . . . . . . . . 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 7188 . . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . 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 12094 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℤ)
24012, 104, 239expnegd 13609 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241240oveq2d 7186 . . . . . . . . . . . . . . . . . 18 (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
24251, 51, 2, 46, 11divdiv1d 11525 . . . . . . . . . . . . . . . . . . . 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 7186 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245241, 244oveq12d 7188 . . . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . . 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 13608 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248206, 53, 156, 247divassd 11529 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249248eqcomd 2744 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
25051, 46dividd 11492 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251250oveq1d 7185 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252251oveq2d 7186 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253249, 252oveq12d 7188 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) = (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))))
254253oveq1d 7185 . . . . . . . . . . . . . . . . 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 10736 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (5 · 1) = 5)
256255oveq1d 7185 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
25713, 18, 53, 2, 26, 11divmuldivd 11535 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258256, 257oveq12d 7188 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259258oveq1d 7185 . . . . . . . . . . . . . . . . . 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 2833 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (2 · 1) ∈ ℂ)
26118, 2mulcld 10739 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
26218, 2, 26, 11mulne0d 11370 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263206, 156, 260, 261, 247, 262divmuldivd 11535 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264180oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · (2 · 1)) = (5 · 2))
265264oveq1d 7185 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266263, 265eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267266oveq1d 7185 . . . . . . . . . . . . . . . . . . 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 12279 . . . . . . . . . . . . . . . . . . . . . . 23 (5 · 2) = 10
269268a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · 2) = 10)
270269oveq1d 7185 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271270oveq1d 7185 . . . . . . . . . . . . . . . . . . . 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 12197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 10 ∈ ℕ0
273272nn0cni 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 10 ∈ ℂ
274273a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑10 ∈ ℂ)
275274mulid1d 10736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (10 · 1) = 10)
276275oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 / (((log‘𝐴)↑1) · (log‘2))))
27713, 156mulcld 10739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278277, 155, 88divcld 11494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279278mulid2d 10737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280276, 279oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ∈ ℂ)
28218, 26, 239expne0d 13608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ≠ 0)
283277, 281, 282divcld 11494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284283mulid1d 10736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285284oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286 10re 12198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 10 ∈ ℝ
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑10 ∈ ℝ)
288287, 40, 104redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ∈ ℝ)
28940, 43, 26redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290289, 91reexpcld 13619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
29137, 290remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292288, 291readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293287, 291readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
29443, 112reexpcld 13619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ∈ ℝ)
295 3z 12096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3 ∈ ℤ
296295a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → 3 ∈ ℤ)
29718, 26, 296expne0d 13608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ≠ 0)
298113, 294, 297redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
2995, 298remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300 ere 15534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 e ∈ ℝ
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e ∈ ℝ)
302112nn0red 12037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 ∈ ℝ)
303 egt2lt3 15651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (2 < e ∧ e < 3)
304303simpri 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 e < 3
305304a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → e < 3)
306 3lt4 11890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3 < 4
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 3 < 4)
308302, 5, 1, 307, 8ltletrd 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 < 𝐴)
309301, 302, 1, 305, 308lttrd 10879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e < 𝐴)
310301, 1, 309ltled 10866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → e ≤ 𝐴)
311301, 1lenltd 10864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312310, 311mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ¬ 𝐴 < e)
313 loglt1b 25377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
31439, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315312, 314mtbird 328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ¬ (log‘𝐴) < 1)
31638, 40lenltd 10864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317315, 316mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → 1 ≤ (log‘𝐴))
318 10nn 12195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 10 ∈ ℕ
319318a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑10 ∈ ℕ)
320 nnledivrp 12584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
321319, 130, 320syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
322317, 321mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ≤ 10)
323288, 287, 291, 322leadd1dd 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
32438, 55gtned 10853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≠ 1)
32537, 15, 1, 9, 324relogbcld 39620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ∈ ℝ)
326325, 91reexpcld 13619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
32742, 55jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328 logbgt0b 25531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
32939, 327, 328syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
33099, 329mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 0 < (2 logb 𝐴))
331325, 330elrpd 12511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332331, 239rpexpcld 13700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333332rpne0d 12519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334287, 326, 333redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335334, 37readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336 sq2 13652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (2↑2) = 4
337336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2↑2) = 4)
338337, 5eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ∈ ℝ)
3395, 338remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ∈ ℝ)
340325resqcld 13703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
3415, 340remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342325recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℂ)
343342exp1d 13597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344343oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (10 / ((2 logb 𝐴)↑1)) = (10 / (2 logb 𝐴)))
345344oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) = ((10 / (2 logb 𝐴)) + 2))
346345, 335eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347287rehalfcld 11963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
348347, 37readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ∈ ℝ)
349344, 334eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ∈ ℝ)
350287, 37, 17redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
351272nn0ge0i 12003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 0 ≤ 10
352351a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 0 ≤ 10)
35342, 324, 87relogbexpd 39621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 logb (2↑2)) = 2)
354353eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 = (2 logb (2↑2)))
355337oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356354, 355eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 2 = (2 logb 4))
35737leidd 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 ≤ 2)
35887, 357, 5, 7, 1, 9, 8logblebd 39623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359356, 358eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≤ (2 logb 𝐴))
36042, 331, 287, 352, 359lediv2ad 12536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ≤ (10 / 2))
361349, 350, 37, 360leadd1dd 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ ((10 / 2) + 2))
362 1nn 11727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 1 ∈ ℕ
363 6nn0 11997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6 ∈ ℕ0
364 2nn0 11993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2 ∈ ℕ0
36527, 364nn0addcli 12013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ∈ ℕ0
366 5p2e7 11872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (5 + 2) = 7
367 7re 11809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 7 ∈ ℝ
368367, 364nn0addge1i 12024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 7 ≤ (7 + 2)
369 7p2e9 11877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (7 + 2) = 9
370368, 369breqtri 5055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7 ≤ 9
371366, 370eqbrtri 5051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ≤ 9
372362, 363, 365, 371declei 12215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (5 + 2) ≤ 16
373372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) ≤ 16)
374206, 13, 274, 17ldiv 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((5 · 2) = 10 ↔ 5 = (10 / 2)))
375269, 374mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 5 = (10 / 2))
376375oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) = ((10 / 2) + 2))
377 4t4e16 12278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (4 · 4) = 16
378377eqcomi 2747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 16 = (4 · 4)
379378a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑16 = (4 · 4))
380337eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 4 = (2↑2))
381380oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (4 · 4) = (4 · (2↑2)))
382379, 381eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑16 = (4 · (2↑2)))
383373, 376, 3823brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ≤ (4 · (2↑2)))
384346, 348, 339, 361, 383letrd 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385345, 384eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
3863, 5, 7ltled 10866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → 0 ≤ 4)
387364a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ ℕ0)
38837, 325, 387, 124, 359leexp1ad 39619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389338, 340, 5, 386, 388lemul2ad 11658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390335, 339, 341, 385, 389letrd 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
39137, 326remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392391recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393326recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394274, 392, 393, 333divdird 11532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))))
39513, 393, 393, 333divassd 11529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396395oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398397oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399398, 180eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400399oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
401396, 400eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
402394, 401eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 + 1) = 3
405404a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 + 1) = 3)
406302recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 3 ∈ ℂ)
407406, 53, 13subadd2d 11094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408405, 407mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (3 − 1) = 2)
409408eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 2 = (3 − 1))
410409oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411410oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
4123, 330gtned 10853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ≠ 0)
413342, 412, 239, 296expsubd 13613 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414413oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415411, 414eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 4 ∈ ℂ)
417325, 112reexpcld 13619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418417recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419416, 418, 393, 333divassd 11529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422390, 403, 4213brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423287, 391readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
4245, 417remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425423, 424, 332lediv1d 12560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
42787uzidd 12340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ (ℤ‘2))
428427, 39jca 515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+))
429 relogbval 25510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431430oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432431oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433432oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) = (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434430oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
43512, 18, 26, 112expdivd 13616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436434, 435eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437436oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438426, 433, 4373brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439292, 293, 299, 323, 438letrd 10875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
44012exp1d 13597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441440eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442441oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 / (log‘𝐴)) = (10 / ((log‘𝐴)↑1)))
44313, 156, 281, 282divassd 11529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
44412, 18, 26, 91expdivd 13616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445444eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446445oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447443, 446eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450113recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
45118, 112expcld 13602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑3) ∈ ℂ)
452416, 450, 451, 297divassd 11529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455285, 454eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456281, 282dividd 11492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457456eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458457oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461460oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463462, 451, 297divcld 11494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464463mulid1d 10736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / ((log‘𝐴)↑1)) ∈ ℂ)
468467mulid1d 10736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = (10 / ((log‘𝐴)↑1)))
469468eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · 1))
47018, 26dividd 11492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2) / (log‘2)) = 1)
471470eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = ((log‘2) / (log‘2)))
472471oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473469, 472eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474274, 156, 18, 18, 247, 26divmuldivd 11535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475473, 474eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
47618exp1d 13597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑1) = (log‘2))
477476oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478 df-2 11779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2 = (1 + 1)
479478a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → 2 = (1 + 1))
480479oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
48118, 91, 91expaddd 13604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482480, 481eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483482eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484477, 483oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)))
485475, 484oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488471, 487eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489488oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490476, 18eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ∈ ℂ)
491476, 26eqnetrd 3001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ≠ 0)
492462, 451, 18, 490, 297, 491divmuldivd 11535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494466, 485, 4933brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496156, 18, 247, 26mulne0d 11370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497274, 18, 495, 496div23d 11531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498277, 18, 155, 88div23d 11531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499497, 498oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
50218, 91, 112expaddd 13604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503501, 502eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504503eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505504oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)))
506494, 499, 5053brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508287, 507, 496redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509508recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510509, 278, 18adddird 10744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((log‘2)↑4) ≠ 0)
513462, 18, 117, 512div23d 11531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514506, 511, 5133brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
51537, 92remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516515, 85, 88redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517508, 516readdcld 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518114, 115, 120redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519517, 518, 135lemul1d 12557 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521280, 520eqbrtrd 5052 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
522274, 53, 495, 496divassd 11529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
52353, 277, 155, 88div12d 11530 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524522, 523oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . . 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 10736 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526525eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527526oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528521, 524, 5273brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))) ≤ (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
5292, 11dividd 11492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴 / 𝐴) = 1)
530529eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 1 = (𝐴 / 𝐴))
531530oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
5322, 2, 495, 11, 496divdiv1d 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533531, 532eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534533oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537536oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538535, 537eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539534, 538oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . . 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 11529 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541528, 539, 5403brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
5422, 495mulcomd 10740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543156, 18, 2mulassd 10742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544542, 543eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545544oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546545oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
5472, 2, 155, 11, 88divdiv1d 11525 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
5482, 155mulcomd 10740 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549548oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550547, 549eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551550oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552546, 551oveq12d 7188 . . . . . . . . . . . . . . . . . . . . . . . 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 7185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555553, 554eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556555oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557541, 552, 5563brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558156, 261mulcld 10739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559156, 261, 247, 262mulne0d 11370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560274, 558, 2, 559div32d 11517 . . . . . . . . . . . . . . . . . . . . . . . . 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 10739 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563155, 2, 88, 11mulne0d 11370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564277, 562, 2, 563div32d 11517 . . . . . . . . . . . . . . . . . . . . . . . . 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 7188 . . . . . . . . . . . . . . . . . . . . . . 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 11525 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
5682, 117mulcomd 10740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569568oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570567, 569eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571570oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572557, 566, 5713brtr3d 5061 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
57343, 1remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
57492, 573remulcld 10749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575287, 574, 559redivcld 11546 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576575recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577157, 94eqeltrrd 2834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578577recnd 10747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579576, 578, 2adddird 10744 . . . . . . . . . . . . . . . . . . . . . . 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 13602 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582416, 581mulcld 10739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583117, 2mulcld 10739 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584117, 2, 512, 11mulne0d 11370 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585582, 583, 2, 584div32d 11517 . . . . . . . . . . . . . . . . . . . . . . 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 5061 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588575, 577readdcld 10748 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589588, 122, 39lemul1d 12557 . . . . . . . . . . . . . . . . . . . . 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 260 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591271, 590eqbrtrd 5052 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592267, 591eqbrtrd 5052 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593259, 592eqbrtrd 5052 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
594254, 593eqbrtrd 5052 . . . . . . . . . . . . . . . 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 5052 . . . . . . . . . . . . . . 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 5052 . . . . . . . . . . . . . 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 5052 . . . . . . . . . . . . 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 5052 . . . . . . . . . . . 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 5052 . . . . . . . . . . 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 5052 . . . . . . . . . 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 5052 . . . . . . . . 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 5052 . . . . . . . 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 5052 . . . . . . 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 5052 . . . . . 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 5052 . . . . 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 5052 . . . 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 10875 . . 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 5052 . 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 587 . . . . . . . . . 10 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610609eqcomd 2744 . . . . . . . . 9 (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611610oveq1d 7185 . . . . . . . 8 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612611oveq1d 7185 . . . . . . 7 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613612oveq1d 7185 . . . . . 6 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614613oveq2d 7186 . . . . 5 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615 5cn 11804 . . . . . . . . . . . . . . 15 5 ∈ ℂ
616615a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 5 ∈ ℂ)
617616, 207mulcld 10739 . . . . . . . . . . . . 13 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618617mulid1d 10736 . . . . . . . . . . . 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 11782 . . . . . . . . . . . . . . . . . . 19 5 = (4 + 1)
622621a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 5 = (4 + 1))
623622oveq2d 7186 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
62418, 91, 77expaddd 13604 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625623, 624eqtrd 2773 . . . . . . . . . . . . . . . 16 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626476oveq2d 7186 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627625, 626eqtrd 2773 . . . . . . . . . . . . . . 15 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628627oveq1d 7185 . . . . . . . . . . . . . 14 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629620, 628eqtrd 2773 . . . . . . . . . . . . 13 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630117, 18, 2mulassd 10742 . . . . . . . . . . . . 13 (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631629, 630eqtrd 2773 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
63218, 2mulcomd 10740 . . . . . . . . . . . . 13 (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633632oveq2d 7186 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634631, 633eqtrd 2773 . . . . . . . . . . 11 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635619, 634oveq12d 7188 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
6362, 18mulcld 10739 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
6372, 18, 11, 26mulne0d 11370 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638186, 117, 53, 636, 120, 637divmuldivd 11535 . . . . . . . . . . 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 2773 . . . . . . . . 9 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641206, 207, 117, 120divassd 11529 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642641oveq1d 7185 . . . . . . . . 9 (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643640, 642eqtrd 2773 . . . . . . . 8 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
64412, 18, 26, 77expdivd 13616 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645644eqcomd 2744 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646645oveq2d 7186 . . . . . . . . 9 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647646oveq1d 7185 . . . . . . . 8 (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648643, 647eqtrd 2773 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649610oveq1d 7185 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650649oveq2d 7186 . . . . . . . 8 (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651650oveq1d 7185 . . . . . . 7 (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652648, 651eqtrd 2773 . . . . . 6 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653342, 77expcld 13602 . . . . . . . . . 10 (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654616, 653mulcld 10739 . . . . . . . . 9 (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
65539rpne0d 12519 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
6562, 18, 655, 26mulne0d 11370 . . . . . . . . . 10 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657636, 656reccld 11487 . . . . . . . . 9 (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658654, 657mulcld 10739 . . . . . . . 8 (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659658addid1d 10918 . . . . . . 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 2773 . . . . 5 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662614, 661oveq12d 7188 . . . 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 7186 . . 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 11843 . . . . . . 7 1 = (2 − 1)
665664a1i 11 . . . . . 6 (𝜑 → 1 = (2 − 1))
666665oveq2d 7186 . . . . 5 (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667666oveq1d 7185 . . . 4 (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668667oveq2d 7186 . . 3 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669663, 668oveq12d 7188 . 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 11801 . . . . 5 4 ∈ ℂ
671670a1i 11 . . . 4 (𝜑 → 4 ∈ ℂ)
672671, 117, 581, 2, 120, 655divmuldivd 11535 . . 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 5061 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 209  wa 399   = wceq 1542  wcel 2114   class class class wbr 5030  cfv 6339  (class class class)co 7170  cc 10613  cr 10614  0cc0 10615  1c1 10616   + caddc 10618   · cmul 10620   < clt 10753  cle 10754  cmin 10948  -cneg 10949   / cdiv 11375  cn 11716  2c2 11771  3c3 11772  4c4 11773  5c5 11774  6c6 11775  7c7 11776  9c9 11778  0cn0 11976  cz 12062  cdc 12179  cuz 12324  +crp 12472  cexp 13521  eceu 15508  logclog 25298   logb clogb 25502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-inf2 9177  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693  ax-addf 10694  ax-mulf 10695
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-of 7425  df-om 7600  df-1st 7714  df-2nd 7715  df-supp 7857  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-er 8320  df-map 8439  df-pm 8440  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-fsupp 8907  df-fi 8948  df-sup 8979  df-inf 8980  df-oi 9047  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-q 12431  df-rp 12473  df-xneg 12590  df-xadd 12591  df-xmul 12592  df-ioo 12825  df-ioc 12826  df-ico 12827  df-icc 12828  df-fz 12982  df-fzo 13125  df-fl 13253  df-mod 13329  df-seq 13461  df-exp 13522  df-fac 13726  df-bc 13755  df-hash 13783  df-shft 14516  df-cj 14548  df-re 14549  df-im 14550  df-sqrt 14684  df-abs 14685  df-limsup 14918  df-clim 14935  df-rlim 14936  df-sum 15136  df-ef 15513  df-e 15514  df-sin 15515  df-cos 15516  df-pi 15518  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-sets 16593  df-ress 16594  df-plusg 16681  df-mulr 16682  df-starv 16683  df-sca 16684  df-vsca 16685  df-ip 16686  df-tset 16687  df-ple 16688  df-ds 16690  df-unif 16691  df-hom 16692  df-cco 16693  df-rest 16799  df-topn 16800  df-0g 16818  df-gsum 16819  df-topgen 16820  df-pt 16821  df-prds 16824  df-xrs 16878  df-qtop 16883  df-imas 16884  df-xps 16886  df-mre 16960  df-mrc 16961  df-acs 16963  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-submnd 18073  df-mulg 18343  df-cntz 18565  df-cmn 19026  df-psmet 20209  df-xmet 20210  df-met 20211  df-bl 20212  df-mopn 20213  df-fbas 20214  df-fg 20215  df-cnfld 20218  df-top 21645  df-topon 21662  df-topsp 21684  df-bases 21697  df-cld 21770  df-ntr 21771  df-cls 21772  df-nei 21849  df-lp 21887  df-perf 21888  df-cn 21978  df-cnp 21979  df-haus 22066  df-tx 22313  df-hmeo 22506  df-fil 22597  df-fm 22689  df-flim 22690  df-flf 22691  df-xms 23073  df-ms 23074  df-tms 23075  df-cncf 23630  df-limc 24618  df-dv 24619  df-log 25300  df-cxp 25301  df-logb 25503
This theorem is referenced by:  aks4d1p1p5  39722
  Copyright terms: Public domain W3C validator