Theorem aks4d1p1p7 39666

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 10712	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		0red 10687	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
4		4re 11763	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℝ
5	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
6		4pos 11786	. . . . . . . . . . . . . . 15 ⊢ 0 < 4
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 4)
8		aks4d1p1p7.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ≤ 𝐴)
9	3, 5, 1, 7, 8	ltletrd 10843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝐴)
10	3, 9	ltned 10819	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 𝐴)
11	10	necomd 3006	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
12	2, 11	logcld 25266	. . . . . . . . . 10 ⊢ (𝜑 → (log‘𝐴) ∈ ℂ)
13		2cnd 11757	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
14		2pos 11782	. . . . . . . . . . . . . 14 ⊢ 0 < 2
15	14	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 2)
16	3, 15	ltned 10819	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 2)
17	16	necomd 3006	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≠ 0)
18	13, 17	logcld 25266	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ∈ ℂ)
19		1lt2 11850	. . . . . . . . . . . . . 14 ⊢ 1 < 2
20		2rp 12440	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
21		loggt0b 25327	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
22	20, 21	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (0 < (log‘2) ↔ 1 < 2)
23	19, 22	mpbir 234	. . . . . . . . . . . . 13 ⊢ 0 < (log‘2)
24	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (log‘2))
25	3, 24	ltned 10819	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≠ (log‘2))
26	25	necomd 3006	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ≠ 0)
27		5nn0 11959	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 5 ∈ ℕ0)
29	12, 18, 26, 28	expdivd 13579	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
30	29	oveq1d 7170	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
31	30	oveq1d 7170	. . . . . . 7 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
32	31	oveq2d 7171	. . . . . 6 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
33	32	oveq1d 7170	. . . . 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 7171	. . . 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 7170	. . 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 11753	. . . . . . 7 ⊢ 2 ∈ ℝ
37	36	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
38		1red 10685	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
39	1, 9	elrpd 12474	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
40	39	relogcld 25318	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)
41	40, 28	reexpcld 13582	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
42	20	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℝ+)
43	42	relogcld 25318	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ)
44	43, 28	reexpcld 13582	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ)
45	28	nn0zd 12129	. . . . . . . . . . . 12 ⊢ (𝜑 → 5 ∈ ℤ)
46	18, 26, 45	expne0d 13571	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ≠ 0)
47	41, 44, 46	redivcld 11511	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
48	47, 38	readdcld 10713	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
49	48, 43	remulcld 10714	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
50	12, 28	expcld 13565	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
51	18, 28	expcld 13565	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℂ)
52	50, 51, 46	divcld 11459	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53		1cnd 10679	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
54	52, 53	addcld 10703	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
55	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 2)
56	37, 55	rplogcld 25324	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
57	56, 45	rpexpcld 13663	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58		1re 10684	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
59		3nn0 11957	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ0
60	58, 59	nn0addge2i 11988	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ≤ (3 + 1)
61	60	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ (3 + 1))
62		df-4 11744	. . . . . . . . . . . . . . . . 17 ⊢ 4 = (3 + 1)
63	61, 62	breqtrrdi 5077	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 4)
64	38, 5, 1, 63, 8	letrd 10840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ 𝐴)
65	1, 64	logge0d 25325	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (log‘𝐴))
66	40, 28, 65	expge0d 13583	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑5))
67	41, 57, 66	divge0d 12517	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
68	47	ltp1d 11613	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
69	3, 47, 48, 67, 68	lelttrd 10841	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
70	3, 69	ltned 10819	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
71	70	necomd 3006	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
72	54, 18, 71, 26	mulne0d 11335	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
73	38, 49, 72	redivcld 11511	. . . . . . 7 ⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74		5re 11766	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
75	74	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 5 ∈ ℝ)
76		4nn0 11958	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
77	76	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ0)
78	40, 77	reexpcld 13582	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
79	75, 78	remulcld 10714	. . . . . . . 8 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
80	44, 1	remulcld 10714	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
81	51, 2, 46, 11	mulne0d 11335	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
82	79, 80, 81	redivcld 11511	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
83	73, 82	remulcld 10714	. . . . . 6 ⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
84	37, 83	remulcld 10714	. . . . 5 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
85	43	resqcld 13666	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℝ)
86		2z 12058	. . . . . . . . 9 ⊢ 2 ∈ ℤ
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
88	18, 26, 87	expne0d 13571	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ≠ 0)
89	37, 85, 88	redivcld 11511	. . . . . 6 ⊢ (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90		1nn0 11955	. . . . . . . . 9 ⊢ 1 ∈ ℕ0
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℕ0)
92	40, 91	reexpcld 13582	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
93	92, 1, 11	redivcld 11511	. . . . . 6 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
94	89, 93	remulcld 10714	. . . . 5 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
95	84, 94	readdcld 10713	. . . 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 10714	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97		1lt4 11855	. . . . . . . . . . . . . . . 16 ⊢ 1 < 4
98	97	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 4)
99	38, 5, 1, 98, 8	ltletrd 10843	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 𝐴)
100		loggt0b 25327	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
101	39, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
102	99, 101	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (log‘𝐴))
103	3, 102	ltned 10819	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ (log‘𝐴))
104	103	necomd 3006	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ≠ 0)
105	12, 104, 45	expne0d 13571	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ≠ 0)
106	50, 51, 105, 46	divne0d 11475	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
107	52, 18, 106, 26	mulne0d 11335	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
108	38, 96, 107	redivcld 11511	. . . . . . 7 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109	108, 82	remulcld 10714	. . . . . 6 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
110	37, 109	remulcld 10714	. . . . 5 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111	110, 94	readdcld 10713	. . . 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 13582	. . . . . 6 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
114	5, 113	remulcld 10714	. . . . 5 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
115	43, 77	reexpcld 13582	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℝ)
116	115, 1	remulcld 10714	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
117	18, 77	expcld 13565	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℂ)
118		4z 12060	. . . . . . . 8 ⊢ 4 ∈ ℤ
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ∈ ℤ)
120	18, 26, 119	expne0d 13571	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
121	117, 2, 120, 11	mulne0d 11335	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122	114, 116, 121	redivcld 11511	. . . 4 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123		0le2 11781	. . . . . . 7 ⊢ 0 ≤ 2
124	123	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ≤ 2)
125	57, 39	rpmulcld 12493	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
126	28	nn0ge0d 12002	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 5)
127	40, 77, 65	expge0d 13583	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑4))
128	75, 78, 126, 127	mulge0d 11260	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
129	79, 125, 128	divge0d 12517	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
130	1, 99	rplogcld 25324	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+)
131	130, 45	rpexpcld 13663	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132	131, 57	rpdivcld 12494	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133	132, 56	rpmulcld 12493	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
134	24, 22	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 2)
135	37, 134	rplogcld 25324	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
136	135, 45	rpexpcld 13663	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
137	41, 136, 66	divge0d 12517	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
138	47, 137	ge0p1rpd 12507	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139	138, 135	rpmulcld 12493	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140		0le1 11206	. . . . . . . . 9 ⊢ 0 ≤ 1
141	140	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
142	135	rpred 12477	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℝ)
143	135	rpge0d 12481	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (log‘2))
144	47	lep1d 11614	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
145	47, 48, 142, 143, 144	lemul1ad 11622	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146	133, 139, 38, 141, 145	lediv2ad 12499	. . . . . . 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 11622	. . . . . 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 11623	. . . . 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 11297	. . . 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 11496	. . . . . . . . . 10 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151	150	eqcomd 2764	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152	151	oveq2d 7171	. . . . . . . 8 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153	152	oveq1d 7170	. . . . . . 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 7171	. . . . . 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 13563	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℂ)
156	12, 91	expcld 13565	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
157	13, 155, 156, 2, 88, 11	divmuldivd 11500	. . . . . 6 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158	154, 157	oveq12d 7173	. . . . 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 10704	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
160	50, 18, 105, 26	mulne0d 11335	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
161	53, 159, 51, 160, 46	divdiv2d 11491	. . . . . . . . . 10 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162	161	oveq1d 7170	. . . . . . . . 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 7171	. . . . . . . 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 10704	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165	164, 159, 160	divcld 11459	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
166	82	recnd 10712	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
167	13, 165, 166	mulassd 10707	. . . . . . . . 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 2764	. . . . . . . 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 2793	. . . . . . 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 7170	. . . . . 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 11494	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172	171	eqcomd 2764	. . . . . . . . 9 ⊢ (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173	172	oveq1d 7170	. . . . . . . 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 7170	. . . . . . 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 10707	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176	175	eqcomd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177	176	oveq1d 7170	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178	177	oveq1d 7170	. . . . . . . . 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 7170	. . . . . . . 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	mulid1d 10701	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 1) = 2)
181	180	oveq1d 7170	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182	181	oveq1d 7170	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183	182	oveq1d 7170	. . . . . . . . . 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 7170	. . . . . . . . 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 10704	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
186	79	recnd 10712	. . . . . . . . . . . 12 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
187	51, 2	mulcld 10704	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188	185, 159, 186, 187, 160, 81	divmuldivd 11500	. . . . . . . . . . 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 7170	. . . . . . . . . 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 10707	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191	190	oveq2d 7171	. . . . . . . . . . . 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 7170	. . . . . . . . . . 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 10705	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
194	18, 51, 2	mulassd 10707	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195	194	eqcomd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196	195	oveq2d 7171	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197	193, 196	oveq12d 7173	. . . . . . . . . . . . 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 7170	. . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200	199, 2	mulcld 10704	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
201	18, 51, 26, 46	mulne0d 11335	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202	199, 2, 201, 11	mulne0d 11335	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203	186, 50, 185, 200, 105, 202	divmuldivd 11500	. . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . 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 10712	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℂ)
207	78	recnd 10712	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208	206, 207, 50, 105	divassd 11494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209	194	oveq2d 7171	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210	208, 209	oveq12d 7173	. . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . 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 12129	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 4 ∈ ℤ)
213	12, 104, 45, 212	expsubd 13576	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214	213	eqcomd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215		4p1e5 11825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 1) = 5
216	74	recni 10698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℂ
217	4	recni 10698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℂ
218		ax-1cn 10638	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℂ
219	216, 217, 218	subaddi 11016	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((5 − 4) = 1 ↔ (4 + 1) = 5)
220	215, 219	mpbir 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (5 − 4) = 1
221	220	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 − 4) = 1)
222	53	subid1d 11029	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 − 0) = 1)
223	221, 222	eqtr4d 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 − 4) = (1 − 0))
224	206, 217	jctir 524	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225		0cnd 10677	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ∈ ℂ)
226	53, 225	jca 515	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227		subeqrev 11105	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228	224, 226, 227	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229	223, 228	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (4 − 5) = (0 − 1))
230		df-neg 10916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 = (0 − 1)
231	229, 230	eqtr4di 2811	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (4 − 5) = -1)
232	231	oveq2d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233	214, 232	eqtrd 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234	233	oveq2d 7171	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
235	13, 18, 51, 187, 26, 81	divmuldivd 11500	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236	235	eqcomd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237	234, 236	oveq12d 7173	. . . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . . 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 12057	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℤ)
240	12, 104, 239	expnegd 13572	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241	240	oveq2d 7171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
242	51, 51, 2, 46, 11	divdiv1d 11490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243	242	eqcomd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244	243	oveq2d 7171	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245	241, 244	oveq12d 7173	. . . . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . . . 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 13571	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248	206, 53, 156, 247	divassd 11494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249	248	eqcomd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
250	51, 46	dividd 11457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251	250	oveq1d 7170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252	251	oveq2d 7171	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253	249, 252	oveq12d 7173	. . . . . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . . . . 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	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (5 · 1) = 5)
256	255	oveq1d 7170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
257	13, 18, 53, 2, 26, 11	divmuldivd 11500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258	256, 257	oveq12d 7173	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259	258	oveq1d 7170	. . . . . . . . . . . . . . . . . 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 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · 1) ∈ ℂ)
261	18, 2	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
262	18, 2, 26, 11	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263	206, 156, 260, 261, 247, 262	divmuldivd 11500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264	180	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · (2 · 1)) = (5 · 2))
265	264	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266	263, 265	eqtrd 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267	266	oveq1d 7170	. . . . . . . . . . . . . . . . . . 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 12242	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (5 · 2) = ;10
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · 2) = ;10)
270	269	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271	270	oveq1d 7170	. . . . . . . . . . . . . . . . . . . 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 12160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ;10 ∈ ℕ0
273	272	nn0cni 11951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ;10 ∈ ℂ
274	273	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ;10 ∈ ℂ)
275	274	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (;10 · 1) = ;10)
276	275	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 / (((log‘𝐴)↑1) · (log‘2))))
277	13, 156	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278	277, 155, 88	divcld 11459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279	278	mulid2d 10702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280	276, 279	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 13565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
282	18, 26, 239	expne0d 13571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
283	277, 281, 282	divcld 11459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284	283	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285	284	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286		10re 12161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ;10 ∈ ℝ
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ;10 ∈ ℝ)
288	287, 40, 104	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ∈ ℝ)
289	40, 43, 26	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290	289, 91	reexpcld 13582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
291	37, 290	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292	288, 291	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293	287, 291	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
294	43, 112	reexpcld 13582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℝ)
295		3z 12059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 3 ∈ ℤ
296	295	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → 3 ∈ ℤ)
297	18, 26, 296	expne0d 13571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ≠ 0)
298	113, 294, 297	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
299	5, 298	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300		ere 15495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ e ∈ ℝ
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e ∈ ℝ)
302	112	nn0red 12000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 ∈ ℝ)
303		egt2lt3 15612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 < e ∧ e < 3)
304	303	simpri 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ e < 3
305	304	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → e < 3)
306		3lt4 11853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 3 < 4
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 3 < 4)
308	302, 5, 1, 307, 8	ltletrd 10843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 < 𝐴)
309	301, 302, 1, 305, 308	lttrd 10844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e < 𝐴)
310	301, 1, 309	ltled 10831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → e ≤ 𝐴)
311	301, 1	lenltd 10829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312	310, 311	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ¬ 𝐴 < e)
313		loglt1b 25329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
314	39, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315	312, 314	mtbird 328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ¬ (log‘𝐴) < 1)
316	38, 40	lenltd 10829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317	315, 316	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 1 ≤ (log‘𝐴))
318		10nn 12158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ;10 ∈ ℕ
319	318	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ;10 ∈ ℕ)
320		nnledivrp 12547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((;10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
321	319, 130, 320	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
322	317, 321	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ≤ ;10)
323	288, 287, 291, 322	leadd1dd 11297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
324	38, 55	gtned 10818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≠ 1)
325	37, 15, 1, 9, 324	relogbcld 39565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ)
326	325, 91	reexpcld 13582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
327	42, 55	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328		logbgt0b 25483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
329	39, 327, 328	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
330	99, 329	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 0 < (2 logb 𝐴))
331	325, 330	elrpd 12474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332	331, 239	rpexpcld 13663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333	332	rpne0d 12482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334	287, 326, 333	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335	334, 37	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336		sq2 13615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (2↑2) = 4
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2↑2) = 4)
338	337, 5	eqeltrd 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ∈ ℝ)
339	5, 338	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ∈ ℝ)
340	325	resqcld 13666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
341	5, 340	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342	325	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℂ)
343	342	exp1d 13560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344	343	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) = (;10 / (2 logb 𝐴)))
345	344	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 / (2 logb 𝐴)) + 2))
346	345, 335	eqeltrrd 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347	287	rehalfcld 11926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
348	347, 37	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ∈ ℝ)
349	344, 334	eqeltrrd 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ∈ ℝ)
350	287, 37, 17	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
351	272	nn0ge0i 11966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 0 ≤ ;10
352	351	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 0 ≤ ;10)
353	42, 324, 87	relogbexpd 39566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
354	353	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 = (2 logb (2↑2)))
355	337	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356	354, 355	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 2 = (2 logb 4))
357	37	leidd 11249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 ≤ 2)
358	87, 357, 5, 7, 1, 9, 8	logblebd 39568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359	356, 358	eqbrtrd 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≤ (2 logb 𝐴))
360	42, 331, 287, 352, 359	lediv2ad 12499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ≤ (;10 / 2))
361	349, 350, 37, 360	leadd1dd 11297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ ((;10 / 2) + 2))
362		1nn 11690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 1 ∈ ℕ
363		6nn0 11960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 6 ∈ ℕ0
364		2nn0 11956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 2 ∈ ℕ0
365	27, 364	nn0addcli 11976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ∈ ℕ0
366		5p2e7 11835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (5 + 2) = 7
367		7re 11772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 7 ∈ ℝ
368	367, 364	nn0addge1i 11987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ 7 ≤ (7 + 2)
369		7p2e9 11840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (7 + 2) = 9
370	368, 369	breqtri 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 7 ≤ 9
371	366, 370	eqbrtri 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ≤ 9
372	362, 363, 365, 371	declei 12178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (5 + 2) ≤ ;16
373	372	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) ≤ ;16)
374	206, 13, 274, 17	ldiv 11517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((5 · 2) = ;10 ↔ 5 = (;10 / 2)))
375	269, 374	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 5 = (;10 / 2))
376	375	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) = ((;10 / 2) + 2))
377		4t4e16 12241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (4 · 4) = ;16
378	377	eqcomi 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ;16 = (4 · 4)
379	378	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → ;16 = (4 · 4))
380	337	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 4 = (2↑2))
381	380	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (4 · 4) = (4 · (2↑2)))
382	379, 381	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ;16 = (4 · (2↑2)))
383	373, 376, 382	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ≤ (4 · (2↑2)))
384	346, 348, 339, 361, 383	letrd 10840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385	345, 384	eqbrtrd 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
386	3, 5, 7	ltled 10831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → 0 ≤ 4)
387	364	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ ℕ0)
388	37, 325, 387, 124, 359	leexp1ad 39564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389	338, 340, 5, 386, 388	lemul2ad 11623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390	335, 339, 341, 385, 389	letrd 10840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
391	37, 326	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392	391	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393	326	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394	274, 392, 393, 333	divdird 11497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396	395	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398	397	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399	398, 180	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400	399	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
401	396, 400	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
402	394, 401	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
403	402	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404		2p1e3 11821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 + 1) = 3
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 + 1) = 3)
406	302	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 3 ∈ ℂ)
407	406, 53, 13	subadd2d 11059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408	405, 407	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (3 − 1) = 2)
409	408	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 2 = (3 − 1))
410	409	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411	410	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
412	3, 330	gtned 10818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ≠ 0)
413	342, 412, 239, 296	expsubd 13576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414	413	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415	411, 414	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 4 ∈ ℂ)
417	325, 112	reexpcld 13582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418	417	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419	416, 418, 393, 333	divassd 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420	419	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421	415, 420	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422	390, 403, 421	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423	287, 391	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
424	5, 417	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425	423, 424, 332	lediv1d 12523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
427	87	uzidd 12303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ (ℤ≥‘2))
428	427, 39	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+))
429		relogbval 25462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431	430	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432	431	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433	432	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) = (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434	430	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
435	12, 18, 26, 112	expdivd 13579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436	434, 435	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437	436	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438	426, 433, 437	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439	292, 293, 299, 323, 438	letrd 10840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
440	12	exp1d 13560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441	440	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442	441	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 / (log‘𝐴)) = (;10 / ((log‘𝐴)↑1)))
443	13, 156, 281, 282	divassd 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
444	12, 18, 26, 91	expdivd 13579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445	444	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446	445	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447	443, 446	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448	447	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449	442, 448	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450	113	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
451	18, 112	expcld 13565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℂ)
452	416, 450, 451, 297	divassd 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453	452	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454	439, 449, 453	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455	285, 454	eqbrtrd 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456	281, 282	dividd 11457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457	456	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458	457	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461	460	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463	462, 451, 297	divcld 11459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464	463	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465	464	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466	455, 461, 465	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) ∈ ℂ)
468	467	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = (;10 / ((log‘𝐴)↑1)))
469	468	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · 1))
470	18, 26	dividd 11457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2) / (log‘2)) = 1)
471	470	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = ((log‘2) / (log‘2)))
472	471	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473	469, 472	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474	274, 156, 18, 18, 247, 26	divmuldivd 11500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475	473, 474	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
476	18	exp1d 13560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑1) = (log‘2))
477	476	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478		df-2 11742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 2 = (1 + 1)
479	478	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 2 = (1 + 1))
480	479	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
481	18, 91, 91	expaddd 13567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482	480, 481	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483	482	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484	477, 483	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (log‘2) = ((log‘2)↑1))
487	486	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488	471, 487	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489	488	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490	476, 18	eqeltrd 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
491	476, 26	eqnetrd 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
492	462, 451, 18, 490, 297, 491	divmuldivd 11500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494	466, 485, 493	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496	156, 18, 247, 26	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497	274, 18, 495, 496	div23d 11496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498	277, 18, 155, 88	div23d 11496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499	497, 498	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
502	18, 91, 112	expaddd 13567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503	501, 502	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504	503	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505	504	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508	287, 507, 496	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509	508	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510	509, 278, 18	adddird 10709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
513	462, 18, 117, 512	div23d 11496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514	506, 511, 513	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516	515, 85, 88	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517	508, 516	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518	114, 115, 120	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519	517, 518, 135	lemul1d 12520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521	280, 520	eqbrtrd 5057	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
523	53, 277, 155, 88	div12d 11495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524	522, 523	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . . 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	mulid1d 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526	525	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527	526	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528	521, 524, 527	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . . 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 11457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
530	529	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 1 = (𝐴 / 𝐴))
531	530	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
532	2, 2, 495, 11, 496	divdiv1d 11490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533	531, 532	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534	533	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535		eqidd 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536	530	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537	536	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538	535, 537	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539	534, 538	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . . 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 11494	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541	528, 539, 540	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
542	2, 495	mulcomd 10705	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543	156, 18, 2	mulassd 10707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544	542, 543	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545	544	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546	545	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
547	2, 2, 155, 11, 88	divdiv1d 11490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
548	2, 155	mulcomd 10705	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549	548	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550	547, 549	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551	550	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552	546, 551	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . . 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 2759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554	530	oveq1d 7170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555	553, 554	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556	555	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557	541, 552, 556	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558	156, 261	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559	156, 261, 247, 262	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560	274, 558, 2, 559	div32d 11482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561	560	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562	155, 2	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563	155, 2, 88, 11	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564	277, 562, 2, 563	div32d 11482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565	564	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566	561, 565	oveq12d 7173	. . . . . . . . . . . . . . . . . . . . . . 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 11490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
568	2, 117	mulcomd 10705	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569	568	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570	567, 569	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571	570	oveq2d 7171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572	557, 566, 571	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
573	43, 1	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
574	92, 573	remulcld 10714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575	287, 574, 559	redivcld 11511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576	575	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577	157, 94	eqeltrrd 2853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578	577	recnd 10712	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579	576, 578, 2	adddird 10709	. . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . . . 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 13565	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582	416, 581	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583	117, 2	mulcld 10704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584	117, 2, 512, 11	mulne0d 11335	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585	582, 583, 2, 584	div32d 11482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586	585	eqcomd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587	572, 580, 586	3brtr3d 5066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588	575, 577	readdcld 10713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589	588, 122, 39	lemul1d 12520	. . . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591	271, 590	eqbrtrd 5057	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592	267, 591	eqbrtrd 5057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593	259, 592	eqbrtrd 5057	. . . . . . . . . . . . . . . . 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 5057	. . . . . . . . . . . . . . . 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 5057	. . . . . . . . . . . . . . 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 5057	. . . . . . . . . . . . . 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 5057	. . . . . . . . . . . . 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 5057	. . . . . . . . . . . 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 5057	. . . . . . . . . . 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 5057	. . . . . . . . . 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 5057	. . . . . . . . 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 5057	. . . . . . . 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 5057	. . . . . . 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 5057	. . . . . 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 5057	. . . . 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 5057	. . . 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 10840	. . 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 5057	. 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 587	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610	609	eqcomd 2764	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611	610	oveq1d 7170	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612	611	oveq1d 7170	. . . . . . 7 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613	612	oveq1d 7170	. . . . . 6 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614	613	oveq2d 7171	. . . . 5 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615		5cn 11767	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
616	615	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℂ)
617	616, 207	mulcld 10704	. . . . . . . . . . . . 13 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618	617	mulid1d 10701	. . . . . . . . . . . 12 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619	618	eqcomd 2764	. . . . . . . . . . 11 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620		eqidd 2759	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621		df-5 11745	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 = (4 + 1)
622	621	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 5 = (4 + 1))
623	622	oveq2d 7171	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
624	18, 91, 77	expaddd 13567	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625	623, 624	eqtrd 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626	476	oveq2d 7171	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627	625, 626	eqtrd 2793	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628	627	oveq1d 7170	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629	620, 628	eqtrd 2793	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630	117, 18, 2	mulassd 10707	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631	629, 630	eqtrd 2793	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
632	18, 2	mulcomd 10705	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633	632	oveq2d 7171	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634	631, 633	eqtrd 2793	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635	619, 634	oveq12d 7173	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
636	2, 18	mulcld 10704	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
637	2, 18, 11, 26	mulne0d 11335	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638	186, 117, 53, 636, 120, 637	divmuldivd 11500	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639	638	eqcomd 2764	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640	635, 639	eqtrd 2793	. . . . . . . . 9 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641	206, 207, 117, 120	divassd 11494	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642	641	oveq1d 7170	. . . . . . . . 9 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643	640, 642	eqtrd 2793	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
644	12, 18, 26, 77	expdivd 13579	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645	644	eqcomd 2764	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646	645	oveq2d 7171	. . . . . . . . 9 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647	646	oveq1d 7170	. . . . . . . 8 ⊢ (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648	643, 647	eqtrd 2793	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649	610	oveq1d 7170	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650	649	oveq2d 7171	. . . . . . . 8 ⊢ (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651	650	oveq1d 7170	. . . . . . 7 ⊢ (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652	648, 651	eqtrd 2793	. . . . . 6 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653	342, 77	expcld 13565	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654	616, 653	mulcld 10704	. . . . . . . . 9 ⊢ (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
655	39	rpne0d 12482	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
656	2, 18, 655, 26	mulne0d 11335	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657	636, 656	reccld 11452	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658	654, 657	mulcld 10704	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659	658	addid1d 10883	. . . . . . 7 ⊢ (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660	659	eqcomd 2764	. . . . . 6 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661	652, 660	eqtrd 2793	. . . . 5 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662	614, 661	oveq12d 7173	. . . 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 7171	. . 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 11806	. . . . . . 7 ⊢ 1 = (2 − 1)
665	664	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 = (2 − 1))
666	665	oveq2d 7171	. . . . 5 ⊢ (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667	666	oveq1d 7170	. . . 4 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668	667	oveq2d 7171	. . 3 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669	663, 668	oveq12d 7173	. 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 11764	. . . . 5 ⊢ 4 ∈ ℂ
671	670	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
672	671, 117, 581, 2, 120, 655	divmuldivd 11500	. . 3 ⊢ (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673	672	eqcomd 2764	. 2 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674	608, 669, 673	3brtr3d 5066	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 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   class class class wbr 5035  ‘cfv 6339  (class class class)co 7155  ℂcc 10578  ℝcr 10579  0cc0 10580  1c1 10581   + caddc 10583   · cmul 10585   < clt 10718   ≤ cle 10719   − cmin 10913  -cneg 10914   / cdiv 11340  ℕcn 11679  2c2 11734  3c3 11735  4c4 11736  5c5 11737  6c6 11738  7c7 11739  9c9 11741  ℕ₀cn0 11939  ℤcz 12025  ;cdc 12142  ℤ_≥cuz 12287  ℝ⁺crp 12435  ↑cexp 13484  eceu 15469  logclog 25250   log_b clogb 25454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-inf2 9142  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657  ax-pre-sup 10658  ax-addf 10659  ax-mulf 10660

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-iin 4889  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-of 7410  df-om 7585  df-1st 7698  df-2nd 7699  df-supp 7841  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-2o 8118  df-er 8304  df-map 8423  df-pm 8424  df-ixp 8485  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-fsupp 8872  df-fi 8913  df-sup 8944  df-inf 8945  df-oi 9012  df-card 9406  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-nn 11680  df-2 11742  df-3 11743  df-4 11744  df-5 11745  df-6 11746  df-7 11747  df-8 11748  df-9 11749  df-n0 11940  df-z 12026  df-dec 12143  df-uz 12288  df-q 12394  df-rp 12436  df-xneg 12553  df-xadd 12554  df-xmul 12555  df-ioo 12788  df-ioc 12789  df-ico 12790  df-icc 12791  df-fz 12945  df-fzo 13088  df-fl 13216  df-mod 13292  df-seq 13424  df-exp 13485  df-fac 13689  df-bc 13718  df-hash 13746  df-shft 14479  df-cj 14511  df-re 14512  df-im 14513  df-sqrt 14647  df-abs 14648  df-limsup 14881  df-clim 14898  df-rlim 14899  df-sum 15096  df-ef 15474  df-e 15475  df-sin 15476  df-cos 15477  df-pi 15479  df-struct 16548  df-ndx 16549  df-slot 16550  df-base 16552  df-sets 16553  df-ress 16554  df-plusg 16641  df-mulr 16642  df-starv 16643  df-sca 16644  df-vsca 16645  df-ip 16646  df-tset 16647  df-ple 16648  df-ds 16650  df-unif 16651  df-hom 16652  df-cco 16653  df-rest 16759  df-topn 16760  df-0g 16778  df-gsum 16779  df-topgen 16780  df-pt 16781  df-prds 16784  df-xrs 16838  df-qtop 16843  df-imas 16844  df-xps 16846  df-mre 16920  df-mrc 16921  df-acs 16923  df-mgm 17923  df-sgrp 17972  df-mnd 17983  df-submnd 18028  df-mulg 18297  df-cntz 18519  df-cmn 18980  df-psmet 20163  df-xmet 20164  df-met 20165  df-bl 20166  df-mopn 20167  df-fbas 20168  df-fg 20169  df-cnfld 20172  df-top 21599  df-topon 21616  df-topsp 21638  df-bases 21651  df-cld 21724  df-ntr 21725  df-cls 21726  df-nei 21803  df-lp 21841  df-perf 21842  df-cn 21932  df-cnp 21933  df-haus 22020  df-tx 22267  df-hmeo 22460  df-fil 22551  df-fm 22643  df-flim 22644  df-flf 22645  df-xms 23027  df-ms 23028  df-tms 23029  df-cncf 23584  df-limc 24570  df-dv 24571  df-log 25252  df-cxp 25253  df-logb 25455

This theorem is referenced by:  aks4d1p1p5  39667