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 40089
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 11012 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℂ)
3 0red 10987 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4 4re 12066 . . . . . . . . . . . . . . 15 4 ∈ ℝ
54a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 ∈ ℝ)
6 4pos 12089 . . . . . . . . . . . . . . 15 0 < 4
76a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 4)
8 aks4d1p1p7.2 . . . . . . . . . . . . . 14 (𝜑 → 4 ≤ 𝐴)
93, 5, 1, 7, 8ltletrd 11144 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝐴)
103, 9ltned 11120 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 𝐴)
1110necomd 3000 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
122, 11logcld 25735 . . . . . . . . . 10 (𝜑 → (log‘𝐴) ∈ ℂ)
13 2cnd 12060 . . . . . . . . . . 11 (𝜑 → 2 ∈ ℂ)
14 2pos 12085 . . . . . . . . . . . . . 14 0 < 2
1514a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 < 2)
163, 15ltned 11120 . . . . . . . . . . . 12 (𝜑 → 0 ≠ 2)
1716necomd 3000 . . . . . . . . . . 11 (𝜑 → 2 ≠ 0)
1813, 17logcld 25735 . . . . . . . . . 10 (𝜑 → (log‘2) ∈ ℂ)
19 1lt2 12153 . . . . . . . . . . . . . 14 1 < 2
20 2rp 12744 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
21 loggt0b 25796 . . . . . . . . . . . . . . 15 (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
2220, 21ax-mp 5 . . . . . . . . . . . . . 14 (0 < (log‘2) ↔ 1 < 2)
2319, 22mpbir 230 . . . . . . . . . . . . 13 0 < (log‘2)
2423a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 < (log‘2))
253, 24ltned 11120 . . . . . . . . . . 11 (𝜑 → 0 ≠ (log‘2))
2625necomd 3000 . . . . . . . . . 10 (𝜑 → (log‘2) ≠ 0)
27 5nn0 12262 . . . . . . . . . . 11 5 ∈ ℕ0
2827a1i 11 . . . . . . . . . 10 (𝜑 → 5 ∈ ℕ0)
2912, 18, 26, 28expdivd 13887 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
3029oveq1d 7299 . . . . . . . 8 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
3130oveq1d 7299 . . . . . . 7 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
3231oveq2d 7300 . . . . . 6 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
3332oveq1d 7299 . . . . 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 7300 . . . 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 7299 . . 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 12056 . . . . . . 7 2 ∈ ℝ
3736a1i 11 . . . . . 6 (𝜑 → 2 ∈ ℝ)
38 1red 10985 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
391, 9elrpd 12778 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℝ+)
4039relogcld 25787 . . . . . . . . . . . 12 (𝜑 → (log‘𝐴) ∈ ℝ)
4140, 28reexpcld 13890 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
4220a1i 11 . . . . . . . . . . . . 13 (𝜑 → 2 ∈ ℝ+)
4342relogcld 25787 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ)
4443, 28reexpcld 13890 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ)
4528nn0zd 12433 . . . . . . . . . . . 12 (𝜑 → 5 ∈ ℤ)
4618, 26, 45expne0d 13879 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ≠ 0)
4741, 44, 46redivcld 11812 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
4847, 38readdcld 11013 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
4948, 43remulcld 11014 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
5012, 28expcld 13873 . . . . . . . . . . 11 (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
5118, 28expcld 13873 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℂ)
5250, 51, 46divcld 11760 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53 1cnd 10979 . . . . . . . . . 10 (𝜑 → 1 ∈ ℂ)
5452, 53addcld 11003 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
5519a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 2)
5637, 55rplogcld 25793 . . . . . . . . . . . . . 14 (𝜑 → (log‘2) ∈ ℝ+)
5756, 45rpexpcld 13971 . . . . . . . . . . . . 13 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58 1re 10984 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
59 3nn0 12260 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℕ0
6058, 59nn0addge2i 12291 . . . . . . . . . . . . . . . . . 18 1 ≤ (3 + 1)
6160a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≤ (3 + 1))
62 df-4 12047 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
6361, 62breqtrrdi 5117 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 4)
6438, 5, 1, 63, 8letrd 11141 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝐴)
651, 64logge0d 25794 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (log‘𝐴))
6640, 28, 65expge0d 13891 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ ((log‘𝐴)↑5))
6741, 57, 66divge0d 12821 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
6847ltp1d 11914 . . . . . . . . . . . 12 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
693, 47, 48, 67, 68lelttrd 11142 . . . . . . . . . . 11 (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
703, 69ltned 11120 . . . . . . . . . 10 (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
7170necomd 3000 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
7254, 18, 71, 26mulne0d 11636 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
7338, 49, 72redivcld 11812 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74 5re 12069 . . . . . . . . . 10 5 ∈ ℝ
7574a1i 11 . . . . . . . . 9 (𝜑 → 5 ∈ ℝ)
76 4nn0 12261 . . . . . . . . . . 11 4 ∈ ℕ0
7776a1i 11 . . . . . . . . . 10 (𝜑 → 4 ∈ ℕ0)
7840, 77reexpcld 13890 . . . . . . . . 9 (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
7975, 78remulcld 11014 . . . . . . . 8 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
8044, 1remulcld 11014 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
8151, 2, 46, 11mulne0d 11636 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
8279, 80, 81redivcld 11812 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
8373, 82remulcld 11014 . . . . . 6 (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
8437, 83remulcld 11014 . . . . 5 (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
8543resqcld 13974 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℝ)
86 2z 12361 . . . . . . . . 9 2 ∈ ℤ
8786a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
8818, 26, 87expne0d 13879 . . . . . . 7 (𝜑 → ((log‘2)↑2) ≠ 0)
8937, 85, 88redivcld 11812 . . . . . 6 (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90 1nn0 12258 . . . . . . . . 9 1 ∈ ℕ0
9190a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℕ0)
9240, 91reexpcld 13890 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
9392, 1, 11redivcld 11812 . . . . . 6 (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
9489, 93remulcld 11014 . . . . 5 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
9584, 94readdcld 11013 . . . 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 11014 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97 1lt4 12158 . . . . . . . . . . . . . . . 16 1 < 4
9897a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 1 < 4)
9938, 5, 1, 98, 8ltletrd 11144 . . . . . . . . . . . . . 14 (𝜑 → 1 < 𝐴)
100 loggt0b 25796 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10139, 100syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
10299, 101mpbird 256 . . . . . . . . . . . . 13 (𝜑 → 0 < (log‘𝐴))
1033, 102ltned 11120 . . . . . . . . . . . 12 (𝜑 → 0 ≠ (log‘𝐴))
104103necomd 3000 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ≠ 0)
10512, 104, 45expne0d 13879 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ≠ 0)
10650, 51, 105, 46divne0d 11776 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
10752, 18, 106, 26mulne0d 11636 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
10838, 96, 107redivcld 11812 . . . . . . 7 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109108, 82remulcld 11014 . . . . . 6 (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
11037, 109remulcld 11014 . . . . 5 (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111110, 94readdcld 11013 . . . 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 13890 . . . . . 6 (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
1145, 113remulcld 11014 . . . . 5 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
11543, 77reexpcld 13890 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℝ)
116115, 1remulcld 11014 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
11718, 77expcld 13873 . . . . . 6 (𝜑 → ((log‘2)↑4) ∈ ℂ)
118 4z 12363 . . . . . . . 8 4 ∈ ℤ
119118a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℤ)
12018, 26, 119expne0d 13879 . . . . . 6 (𝜑 → ((log‘2)↑4) ≠ 0)
121117, 2, 120, 11mulne0d 11636 . . . . 5 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122114, 116, 121redivcld 11812 . . . 4 (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123 0le2 12084 . . . . . . 7 0 ≤ 2
124123a1i 11 . . . . . 6 (𝜑 → 0 ≤ 2)
12557, 39rpmulcld 12797 . . . . . . . 8 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
12628nn0ge0d 12305 . . . . . . . . 9 (𝜑 → 0 ≤ 5)
12740, 77, 65expge0d 13891 . . . . . . . . 9 (𝜑 → 0 ≤ ((log‘𝐴)↑4))
12875, 78, 126, 127mulge0d 11561 . . . . . . . 8 (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
12979, 125, 128divge0d 12821 . . . . . . 7 (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
1301, 99rplogcld 25793 . . . . . . . . . . 11 (𝜑 → (log‘𝐴) ∈ ℝ+)
131130, 45rpexpcld 13971 . . . . . . . . . 10 (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132131, 57rpdivcld 12798 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133132, 56rpmulcld 12797 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
13424, 22sylib 217 . . . . . . . . . . . . 13 (𝜑 → 1 < 2)
13537, 134rplogcld 25793 . . . . . . . . . . . 12 (𝜑 → (log‘2) ∈ ℝ+)
136135, 45rpexpcld 13971 . . . . . . . . . . 11 (𝜑 → ((log‘2)↑5) ∈ ℝ+)
13741, 136, 66divge0d 12821 . . . . . . . . . 10 (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
13847, 137ge0p1rpd 12811 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139138, 135rpmulcld 12797 . . . . . . . 8 (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140 0le1 11507 . . . . . . . . 9 0 ≤ 1
141140a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ 1)
142135rpred 12781 . . . . . . . . 9 (𝜑 → (log‘2) ∈ ℝ)
143135rpge0d 12785 . . . . . . . . 9 (𝜑 → 0 ≤ (log‘2))
14447lep1d 11915 . . . . . . . . 9 (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
14547, 48, 142, 143, 144lemul1ad 11923 . . . . . . . 8 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146133, 139, 38, 141, 145lediv2ad 12803 . . . . . . 7 (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ≤ (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))))
14773, 108, 82, 129, 146lemul1ad 11923 . . . . . 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 11924 . . . . 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 11598 . . . 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 11797 . . . . . . . . . 10 (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151150eqcomd 2745 . . . . . . . . 9 (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152151oveq2d 7300 . . . . . . . 8 (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153152oveq1d 7299 . . . . . . 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 7300 . . . . . 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 13871 . . . . . . 7 (𝜑 → ((log‘2)↑2) ∈ ℂ)
15612, 91expcld 13873 . . . . . . 7 (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
15713, 155, 156, 2, 88, 11divmuldivd 11801 . . . . . 6 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158154, 157oveq12d 7302 . . . . 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 11004 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
16050, 18, 105, 26mulne0d 11636 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
16153, 159, 51, 160, 46divdiv2d 11792 . . . . . . . . . 10 (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162161oveq1d 7299 . . . . . . . . 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 7300 . . . . . . . 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 11004 . . . . . . . . . . 11 (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165164, 159, 160divcld 11760 . . . . . . . . . 10 (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
16682recnd 11012 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
16713, 165, 166mulassd 11007 . . . . . . . . 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 2745 . . . . . . . 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 2779 . . . . . . 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 7299 . . . . . 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 11795 . . . . . . . . . 10 (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172171eqcomd 2745 . . . . . . . . 9 (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173172oveq1d 7299 . . . . . . . 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 7299 . . . . . . 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 11007 . . . . . . . . . . . 12 (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176175eqcomd 2745 . . . . . . . . . . 11 (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177176oveq1d 7299 . . . . . . . . . 10 (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178177oveq1d 7299 . . . . . . . . 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 7299 . . . . . . . 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 11001 . . . . . . . . . . . . 13 (𝜑 → (2 · 1) = 2)
181180oveq1d 7299 . . . . . . . . . . . 12 (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182181oveq1d 7299 . . . . . . . . . . 11 (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183182oveq1d 7299 . . . . . . . . . 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 7299 . . . . . . . . 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 11004 . . . . . . . . . . . 12 (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
18679recnd 11012 . . . . . . . . . . . 12 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
18751, 2mulcld 11004 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188185, 159, 186, 187, 160, 81divmuldivd 11801 . . . . . . . . . . 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 7299 . . . . . . . . . 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 11007 . . . . . . . . . . . . 13 (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191190oveq2d 7300 . . . . . . . . . . . 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 7299 . . . . . . . . . . 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 11005 . . . . . . . . . . . . . 14 (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
19418, 51, 2mulassd 11007 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195194eqcomd 2745 . . . . . . . . . . . . . . 15 (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196195oveq2d 7300 . . . . . . . . . . . . . 14 (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197193, 196oveq12d 7302 . . . . . . . . . . . . 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 7299 . . . . . . . . . . . 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 11004 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200199, 2mulcld 11004 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
20118, 51, 26, 46mulne0d 11636 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202199, 2, 201, 11mulne0d 11636 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203186, 50, 185, 200, 105, 202divmuldivd 11801 . . . . . . . . . . . . . . 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 2745 . . . . . . . . . . . . . 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 7299 . . . . . . . . . . . . 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 11012 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℂ)
20778recnd 11012 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208206, 207, 50, 105divassd 11795 . . . . . . . . . . . . . . . 16 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209194oveq2d 7300 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210208, 209oveq12d 7302 . . . . . . . . . . . . . . 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 7299 . . . . . . . . . . . . . 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 12433 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 4 ∈ ℤ)
21312, 104, 45, 212expsubd 13884 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214213eqcomd 2745 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215 4p1e5 12128 . . . . . . . . . . . . . . . . . . . . . . . . 25 (4 + 1) = 5
21674recni 10998 . . . . . . . . . . . . . . . . . . . . . . . . . 26 5 ∈ ℂ
2174recni 10998 . . . . . . . . . . . . . . . . . . . . . . . . . 26 4 ∈ ℂ
218 ax-1cn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℂ
219216, 217, 218subaddi 11317 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((5 − 4) = 1 ↔ (4 + 1) = 5)
220215, 219mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . 24 (5 − 4) = 1
221220a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 − 4) = 1)
22253subid1d 11330 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 − 0) = 1)
223221, 222eqtr4d 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 − 4) = (1 − 0))
224206, 217jctir 521 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225 0cnd 10977 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 ∈ ℂ)
22653, 225jca 512 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227 subeqrev 11406 . . . . . . . . . . . . . . . . . . . . . . 23 (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228224, 226, 227syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229223, 228mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (4 − 5) = (0 − 1))
230 df-neg 11217 . . . . . . . . . . . . . . . . . . . . 21 -1 = (0 − 1)
231229, 230eqtr4di 2797 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (4 − 5) = -1)
232231oveq2d 7300 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233214, 232eqtrd 2779 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234233oveq2d 7300 . . . . . . . . . . . . . . . . 17 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
23513, 18, 51, 187, 26, 81divmuldivd 11801 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236235eqcomd 2745 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237234, 236oveq12d 7302 . . . . . . . . . . . . . . . 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 7299 . . . . . . . . . . . . . . 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 12360 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℤ)
24012, 104, 239expnegd 13880 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241240oveq2d 7300 . . . . . . . . . . . . . . . . . 18 (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
24251, 51, 2, 46, 11divdiv1d 11791 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243242eqcomd 2745 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244243oveq2d 7300 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245241, 244oveq12d 7302 . . . . . . . . . . . . . . . . 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 7299 . . . . . . . . . . . . . . . 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 13879 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248206, 53, 156, 247divassd 11795 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249248eqcomd 2745 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
25051, 46dividd 11758 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251250oveq1d 7299 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252251oveq2d 7300 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253249, 252oveq12d 7302 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) = (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))))
254253oveq1d 7299 . . . . . . . . . . . . . . . . 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 11001 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (5 · 1) = 5)
256255oveq1d 7299 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
25713, 18, 53, 2, 26, 11divmuldivd 11801 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258256, 257oveq12d 7302 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259258oveq1d 7299 . . . . . . . . . . . . . . . . . 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 2840 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (2 · 1) ∈ ℂ)
26118, 2mulcld 11004 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
26218, 2, 26, 11mulne0d 11636 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263206, 156, 260, 261, 247, 262divmuldivd 11801 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264180oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · (2 · 1)) = (5 · 2))
265264oveq1d 7299 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266263, 265eqtrd 2779 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267266oveq1d 7299 . . . . . . . . . . . . . . . . . . 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 12546 . . . . . . . . . . . . . . . . . . . . . . 23 (5 · 2) = 10
269268a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (5 · 2) = 10)
270269oveq1d 7299 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271270oveq1d 7299 . . . . . . . . . . . . . . . . . . . 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 12464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 10 ∈ ℕ0
273272nn0cni 12254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 10 ∈ ℂ
274273a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑10 ∈ ℂ)
275274mulid1d 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (10 · 1) = 10)
276275oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 / (((log‘𝐴)↑1) · (log‘2))))
27713, 156mulcld 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278277, 155, 88divcld 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279278mulid2d 11002 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280276, 279oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ∈ ℂ)
28218, 26, 239expne0d 13879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑1) ≠ 0)
283277, 281, 282divcld 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284283mulid1d 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285284oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286 10re 12465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 10 ∈ ℝ
287286a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑10 ∈ ℝ)
288287, 40, 104redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ∈ ℝ)
28940, 43, 26redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290289, 91reexpcld 13890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
29137, 290remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292288, 291readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293287, 291readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
29443, 112reexpcld 13890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ∈ ℝ)
295 3z 12362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3 ∈ ℤ
296295a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → 3 ∈ ℤ)
29718, 26, 296expne0d 13879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘2)↑3) ≠ 0)
298113, 294, 297redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
2995, 298remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300 ere 15807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 e ∈ ℝ
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e ∈ ℝ)
302112nn0red 12303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 ∈ ℝ)
303 egt2lt3 15924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (2 < e ∧ e < 3)
304303simpri 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 e < 3
305304a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → e < 3)
306 3lt4 12156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3 < 4
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 3 < 4)
308302, 5, 1, 307, 8ltletrd 11144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 3 < 𝐴)
309301, 302, 1, 305, 308lttrd 11145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → e < 𝐴)
310301, 1, 309ltled 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → e ≤ 𝐴)
311301, 1lenltd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312310, 311mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ¬ 𝐴 < e)
313 loglt1b 25798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
31439, 313syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315312, 314mtbird 325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ¬ (log‘𝐴) < 1)
31638, 40lenltd 11130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317315, 316mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → 1 ≤ (log‘𝐴))
318 10nn 12462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 10 ∈ ℕ
319318a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑10 ∈ ℕ)
320 nnledivrp 12851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
321319, 130, 320syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (1 ≤ (log‘𝐴) ↔ (10 / (log‘𝐴)) ≤ 10))
322317, 321mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / (log‘𝐴)) ≤ 10)
323288, 287, 291, 322leadd1dd 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
32438, 55gtned 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≠ 1)
32537, 15, 1, 9, 324relogbcld 39988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ∈ ℝ)
326325, 91reexpcld 13890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
32742, 55jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328 logbgt0b 25952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
32939, 327, 328syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
33099, 329mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 0 < (2 logb 𝐴))
331325, 330elrpd 12778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332331, 239rpexpcld 13971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333332rpne0d 12786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334287, 326, 333redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335334, 37readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336 sq2 13923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (2↑2) = 4
337336a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2↑2) = 4)
338337, 5eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ∈ ℝ)
3395, 338remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ∈ ℝ)
340325resqcld 13974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
3415, 340remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342325recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 logb 𝐴) ∈ ℂ)
343342exp1d 13868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344343oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (10 / ((2 logb 𝐴)↑1)) = (10 / (2 logb 𝐴)))
345344oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) = ((10 / (2 logb 𝐴)) + 2))
346345, 335eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347287rehalfcld 12229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
348347, 37readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ∈ ℝ)
349344, 334eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ∈ ℝ)
350287, 37, 17redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / 2) ∈ ℝ)
351272nn0ge0i 12269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 0 ≤ 10
352351a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 0 ≤ 10)
35342, 324, 87relogbexpd 39989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝜑 → (2 logb (2↑2)) = 2)
354353eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 = (2 logb (2↑2)))
355337oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356354, 355eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 2 = (2 logb 4))
35737leidd 11550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 2 ≤ 2)
35887, 357, 5, 7, 1, 9, 8logblebd 39991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359356, 358eqbrtrd 5097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 2 ≤ (2 logb 𝐴))
36042, 331, 287, 352, 359lediv2ad 12803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (10 / (2 logb 𝐴)) ≤ (10 / 2))
361349, 350, 37, 360leadd1dd 11598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ ((10 / 2) + 2))
362 1nn 11993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 1 ∈ ℕ
363 6nn0 12263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6 ∈ ℕ0
364 2nn0 12259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2 ∈ ℕ0
36527, 364nn0addcli 12279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ∈ ℕ0
366 5p2e7 12138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (5 + 2) = 7
367 7re 12075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 7 ∈ ℝ
368367, 364nn0addge1i 12290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 7 ≤ (7 + 2)
369 7p2e9 12143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (7 + 2) = 9
370368, 369breqtri 5100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 7 ≤ 9
371366, 370eqbrtri 5096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (5 + 2) ≤ 9
372362, 363, 365, 371declei 12482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (5 + 2) ≤ 16
373372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) ≤ 16)
374206, 13, 274, 17ldiv 11818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((5 · 2) = 10 ↔ 5 = (10 / 2)))
375269, 374mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → 5 = (10 / 2))
376375oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (5 + 2) = ((10 / 2) + 2))
377 4t4e16 12545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (4 · 4) = 16
378377eqcomi 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 16 = (4 · 4)
379378a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑16 = (4 · 4))
380337eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → 4 = (2↑2))
381380oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (4 · 4) = (4 · (2↑2)))
382379, 381eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑16 = (4 · (2↑2)))
383373, 376, 3823brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / 2) + 2) ≤ (4 · (2↑2)))
384346, 348, 339, 361, 383letrd 11141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385345, 384eqbrtrd 5097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
3863, 5, 7ltled 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → 0 ≤ 4)
387364a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ ℕ0)
38837, 325, 387, 124, 359leexp1ad 39987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389338, 340, 5, 386, 388lemul2ad 11924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390335, 339, 341, 385, 389letrd 11141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
39137, 326remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392391recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393326recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394274, 392, 393, 333divdird 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))))
39513, 393, 393, 333divassd 11795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396395oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398397oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399398, 180eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400399oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
401396, 400eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((10 / ((2 logb 𝐴)↑1)) + 2))
402394, 401eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((10 / ((2 logb 𝐴)↑1)) + 2))
403402eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((10 / ((2 logb 𝐴)↑1)) + 2) = ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404 2p1e3 12124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (2 + 1) = 3
405404a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → (2 + 1) = 3)
406302recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝜑 → 3 ∈ ℂ)
407406, 53, 13subadd2d 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408405, 407mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝜑 → (3 − 1) = 2)
409408eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → 2 = (3 − 1))
410409oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411410oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
4123, 330gtned 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → (2 logb 𝐴) ≠ 0)
413342, 412, 239, 296expsubd 13884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414413oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415411, 414eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416217a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 4 ∈ ℂ)
417325, 112reexpcld 13890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418417recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419416, 418, 393, 333divassd 11795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420419eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421415, 420eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422390, 403, 4213brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423287, 391readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
4245, 417remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425423, 424, 332lediv1d 12827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
42787uzidd 12607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝜑 → 2 ∈ (ℤ‘2))
428427, 39jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝜑 → (2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+))
429 relogbval 25931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((2 ∈ (ℤ‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430428, 429syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431430oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432431oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433432oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 + (2 · ((2 logb 𝐴)↑1))) = (10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434430oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
43512, 18, 26, 112expdivd 13887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436434, 435eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437436oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438426, 433, 4373brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439292, 293, 299, 323, 438letrd 11141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
44012exp1d 13868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441440eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442441oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (10 / (log‘𝐴)) = (10 / ((log‘𝐴)↑1)))
44313, 156, 281, 282divassd 11795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
44412, 18, 26, 91expdivd 13887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445444eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446445oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447443, 446eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448447eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449442, 448oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450113recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
45118, 112expcld 13873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2)↑3) ∈ ℂ)
452416, 450, 451, 297divassd 11795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453452eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454439, 449, 4533brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455285, 454eqbrtrd 5097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456281, 282dividd 11758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457456eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458457oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461460oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463462, 451, 297divcld 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464463mulid1d 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465464eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466455, 461, 4653brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → (10 / ((log‘𝐴)↑1)) ∈ ℂ)
468467mulid1d 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = (10 / ((log‘𝐴)↑1)))
469468eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · 1))
47018, 26dividd 11758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → ((log‘2) / (log‘2)) = 1)
471470eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → 1 = ((log‘2) / (log‘2)))
472471oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((10 / ((log‘𝐴)↑1)) · 1) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473469, 472eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474274, 156, 18, 18, 247, 26divmuldivd 11801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475473, 474eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / ((log‘𝐴)↑1)) = ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
47618exp1d 13868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑1) = (log‘2))
477476oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478 df-2 12045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2 = (1 + 1)
479478a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝜑 → 2 = (1 + 1))
480479oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
48118, 91, 91expaddd 13875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482480, 481eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483482eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484477, 483oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)))
485475, 484oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (log‘2) = ((log‘2)↑1))
487486oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488471, 487eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489488oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490476, 18eqeltrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ∈ ℂ)
491476, 26eqnetrd 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑1) ≠ 0)
492462, 451, 18, 490, 297, 491divmuldivd 11801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494466, 485, 4933brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496156, 18, 247, 26mulne0d 11636 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497274, 18, 495, 496div23d 11797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ((10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498277, 18, 155, 88div23d 11797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499497, 498oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
50218, 91, 112expaddd 13875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503501, 502eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504503eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505504oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)))
506494, 499, 5053brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508287, 507, 496redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509508recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510509, 278, 18adddird 11009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((log‘2)↑4) ≠ 0)
513462, 18, 117, 512div23d 11797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514506, 511, 5133brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
51537, 92remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516515, 85, 88redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517508, 516readdcld 11013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518114, 115, 120redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519517, 518, 135lemul1d 12824 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521280, 520eqbrtrd 5097 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
522274, 53, 495, 496divassd 11795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
52353, 277, 155, 88div12d 11796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524522, 523oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . . 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 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526525eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527526oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528521, 524, 5273brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))) ≤ (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
5292, 11dividd 11758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (𝐴 / 𝐴) = 1)
530529eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 1 = (𝐴 / 𝐴))
531530oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
5322, 2, 495, 11, 496divdiv1d 11791 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533531, 532eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534533oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535 eqidd 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536530oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537536oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538535, 537eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539534, 538oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . . 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 11795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541528, 539, 5403brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
5422, 495mulcomd 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543156, 18, 2mulassd 11007 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544542, 543eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545544oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546545oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
5472, 2, 155, 11, 88divdiv1d 11791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
5482, 155mulcomd 11005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549548oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550547, 549eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551550oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552546, 551oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . . 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 2740 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554530oveq1d 7299 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555553, 554eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556555oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557541, 552, 5563brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558156, 261mulcld 11004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559156, 261, 247, 262mulne0d 11636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560274, 558, 2, 559div32d 11783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561560eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562155, 2mulcld 11004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563155, 2, 88, 11mulne0d 11636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564277, 562, 2, 563div32d 11783 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565564eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566561, 565oveq12d 7302 . . . . . . . . . . . . . . . . . . . . . . 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 11791 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
5682, 117mulcomd 11005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569568oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570567, 569eqtrd 2779 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571570oveq2d 7300 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572557, 566, 5713brtr3d 5106 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
57343, 1remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
57492, 573remulcld 11014 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575287, 574, 559redivcld 11812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576575recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577157, 94eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578577recnd 11012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579576, 578, 2adddird 11009 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) = (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)))
580579eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . 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 13873 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582416, 581mulcld 11004 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583117, 2mulcld 11004 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584117, 2, 512, 11mulne0d 11636 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585582, 583, 2, 584div32d 11783 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586585eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587572, 580, 5863brtr3d 5106 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588575, 577readdcld 11013 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589588, 122, 39lemul1d 12824 . . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591271, 590eqbrtrd 5097 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592267, 591eqbrtrd 5097 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593259, 592eqbrtrd 5097 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
594254, 593eqbrtrd 5097 . . . . . . . . . . . . . . . 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 5097 . . . . . . . . . . . . . . 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 5097 . . . . . . . . . . . . . 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 5097 . . . . . . . . . . . . 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 5097 . . . . . . . . . . . 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 5097 . . . . . . . . . . 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 5097 . . . . . . . . . 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 5097 . . . . . . . . 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 5097 . . . . . . . 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 5097 . . . . . . 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 5097 . . . . . 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 5097 . . . . 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 5097 . . . 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 11141 . . 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 5097 . 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 584 . . . . . . . . . 10 (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610609eqcomd 2745 . . . . . . . . 9 (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611610oveq1d 7299 . . . . . . . 8 (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612611oveq1d 7299 . . . . . . 7 (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613612oveq1d 7299 . . . . . 6 (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614613oveq2d 7300 . . . . 5 (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615 5cn 12070 . . . . . . . . . . . . . . 15 5 ∈ ℂ
616615a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 5 ∈ ℂ)
617616, 207mulcld 11004 . . . . . . . . . . . . 13 (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618617mulid1d 11001 . . . . . . . . . . . 12 (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619618eqcomd 2745 . . . . . . . . . . 11 (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620 eqidd 2740 . . . . . . . . . . . . . 14 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621 df-5 12048 . . . . . . . . . . . . . . . . . . 19 5 = (4 + 1)
622621a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 5 = (4 + 1))
623622oveq2d 7300 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
62418, 91, 77expaddd 13875 . . . . . . . . . . . . . . . . 17 (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625623, 624eqtrd 2779 . . . . . . . . . . . . . . . 16 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626476oveq2d 7300 . . . . . . . . . . . . . . . 16 (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627625, 626eqtrd 2779 . . . . . . . . . . . . . . 15 (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628627oveq1d 7299 . . . . . . . . . . . . . 14 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629620, 628eqtrd 2779 . . . . . . . . . . . . 13 (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630117, 18, 2mulassd 11007 . . . . . . . . . . . . 13 (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631629, 630eqtrd 2779 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
63218, 2mulcomd 11005 . . . . . . . . . . . . 13 (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633632oveq2d 7300 . . . . . . . . . . . 12 (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634631, 633eqtrd 2779 . . . . . . . . . . 11 (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635619, 634oveq12d 7302 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
6362, 18mulcld 11004 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
6372, 18, 11, 26mulne0d 11636 . . . . . . . . . . . 12 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638186, 117, 53, 636, 120, 637divmuldivd 11801 . . . . . . . . . . 11 (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639638eqcomd 2745 . . . . . . . . . 10 (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640635, 639eqtrd 2779 . . . . . . . . 9 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641206, 207, 117, 120divassd 11795 . . . . . . . . . 10 (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642641oveq1d 7299 . . . . . . . . 9 (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643640, 642eqtrd 2779 . . . . . . . 8 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
64412, 18, 26, 77expdivd 13887 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645644eqcomd 2745 . . . . . . . . . 10 (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646645oveq2d 7300 . . . . . . . . 9 (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647646oveq1d 7299 . . . . . . . 8 (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648643, 647eqtrd 2779 . . . . . . 7 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649610oveq1d 7299 . . . . . . . . 9 (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650649oveq2d 7300 . . . . . . . 8 (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651650oveq1d 7299 . . . . . . 7 (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652648, 651eqtrd 2779 . . . . . 6 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653342, 77expcld 13873 . . . . . . . . . 10 (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654616, 653mulcld 11004 . . . . . . . . 9 (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
65539rpne0d 12786 . . . . . . . . . . 11 (𝜑𝐴 ≠ 0)
6562, 18, 655, 26mulne0d 11636 . . . . . . . . . 10 (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657636, 656reccld 11753 . . . . . . . . 9 (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658654, 657mulcld 11004 . . . . . . . 8 (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659658addid1d 11184 . . . . . . 7 (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660659eqcomd 2745 . . . . . 6 (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661652, 660eqtrd 2779 . . . . 5 (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662614, 661oveq12d 7302 . . . 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 7300 . . 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 12109 . . . . . . 7 1 = (2 − 1)
665664a1i 11 . . . . . 6 (𝜑 → 1 = (2 − 1))
666665oveq2d 7300 . . . . 5 (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667666oveq1d 7299 . . . 4 (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668667oveq2d 7300 . . 3 (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669663, 668oveq12d 7302 . 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 12067 . . . . 5 4 ∈ ℂ
671670a1i 11 . . . 4 (𝜑 → 4 ∈ ℂ)
672671, 117, 581, 2, 120, 655divmuldivd 11801 . . 3 (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673672eqcomd 2745 . 2 (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674608, 669, 6733brtr3d 5106 1 (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2107   class class class wbr 5075  cfv 6437  (class class class)co 7284  cc 10878  cr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885   < clt 11018  cle 11019  cmin 11214  -cneg 11215   / cdiv 11641  cn 11982  2c2 12037  3c3 12038  4c4 12039  5c5 12040  6c6 12041  7c7 12042  9c9 12044  0cn0 12242  cz 12328  cdc 12446  cuz 12591  +crp 12739  cexp 13791  eceu 15781  logclog 25719   logb clogb 25923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ioc 13093  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-fac 13997  df-bc 14026  df-hash 14054  df-shft 14787  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-limsup 15189  df-clim 15206  df-rlim 15207  df-sum 15407  df-ef 15786  df-e 15787  df-sin 15788  df-cos 15789  df-pi 15791  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-0g 17161  df-gsum 17162  df-topgen 17163  df-pt 17164  df-prds 17167  df-xrs 17222  df-qtop 17227  df-imas 17228  df-xps 17230  df-mre 17304  df-mrc 17305  df-acs 17307  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-submnd 18440  df-mulg 18710  df-cntz 18932  df-cmn 19397  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-fbas 20603  df-fg 20604  df-cnfld 20607  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-lp 22296  df-perf 22297  df-cn 22387  df-cnp 22388  df-haus 22475  df-tx 22722  df-hmeo 22915  df-fil 23006  df-fm 23098  df-flim 23099  df-flf 23100  df-xms 23482  df-ms 23483  df-tms 23484  df-cncf 24050  df-limc 25039  df-dv 25040  df-log 25721  df-cxp 25722  df-logb 25924
This theorem is referenced by:  aks4d1p1p5  40090
  Copyright terms: Public domain W3C validator