Theorem aks4d1p1p7 41245

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

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   class class class wbr 5147  ‘cfv 6542  (class class class)co 7411  ℂcc 11110  ℝcr 11111  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117   < clt 11252   ≤ cle 11253   − cmin 11448  -cneg 11449   / cdiv 11875  ℕcn 12216  2c2 12271  3c3 12272  4c4 12273  5c5 12274  6c6 12275  7c7 12276  9c9 12278  ℕ₀cn0 12476  ℤcz 12562  ;cdc 12681  ℤ_≥cuz 12826  ℝ⁺crp 12978  ↑cexp 14031  eceu 16010  logclog 26299   log_b clogb 26505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-e 16016  df-sin 16017  df-cos 16018  df-pi 16020  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-haus 23039  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-limc 25615  df-dv 25616  df-log 26301  df-cxp 26302  df-logb 26506

This theorem is referenced by:  aks4d1p1p5  41246