Theorem aks4d1p1p7 42033

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 11261	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		0red 11236	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
4		4re 12322	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℝ
5	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
6		4pos 12345	. . . . . . . . . . . . . . 15 ⊢ 0 < 4
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 4)
8		aks4d1p1p7.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ≤ 𝐴)
9	3, 5, 1, 7, 8	ltletrd 11393	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝐴)
10	3, 9	ltned 11369	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 𝐴)
11	10	necomd 2987	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
12	2, 11	logcld 26529	. . . . . . . . . 10 ⊢ (𝜑 → (log‘𝐴) ∈ ℂ)
13		2cnd 12316	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
14		2pos 12341	. . . . . . . . . . . . . 14 ⊢ 0 < 2
15	14	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 2)
16	3, 15	ltned 11369	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 2)
17	16	necomd 2987	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≠ 0)
18	13, 17	logcld 26529	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ∈ ℂ)
19		1lt2 12409	. . . . . . . . . . . . . 14 ⊢ 1 < 2
20		2rp 13011	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
21		loggt0b 26591	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
22	20, 21	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (0 < (log‘2) ↔ 1 < 2)
23	19, 22	mpbir 231	. . . . . . . . . . . . 13 ⊢ 0 < (log‘2)
24	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (log‘2))
25	3, 24	ltned 11369	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≠ (log‘2))
26	25	necomd 2987	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ≠ 0)
27		5nn0 12519	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 5 ∈ ℕ0)
29	12, 18, 26, 28	expdivd 14176	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
30	29	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
31	30	oveq1d 7418	. . . . . . 7 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
32	31	oveq2d 7419	. . . . . 6 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
33	32	oveq1d 7418	. . . . 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 7419	. . . 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 7418	. . 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 12312	. . . . . . 7 ⊢ 2 ∈ ℝ
37	36	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
38		1red 11234	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
39	1, 9	elrpd 13046	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
40	39	relogcld 26582	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)
41	40, 28	reexpcld 14179	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
42	20	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℝ+)
43	42	relogcld 26582	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ)
44	43, 28	reexpcld 14179	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ)
45	28	nn0zd 12612	. . . . . . . . . . . 12 ⊢ (𝜑 → 5 ∈ ℤ)
46	18, 26, 45	expne0d 14168	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ≠ 0)
47	41, 44, 46	redivcld 12067	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
48	47, 38	readdcld 11262	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
49	48, 43	remulcld 11263	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
50	12, 28	expcld 14162	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
51	18, 28	expcld 14162	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℂ)
52	50, 51, 46	divcld 12015	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53		1cnd 11228	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
54	52, 53	addcld 11252	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
55	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 2)
56	37, 55	rplogcld 26588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
57	56, 45	rpexpcld 14263	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58		1re 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
59		3nn0 12517	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ0
60	58, 59	nn0addge2i 12548	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ≤ (3 + 1)
61	60	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ (3 + 1))
62		df-4 12303	. . . . . . . . . . . . . . . . 17 ⊢ 4 = (3 + 1)
63	61, 62	breqtrrdi 5161	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 4)
64	38, 5, 1, 63, 8	letrd 11390	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ 𝐴)
65	1, 64	logge0d 26589	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (log‘𝐴))
66	40, 28, 65	expge0d 14180	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑5))
67	41, 57, 66	divge0d 13089	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
68	47	ltp1d 12170	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
69	3, 47, 48, 67, 68	lelttrd 11391	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
70	3, 69	ltned 11369	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
71	70	necomd 2987	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
72	54, 18, 71, 26	mulne0d 11887	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
73	38, 49, 72	redivcld 12067	. . . . . . 7 ⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74		5re 12325	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
75	74	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 5 ∈ ℝ)
76		4nn0 12518	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
77	76	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ0)
78	40, 77	reexpcld 14179	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
79	75, 78	remulcld 11263	. . . . . . . 8 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
80	44, 1	remulcld 11263	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
81	51, 2, 46, 11	mulne0d 11887	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
82	79, 80, 81	redivcld 12067	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
83	73, 82	remulcld 11263	. . . . . 6 ⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
84	37, 83	remulcld 11263	. . . . 5 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
85	43	resqcld 14141	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℝ)
86		2z 12622	. . . . . . . . 9 ⊢ 2 ∈ ℤ
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
88	18, 26, 87	expne0d 14168	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ≠ 0)
89	37, 85, 88	redivcld 12067	. . . . . 6 ⊢ (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90		1nn0 12515	. . . . . . . . 9 ⊢ 1 ∈ ℕ0
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℕ0)
92	40, 91	reexpcld 14179	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
93	92, 1, 11	redivcld 12067	. . . . . 6 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
94	89, 93	remulcld 11263	. . . . 5 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
95	84, 94	readdcld 11262	. . . 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 11263	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97		1lt4 12414	. . . . . . . . . . . . . . . 16 ⊢ 1 < 4
98	97	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 4)
99	38, 5, 1, 98, 8	ltletrd 11393	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 𝐴)
100		loggt0b 26591	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
101	39, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
102	99, 101	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (log‘𝐴))
103	3, 102	ltned 11369	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ (log‘𝐴))
104	103	necomd 2987	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ≠ 0)
105	12, 104, 45	expne0d 14168	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ≠ 0)
106	50, 51, 105, 46	divne0d 12031	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
107	52, 18, 106, 26	mulne0d 11887	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
108	38, 96, 107	redivcld 12067	. . . . . . 7 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109	108, 82	remulcld 11263	. . . . . 6 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
110	37, 109	remulcld 11263	. . . . 5 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111	110, 94	readdcld 11262	. . . 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 14179	. . . . . 6 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
114	5, 113	remulcld 11263	. . . . 5 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
115	43, 77	reexpcld 14179	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℝ)
116	115, 1	remulcld 11263	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
117	18, 77	expcld 14162	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℂ)
118		4z 12624	. . . . . . . 8 ⊢ 4 ∈ ℤ
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ∈ ℤ)
120	18, 26, 119	expne0d 14168	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
121	117, 2, 120, 11	mulne0d 11887	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122	114, 116, 121	redivcld 12067	. . . 4 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123		0le2 12340	. . . . . . 7 ⊢ 0 ≤ 2
124	123	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ≤ 2)
125	57, 39	rpmulcld 13065	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
126	28	nn0ge0d 12563	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 5)
127	40, 77, 65	expge0d 14180	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑4))
128	75, 78, 126, 127	mulge0d 11812	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
129	79, 125, 128	divge0d 13089	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
130	1, 99	rplogcld 26588	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+)
131	130, 45	rpexpcld 14263	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132	131, 57	rpdivcld 13066	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133	132, 56	rpmulcld 13065	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
134	24, 22	sylib 218	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 2)
135	37, 134	rplogcld 26588	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
136	135, 45	rpexpcld 14263	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
137	41, 136, 66	divge0d 13089	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
138	47, 137	ge0p1rpd 13079	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139	138, 135	rpmulcld 13065	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140		0le1 11758	. . . . . . . . 9 ⊢ 0 ≤ 1
141	140	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
142	135	rpred 13049	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℝ)
143	135	rpge0d 13053	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (log‘2))
144	47	lep1d 12171	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
145	47, 48, 142, 143, 144	lemul1ad 12179	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146	133, 139, 38, 141, 145	lediv2ad 13071	. . . . . . 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 12179	. . . . . 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 12180	. . . . 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 11849	. . . 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 12052	. . . . . . . . . 10 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151	150	eqcomd 2741	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152	151	oveq2d 7419	. . . . . . . 8 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153	152	oveq1d 7418	. . . . . . 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 7419	. . . . . 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 14160	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℂ)
156	12, 91	expcld 14162	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
157	13, 155, 156, 2, 88, 11	divmuldivd 12056	. . . . . 6 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158	154, 157	oveq12d 7421	. . . . 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 11253	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
160	50, 18, 105, 26	mulne0d 11887	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
161	53, 159, 51, 160, 46	divdiv2d 12047	. . . . . . . . . 10 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162	161	oveq1d 7418	. . . . . . . . 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 7419	. . . . . . . 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 11253	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165	164, 159, 160	divcld 12015	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
166	82	recnd 11261	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
167	13, 165, 166	mulassd 11256	. . . . . . . . 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 2741	. . . . . . . 8 ⊢ (𝜑 → (2 · (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
169	163, 168	eqtrd 2770	. . . . . . 7 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
170	169	oveq1d 7418	. . . . . 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 12050	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172	171	eqcomd 2741	. . . . . . . . 9 ⊢ (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173	172	oveq1d 7418	. . . . . . . 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 7418	. . . . . . 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 11256	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176	175	eqcomd 2741	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177	176	oveq1d 7418	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178	177	oveq1d 7418	. . . . . . . . 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 7418	. . . . . . . 8 ⊢ (𝜑 → ((((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
180	13	mulridd 11250	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 1) = 2)
181	180	oveq1d 7418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182	181	oveq1d 7418	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183	182	oveq1d 7418	. . . . . . . . . 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 7418	. . . . . . . . 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 11253	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
186	79	recnd 11261	. . . . . . . . . . . 12 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
187	51, 2	mulcld 11253	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188	185, 159, 186, 187, 160, 81	divmuldivd 12056	. . . . . . . . . . 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 7418	. . . . . . . . . 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 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191	190	oveq2d 7419	. . . . . . . . . . . 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 7418	. . . . . . . . . . 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 11254	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
194	18, 51, 2	mulassd 11256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195	194	eqcomd 2741	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196	195	oveq2d 7419	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197	193, 196	oveq12d 7421	. . . . . . . . . . . . 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 7418	. . . . . . . . . . . 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 11253	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200	199, 2	mulcld 11253	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
201	18, 51, 26, 46	mulne0d 11887	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202	199, 2, 201, 11	mulne0d 11887	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203	186, 50, 185, 200, 105, 202	divmuldivd 12056	. . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . 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 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℂ)
207	78	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208	206, 207, 50, 105	divassd 12050	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209	194	oveq2d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210	208, 209	oveq12d 7421	. . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . 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 12612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 4 ∈ ℤ)
213	12, 104, 45, 212	expsubd 14173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214	213	eqcomd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215		4p1e5 12384	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 1) = 5
216	74	recni 11247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℂ
217	4	recni 11247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℂ
218		ax-1cn 11185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℂ
219	216, 217, 218	subaddi 11568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((5 − 4) = 1 ↔ (4 + 1) = 5)
220	215, 219	mpbir 231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (5 − 4) = 1
221	220	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 − 4) = 1)
222	53	subid1d 11581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 − 0) = 1)
223	221, 222	eqtr4d 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 − 4) = (1 − 0))
224	206, 217	jctir 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225		0cnd 11226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ∈ ℂ)
226	53, 225	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227		subeqrev 11657	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228	224, 226, 227	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229	223, 228	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (4 − 5) = (0 − 1))
230		df-neg 11467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 = (0 − 1)
231	229, 230	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (4 − 5) = -1)
232	231	oveq2d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233	214, 232	eqtrd 2770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234	233	oveq2d 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
235	13, 18, 51, 187, 26, 81	divmuldivd 12056	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236	235	eqcomd 2741	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237	234, 236	oveq12d 7421	. . . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . . 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 12621	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℤ)
240	12, 104, 239	expnegd 14169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241	240	oveq2d 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
242	51, 51, 2, 46, 11	divdiv1d 12046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243	242	eqcomd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244	243	oveq2d 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245	241, 244	oveq12d 7421	. . . . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . . . 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 14168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248	206, 53, 156, 247	divassd 12050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249	248	eqcomd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
250	51, 46	dividd 12013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251	250	oveq1d 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252	251	oveq2d 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253	249, 252	oveq12d 7421	. . . . . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
255	206	mulridd 11250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (5 · 1) = 5)
256	255	oveq1d 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
257	13, 18, 53, 2, 26, 11	divmuldivd 12056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258	256, 257	oveq12d 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259	258	oveq1d 7418	. . . . . . . . . . . . . . . . . 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 2834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · 1) ∈ ℂ)
261	18, 2	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
262	18, 2, 26, 11	mulne0d 11887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263	206, 156, 260, 261, 247, 262	divmuldivd 12056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264	180	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · (2 · 1)) = (5 · 2))
265	264	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266	263, 265	eqtrd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267	266	oveq1d 7418	. . . . . . . . . . . . . . . . . . 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 12806	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (5 · 2) = ;10
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · 2) = ;10)
270	269	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271	270	oveq1d 7418	. . . . . . . . . . . . . . . . . . . 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 12724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ;10 ∈ ℕ0
273	272	nn0cni 12511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ;10 ∈ ℂ
274	273	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ;10 ∈ ℂ)
275	274	mulridd 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (;10 · 1) = ;10)
276	275	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 / (((log‘𝐴)↑1) · (log‘2))))
277	13, 156	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278	277, 155, 88	divcld 12015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279	278	mullidd 11251	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280	276, 279	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 14162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
282	18, 26, 239	expne0d 14168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
283	277, 281, 282	divcld 12015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284	283	mulridd 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285	284	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286		10re 12725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ;10 ∈ ℝ
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ;10 ∈ ℝ)
288	287, 40, 104	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ∈ ℝ)
289	40, 43, 26	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290	289, 91	reexpcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
291	37, 290	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292	288, 291	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293	287, 291	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
294	43, 112	reexpcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℝ)
295		3z 12623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 3 ∈ ℤ
296	295	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → 3 ∈ ℤ)
297	18, 26, 296	expne0d 14168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ≠ 0)
298	113, 294, 297	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
299	5, 298	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300		ere 16103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ e ∈ ℝ
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e ∈ ℝ)
302	112	nn0red 12561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 ∈ ℝ)
303		egt2lt3 16222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 < e ∧ e < 3)
304	303	simpri 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ e < 3
305	304	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → e < 3)
306		3lt4 12412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 3 < 4
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 3 < 4)
308	302, 5, 1, 307, 8	ltletrd 11393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 < 𝐴)
309	301, 302, 1, 305, 308	lttrd 11394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e < 𝐴)
310	301, 1, 309	ltled 11381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → e ≤ 𝐴)
311	301, 1	lenltd 11379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312	310, 311	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ¬ 𝐴 < e)
313		loglt1b 26593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
314	39, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315	312, 314	mtbird 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ¬ (log‘𝐴) < 1)
316	38, 40	lenltd 11379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317	315, 316	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 1 ≤ (log‘𝐴))
318		10nn 12722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ;10 ∈ ℕ
319	318	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ;10 ∈ ℕ)
320		nnledivrp 13119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((;10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
321	319, 130, 320	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
322	317, 321	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ≤ ;10)
323	288, 287, 291, 322	leadd1dd 11849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
324	38, 55	gtned 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≠ 1)
325	37, 15, 1, 9, 324	relogbcld 41932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ)
326	325, 91	reexpcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
327	42, 55	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328		logbgt0b 26753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
329	39, 327, 328	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
330	99, 329	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 0 < (2 logb 𝐴))
331	325, 330	elrpd 13046	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332	331, 239	rpexpcld 14263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333	332	rpne0d 13054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334	287, 326, 333	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335	334, 37	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336		sq2 14213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (2↑2) = 4
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2↑2) = 4)
338	337, 5	eqeltrd 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ∈ ℝ)
339	5, 338	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ∈ ℝ)
340	325	resqcld 14141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
341	5, 340	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342	325	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℂ)
343	342	exp1d 14157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344	343	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) = (;10 / (2 logb 𝐴)))
345	344	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 / (2 logb 𝐴)) + 2))
346	345, 335	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347	287	rehalfcld 12486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
348	347, 37	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ∈ ℝ)
349	344, 334	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ∈ ℝ)
350	287, 37, 17	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
351	272	nn0ge0i 12526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 0 ≤ ;10
352	351	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 0 ≤ ;10)
353	42, 324, 87	relogbexpd 41933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
354	353	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 = (2 logb (2↑2)))
355	337	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356	354, 355	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 2 = (2 logb 4))
357	37	leidd 11801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 ≤ 2)
358	87, 357, 5, 7, 1, 9, 8	logblebd 41935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359	356, 358	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≤ (2 logb 𝐴))
360	42, 331, 287, 352, 359	lediv2ad 13071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ≤ (;10 / 2))
361	349, 350, 37, 360	leadd1dd 11849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ ((;10 / 2) + 2))
362		1nn 12249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 1 ∈ ℕ
363		6nn0 12520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 6 ∈ ℕ0
364		2nn0 12516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 2 ∈ ℕ0
365	27, 364	nn0addcli 12536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ∈ ℕ0
366		5p2e7 12394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (5 + 2) = 7
367		7re 12331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 7 ∈ ℝ
368	367, 364	nn0addge1i 12547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ 7 ≤ (7 + 2)
369		7p2e9 12399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (7 + 2) = 9
370	368, 369	breqtri 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 7 ≤ 9
371	366, 370	eqbrtri 5140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ≤ 9
372	362, 363, 365, 371	declei 12742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (5 + 2) ≤ ;16
373	372	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) ≤ ;16)
374	206, 13, 274, 17	ldiv 12073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((5 · 2) = ;10 ↔ 5 = (;10 / 2)))
375	269, 374	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 5 = (;10 / 2))
376	375	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) = ((;10 / 2) + 2))
377		4t4e16 12805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (4 · 4) = ;16
378	377	eqcomi 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ;16 = (4 · 4)
379	378	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → ;16 = (4 · 4))
380	337	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 4 = (2↑2))
381	380	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (4 · 4) = (4 · (2↑2)))
382	379, 381	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ;16 = (4 · (2↑2)))
383	373, 376, 382	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ≤ (4 · (2↑2)))
384	346, 348, 339, 361, 383	letrd 11390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385	345, 384	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
386	3, 5, 7	ltled 11381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → 0 ≤ 4)
387	364	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ ℕ0)
388	37, 325, 387, 124, 359	leexp1ad 14192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389	338, 340, 5, 386, 388	lemul2ad 12180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390	335, 339, 341, 385, 389	letrd 11390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
391	37, 326	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392	391	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393	326	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394	274, 392, 393, 333	divdird 12053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396	395	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398	397	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399	398, 180	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400	399	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
401	396, 400	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
402	394, 401	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
403	402	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404		2p1e3 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 + 1) = 3
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 + 1) = 3)
406	302	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 3 ∈ ℂ)
407	406, 53, 13	subadd2d 11611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408	405, 407	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (3 − 1) = 2)
409	408	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 2 = (3 − 1))
410	409	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411	410	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
412	3, 330	gtned 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ≠ 0)
413	342, 412, 239, 296	expsubd 14173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414	413	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415	411, 414	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 4 ∈ ℂ)
417	325, 112	reexpcld 14179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418	417	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419	416, 418, 393, 333	divassd 12050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420	419	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421	415, 420	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422	390, 403, 421	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423	287, 391	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
424	5, 417	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425	423, 424, 332	lediv1d 13095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
427	87	uzidd 12866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ (ℤ≥‘2))
428	427, 39	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+))
429		relogbval 26732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431	430	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432	431	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433	432	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) = (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434	430	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
435	12, 18, 26, 112	expdivd 14176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436	434, 435	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437	436	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438	426, 433, 437	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439	292, 293, 299, 323, 438	letrd 11390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
440	12	exp1d 14157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441	440	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442	441	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 / (log‘𝐴)) = (;10 / ((log‘𝐴)↑1)))
443	13, 156, 281, 282	divassd 12050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
444	12, 18, 26, 91	expdivd 14176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445	444	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446	445	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447	443, 446	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448	447	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449	442, 448	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450	113	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
451	18, 112	expcld 14162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℂ)
452	416, 450, 451, 297	divassd 12050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453	452	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454	439, 449, 453	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455	285, 454	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456	281, 282	dividd 12013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457	456	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458	457	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · (((log‘2)↑1) / ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
460	458, 459	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461	460	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463	462, 451, 297	divcld 12015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464	463	mulridd 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465	464	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466	455, 461, 465	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) ∈ ℂ)
468	467	mulridd 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = (;10 / ((log‘𝐴)↑1)))
469	468	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · 1))
470	18, 26	dividd 12013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2) / (log‘2)) = 1)
471	470	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = ((log‘2) / (log‘2)))
472	471	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473	469, 472	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474	274, 156, 18, 18, 247, 26	divmuldivd 12056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475	473, 474	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
476	18	exp1d 14157	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑1) = (log‘2))
477	476	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478		df-2 12301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 2 = (1 + 1)
479	478	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 2 = (1 + 1))
480	479	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
481	18, 91, 91	expaddd 14164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482	480, 481	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483	482	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484	477, 483	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (log‘2) = ((log‘2)↑1))
487	486	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488	471, 487	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489	488	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490	476, 18	eqeltrd 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
491	476, 26	eqnetrd 2999	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
492	462, 451, 18, 490, 297, 491	divmuldivd 12056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
493	489, 492	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494	466, 485, 493	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496	156, 18, 247, 26	mulne0d 11887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497	274, 18, 495, 496	div23d 12052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498	277, 18, 155, 88	div23d 12052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499	497, 498	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
502	18, 91, 112	expaddd 14164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503	501, 502	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504	503	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505	504	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508	287, 507, 496	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509	508	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510	509, 278, 18	adddird 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
513	462, 18, 117, 512	div23d 12052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514	506, 511, 513	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516	515, 85, 88	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517	508, 516	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518	114, 115, 120	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519	517, 518, 135	lemul1d 13092	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521	280, 520	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12050	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
523	53, 277, 155, 88	div12d 12051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524	522, 523	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))))
525	462	mulridd 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526	525	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527	526	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528	521, 524, 527	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . . 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 12013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
530	529	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 1 = (𝐴 / 𝐴))
531	530	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
532	2, 2, 495, 11, 496	divdiv1d 12046	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533	531, 532	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534	533	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535		eqidd 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536	530	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537	536	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538	535, 537	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539	534, 538	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . . 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 12050	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541	528, 539, 540	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
542	2, 495	mulcomd 11254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543	156, 18, 2	mulassd 11256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544	542, 543	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545	544	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546	545	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
547	2, 2, 155, 11, 88	divdiv1d 12046	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
548	2, 155	mulcomd 11254	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549	548	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550	547, 549	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551	550	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552	546, 551	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554	530	oveq1d 7418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555	553, 554	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556	555	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557	541, 552, 556	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558	156, 261	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559	156, 261, 247, 262	mulne0d 11887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560	274, 558, 2, 559	div32d 12038	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561	560	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562	155, 2	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563	155, 2, 88, 11	mulne0d 11887	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564	277, 562, 2, 563	div32d 12038	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565	564	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566	561, 565	oveq12d 7421	. . . . . . . . . . . . . . . . . . . . . . 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 12046	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
568	2, 117	mulcomd 11254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569	568	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570	567, 569	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571	570	oveq2d 7419	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572	557, 566, 571	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
573	43, 1	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
574	92, 573	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575	287, 574, 559	redivcld 12067	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576	575	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577	157, 94	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578	577	recnd 11261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579	576, 578, 2	adddird 11258	. . . . . . . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . . . . 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 14162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582	416, 581	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583	117, 2	mulcld 11253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584	117, 2, 512, 11	mulne0d 11887	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585	582, 583, 2, 584	div32d 12038	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586	585	eqcomd 2741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587	572, 580, 586	3brtr3d 5150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588	575, 577	readdcld 11262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589	588, 122, 39	lemul1d 13092	. . . . . . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591	271, 590	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592	267, 591	eqbrtrd 5141	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593	259, 592	eqbrtrd 5141	. . . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . 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 5141	. . . . . . . . . . . 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 5141	. . . . . . . . . . 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 5141	. . . . . . . . . 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 5141	. . . . . . . . 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 5141	. . . . . . . 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 5141	. . . . . . 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 5141	. . . . . 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 5141	. . . . 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 5141	. . . 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 11390	. . 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 5141	. 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 584	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610	609	eqcomd 2741	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611	610	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612	611	oveq1d 7418	. . . . . . 7 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613	612	oveq1d 7418	. . . . . 6 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614	613	oveq2d 7419	. . . . 5 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615		5cn 12326	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
616	615	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℂ)
617	616, 207	mulcld 11253	. . . . . . . . . . . . 13 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618	617	mulridd 11250	. . . . . . . . . . . 12 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619	618	eqcomd 2741	. . . . . . . . . . 11 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620		eqidd 2736	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621		df-5 12304	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 = (4 + 1)
622	621	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 5 = (4 + 1))
623	622	oveq2d 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
624	18, 91, 77	expaddd 14164	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625	623, 624	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626	476	oveq2d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627	625, 626	eqtrd 2770	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628	627	oveq1d 7418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629	620, 628	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630	117, 18, 2	mulassd 11256	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631	629, 630	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
632	18, 2	mulcomd 11254	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633	632	oveq2d 7419	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634	631, 633	eqtrd 2770	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635	619, 634	oveq12d 7421	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
636	2, 18	mulcld 11253	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
637	2, 18, 11, 26	mulne0d 11887	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638	186, 117, 53, 636, 120, 637	divmuldivd 12056	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639	638	eqcomd 2741	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640	635, 639	eqtrd 2770	. . . . . . . . 9 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641	206, 207, 117, 120	divassd 12050	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642	641	oveq1d 7418	. . . . . . . . 9 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643	640, 642	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
644	12, 18, 26, 77	expdivd 14176	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645	644	eqcomd 2741	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646	645	oveq2d 7419	. . . . . . . . 9 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647	646	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648	643, 647	eqtrd 2770	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649	610	oveq1d 7418	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650	649	oveq2d 7419	. . . . . . . 8 ⊢ (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651	650	oveq1d 7418	. . . . . . 7 ⊢ (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652	648, 651	eqtrd 2770	. . . . . 6 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653	342, 77	expcld 14162	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654	616, 653	mulcld 11253	. . . . . . . . 9 ⊢ (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
655	39	rpne0d 13054	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
656	2, 18, 655, 26	mulne0d 11887	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657	636, 656	reccld 12008	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658	654, 657	mulcld 11253	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659	658	addridd 11433	. . . . . . 7 ⊢ (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660	659	eqcomd 2741	. . . . . 6 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661	652, 660	eqtrd 2770	. . . . 5 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662	614, 661	oveq12d 7421	. . . 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 7419	. . 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 12365	. . . . . . 7 ⊢ 1 = (2 − 1)
665	664	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 = (2 − 1))
666	665	oveq2d 7419	. . . . 5 ⊢ (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667	666	oveq1d 7418	. . . 4 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668	667	oveq2d 7419	. . 3 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669	663, 668	oveq12d 7421	. 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 12323	. . . . 5 ⊢ 4 ∈ ℂ
671	670	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
672	671, 117, 581, 2, 120, 655	divmuldivd 12056	. . 3 ⊢ (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673	672	eqcomd 2741	. 2 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674	608, 669, 673	3brtr3d 5150	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 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108   class class class wbr 5119  ‘cfv 6530  (class class class)co 7403  ℂcc 11125  ℝcr 11126  0cc0 11127  1c1 11128   + caddc 11130   · cmul 11132   < clt 11267   ≤ cle 11268   − cmin 11464  -cneg 11465   / cdiv 11892  ℕcn 12238  2c2 12293  3c3 12294  4c4 12295  5c5 12296  6c6 12297  7c7 12298  9c9 12300  ℕ₀cn0 12499  ℤcz 12586  ;cdc 12706  ℤ_≥cuz 12850  ℝ⁺crp 13006  ↑cexp 14077  eceu 16076  logclog 26513   log_b clogb 26724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8717  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9372  df-fi 9421  df-sup 9452  df-inf 9453  df-oi 9522  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-z 12587  df-dec 12707  df-uz 12851  df-q 12963  df-rp 13007  df-xneg 13126  df-xadd 13127  df-xmul 13128  df-ioo 13364  df-ioc 13365  df-ico 13366  df-icc 13367  df-fz 13523  df-fzo 13670  df-fl 13807  df-mod 13885  df-seq 14018  df-exp 14078  df-fac 14290  df-bc 14319  df-hash 14347  df-shft 15084  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-limsup 15485  df-clim 15502  df-rlim 15503  df-sum 15701  df-ef 16081  df-e 16082  df-sin 16083  df-cos 16084  df-pi 16086  df-struct 17164  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-hom 17293  df-cco 17294  df-rest 17434  df-topn 17435  df-0g 17453  df-gsum 17454  df-topgen 17455  df-pt 17456  df-prds 17459  df-xrs 17514  df-qtop 17519  df-imas 17520  df-xps 17522  df-mre 17596  df-mrc 17597  df-acs 17599  df-mgm 18616  df-sgrp 18695  df-mnd 18711  df-submnd 18760  df-mulg 19049  df-cntz 19298  df-cmn 19761  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-fbas 21310  df-fg 21311  df-cnfld 21314  df-top 22830  df-topon 22847  df-topsp 22869  df-bases 22882  df-cld 22955  df-ntr 22956  df-cls 22957  df-nei 23034  df-lp 23072  df-perf 23073  df-cn 23163  df-cnp 23164  df-haus 23251  df-tx 23498  df-hmeo 23691  df-fil 23782  df-fm 23874  df-flim 23875  df-flf 23876  df-xms 24257  df-ms 24258  df-tms 24259  df-cncf 24820  df-limc 25817  df-dv 25818  df-log 26515  df-cxp 26516  df-logb 26725

This theorem is referenced by:  aks4d1p1p5  42034