Theorem aks4d1p1p7 40010

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 10934	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		0red 10909	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
4		4re 11987	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℝ
5	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
6		4pos 12010	. . . . . . . . . . . . . . 15 ⊢ 0 < 4
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 4)
8		aks4d1p1p7.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ≤ 𝐴)
9	3, 5, 1, 7, 8	ltletrd 11065	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝐴)
10	3, 9	ltned 11041	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 𝐴)
11	10	necomd 2998	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
12	2, 11	logcld 25631	. . . . . . . . . 10 ⊢ (𝜑 → (log‘𝐴) ∈ ℂ)
13		2cnd 11981	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
14		2pos 12006	. . . . . . . . . . . . . 14 ⊢ 0 < 2
15	14	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 2)
16	3, 15	ltned 11041	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 2)
17	16	necomd 2998	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≠ 0)
18	13, 17	logcld 25631	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ∈ ℂ)
19		1lt2 12074	. . . . . . . . . . . . . 14 ⊢ 1 < 2
20		2rp 12664	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
21		loggt0b 25692	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
22	20, 21	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (0 < (log‘2) ↔ 1 < 2)
23	19, 22	mpbir 230	. . . . . . . . . . . . 13 ⊢ 0 < (log‘2)
24	23	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (log‘2))
25	3, 24	ltned 11041	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≠ (log‘2))
26	25	necomd 2998	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ≠ 0)
27		5nn0 12183	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 5 ∈ ℕ0)
29	12, 18, 26, 28	expdivd 13806	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
30	29	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
31	30	oveq1d 7270	. . . . . . 7 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
32	31	oveq2d 7271	. . . . . 6 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
33	32	oveq1d 7270	. . . . 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 7271	. . . 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 7270	. . 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 11977	. . . . . . 7 ⊢ 2 ∈ ℝ
37	36	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
38		1red 10907	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
39	1, 9	elrpd 12698	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
40	39	relogcld 25683	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)
41	40, 28	reexpcld 13809	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
42	20	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℝ+)
43	42	relogcld 25683	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ)
44	43, 28	reexpcld 13809	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ)
45	28	nn0zd 12353	. . . . . . . . . . . 12 ⊢ (𝜑 → 5 ∈ ℤ)
46	18, 26, 45	expne0d 13798	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ≠ 0)
47	41, 44, 46	redivcld 11733	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
48	47, 38	readdcld 10935	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
49	48, 43	remulcld 10936	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
50	12, 28	expcld 13792	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
51	18, 28	expcld 13792	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℂ)
52	50, 51, 46	divcld 11681	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53		1cnd 10901	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
54	52, 53	addcld 10925	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
55	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 2)
56	37, 55	rplogcld 25689	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
57	56, 45	rpexpcld 13890	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58		1re 10906	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
59		3nn0 12181	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ0
60	58, 59	nn0addge2i 12212	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ≤ (3 + 1)
61	60	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ (3 + 1))
62		df-4 11968	. . . . . . . . . . . . . . . . 17 ⊢ 4 = (3 + 1)
63	61, 62	breqtrrdi 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 4)
64	38, 5, 1, 63, 8	letrd 11062	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ 𝐴)
65	1, 64	logge0d 25690	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (log‘𝐴))
66	40, 28, 65	expge0d 13810	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑5))
67	41, 57, 66	divge0d 12741	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
68	47	ltp1d 11835	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
69	3, 47, 48, 67, 68	lelttrd 11063	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
70	3, 69	ltned 11041	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
71	70	necomd 2998	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
72	54, 18, 71, 26	mulne0d 11557	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
73	38, 49, 72	redivcld 11733	. . . . . . 7 ⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74		5re 11990	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
75	74	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 5 ∈ ℝ)
76		4nn0 12182	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
77	76	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ0)
78	40, 77	reexpcld 13809	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
79	75, 78	remulcld 10936	. . . . . . . 8 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
80	44, 1	remulcld 10936	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
81	51, 2, 46, 11	mulne0d 11557	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
82	79, 80, 81	redivcld 11733	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
83	73, 82	remulcld 10936	. . . . . 6 ⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
84	37, 83	remulcld 10936	. . . . 5 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
85	43	resqcld 13893	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℝ)
86		2z 12282	. . . . . . . . 9 ⊢ 2 ∈ ℤ
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
88	18, 26, 87	expne0d 13798	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ≠ 0)
89	37, 85, 88	redivcld 11733	. . . . . 6 ⊢ (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90		1nn0 12179	. . . . . . . . 9 ⊢ 1 ∈ ℕ0
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℕ0)
92	40, 91	reexpcld 13809	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
93	92, 1, 11	redivcld 11733	. . . . . 6 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
94	89, 93	remulcld 10936	. . . . 5 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
95	84, 94	readdcld 10935	. . . 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 10936	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97		1lt4 12079	. . . . . . . . . . . . . . . 16 ⊢ 1 < 4
98	97	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 4)
99	38, 5, 1, 98, 8	ltletrd 11065	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 𝐴)
100		loggt0b 25692	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
101	39, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴))
102	99, 101	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (log‘𝐴))
103	3, 102	ltned 11041	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ (log‘𝐴))
104	103	necomd 2998	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ≠ 0)
105	12, 104, 45	expne0d 13798	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ≠ 0)
106	50, 51, 105, 46	divne0d 11697	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
107	52, 18, 106, 26	mulne0d 11557	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
108	38, 96, 107	redivcld 11733	. . . . . . 7 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109	108, 82	remulcld 10936	. . . . . 6 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
110	37, 109	remulcld 10936	. . . . 5 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111	110, 94	readdcld 10935	. . . 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 13809	. . . . . 6 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
114	5, 113	remulcld 10936	. . . . 5 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
115	43, 77	reexpcld 13809	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℝ)
116	115, 1	remulcld 10936	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
117	18, 77	expcld 13792	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℂ)
118		4z 12284	. . . . . . . 8 ⊢ 4 ∈ ℤ
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ∈ ℤ)
120	18, 26, 119	expne0d 13798	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
121	117, 2, 120, 11	mulne0d 11557	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122	114, 116, 121	redivcld 11733	. . . 4 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123		0le2 12005	. . . . . . 7 ⊢ 0 ≤ 2
124	123	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ≤ 2)
125	57, 39	rpmulcld 12717	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
126	28	nn0ge0d 12226	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 5)
127	40, 77, 65	expge0d 13810	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑4))
128	75, 78, 126, 127	mulge0d 11482	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
129	79, 125, 128	divge0d 12741	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
130	1, 99	rplogcld 25689	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+)
131	130, 45	rpexpcld 13890	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132	131, 57	rpdivcld 12718	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133	132, 56	rpmulcld 12717	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
134	24, 22	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 2)
135	37, 134	rplogcld 25689	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
136	135, 45	rpexpcld 13890	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
137	41, 136, 66	divge0d 12741	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
138	47, 137	ge0p1rpd 12731	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139	138, 135	rpmulcld 12717	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140		0le1 11428	. . . . . . . . 9 ⊢ 0 ≤ 1
141	140	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
142	135	rpred 12701	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℝ)
143	135	rpge0d 12705	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (log‘2))
144	47	lep1d 11836	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
145	47, 48, 142, 143, 144	lemul1ad 11844	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146	133, 139, 38, 141, 145	lediv2ad 12723	. . . . . . 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 11844	. . . . . 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 11845	. . . . 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 11519	. . . 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 11718	. . . . . . . . . 10 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151	150	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152	151	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153	152	oveq1d 7270	. . . . . . 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 7271	. . . . . 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 13790	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℂ)
156	12, 91	expcld 13792	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
157	13, 155, 156, 2, 88, 11	divmuldivd 11722	. . . . . 6 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158	154, 157	oveq12d 7273	. . . . 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 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
160	50, 18, 105, 26	mulne0d 11557	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
161	53, 159, 51, 160, 46	divdiv2d 11713	. . . . . . . . . 10 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162	161	oveq1d 7270	. . . . . . . . 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 7271	. . . . . . . 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 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165	164, 159, 160	divcld 11681	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
166	82	recnd 10934	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
167	13, 165, 166	mulassd 10929	. . . . . . . . 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 2744	. . . . . . . 8 ⊢ (𝜑 → (2 · (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
169	163, 168	eqtrd 2778	. . . . . . 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 7270	. . . . . 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 11716	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172	171	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173	172	oveq1d 7270	. . . . . . . 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 7270	. . . . . . 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 10929	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176	175	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177	176	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178	177	oveq1d 7270	. . . . . . . . 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 7270	. . . . . . . 8 ⊢ (𝜑 → ((((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
180	13	mulid1d 10923	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 1) = 2)
181	180	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182	181	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183	182	oveq1d 7270	. . . . . . . . . 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 7270	. . . . . . . . 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 10926	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
186	79	recnd 10934	. . . . . . . . . . . 12 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
187	51, 2	mulcld 10926	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188	185, 159, 186, 187, 160, 81	divmuldivd 11722	. . . . . . . . . . 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 7270	. . . . . . . . . 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 10929	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191	190	oveq2d 7271	. . . . . . . . . . . 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 7270	. . . . . . . . . . 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 10927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
194	18, 51, 2	mulassd 10929	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195	194	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196	195	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197	193, 196	oveq12d 7273	. . . . . . . . . . . . 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 7270	. . . . . . . . . . . 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 10926	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200	199, 2	mulcld 10926	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
201	18, 51, 26, 46	mulne0d 11557	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202	199, 2, 201, 11	mulne0d 11557	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203	186, 50, 185, 200, 105, 202	divmuldivd 11722	. . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))) = (((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))))
205	204	oveq1d 7270	. . . . . . . . . . . . 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 10934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℂ)
207	78	recnd 10934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208	206, 207, 50, 105	divassd 11716	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209	194	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210	208, 209	oveq12d 7273	. . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . 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 12353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 4 ∈ ℤ)
213	12, 104, 45, 212	expsubd 13803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214	213	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215		4p1e5 12049	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 1) = 5
216	74	recni 10920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℂ
217	4	recni 10920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℂ
218		ax-1cn 10860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℂ
219	216, 217, 218	subaddi 11238	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((5 − 4) = 1 ↔ (4 + 1) = 5)
220	215, 219	mpbir 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (5 − 4) = 1
221	220	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 − 4) = 1)
222	53	subid1d 11251	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 − 0) = 1)
223	221, 222	eqtr4d 2781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 − 4) = (1 − 0))
224	206, 217	jctir 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225		0cnd 10899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ∈ ℂ)
226	53, 225	jca 511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227		subeqrev 11327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228	224, 226, 227	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229	223, 228	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (4 − 5) = (0 − 1))
230		df-neg 11138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 = (0 − 1)
231	229, 230	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (4 − 5) = -1)
232	231	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233	214, 232	eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234	233	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
235	13, 18, 51, 187, 26, 81	divmuldivd 11722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236	235	eqcomd 2744	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237	234, 236	oveq12d 7273	. . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . 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 12281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℤ)
240	12, 104, 239	expnegd 13799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241	240	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
242	51, 51, 2, 46, 11	divdiv1d 11712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243	242	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244	243	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245	241, 244	oveq12d 7273	. . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . 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 13798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248	206, 53, 156, 247	divassd 11716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249	248	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
250	51, 46	dividd 11679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251	250	oveq1d 7270	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252	251	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253	249, 252	oveq12d 7273	. . . . . . . . . . . . . . . . . 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 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
255	206	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (5 · 1) = 5)
256	255	oveq1d 7270	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
257	13, 18, 53, 2, 26, 11	divmuldivd 11722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258	256, 257	oveq12d 7273	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259	258	oveq1d 7270	. . . . . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · 1) ∈ ℂ)
261	18, 2	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
262	18, 2, 26, 11	mulne0d 11557	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263	206, 156, 260, 261, 247, 262	divmuldivd 11722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264	180	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · (2 · 1)) = (5 · 2))
265	264	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266	263, 265	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267	266	oveq1d 7270	. . . . . . . . . . . . . . . . . . 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 12466	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (5 · 2) = ;10
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · 2) = ;10)
270	269	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271	270	oveq1d 7270	. . . . . . . . . . . . . . . . . . . 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 12384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ;10 ∈ ℕ0
273	272	nn0cni 12175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ;10 ∈ ℂ
274	273	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ;10 ∈ ℂ)
275	274	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (;10 · 1) = ;10)
276	275	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 / (((log‘𝐴)↑1) · (log‘2))))
277	13, 156	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278	277, 155, 88	divcld 11681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279	278	mulid2d 10924	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280	276, 279	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 13792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
282	18, 26, 239	expne0d 13798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
283	277, 281, 282	divcld 11681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284	283	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285	284	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286		10re 12385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ;10 ∈ ℝ
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ;10 ∈ ℝ)
288	287, 40, 104	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ∈ ℝ)
289	40, 43, 26	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290	289, 91	reexpcld 13809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
291	37, 290	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292	288, 291	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293	287, 291	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
294	43, 112	reexpcld 13809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℝ)
295		3z 12283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 3 ∈ ℤ
296	295	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → 3 ∈ ℤ)
297	18, 26, 296	expne0d 13798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ≠ 0)
298	113, 294, 297	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
299	5, 298	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300		ere 15726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ e ∈ ℝ
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e ∈ ℝ)
302	112	nn0red 12224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 ∈ ℝ)
303		egt2lt3 15843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 < e ∧ e < 3)
304	303	simpri 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ e < 3
305	304	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → e < 3)
306		3lt4 12077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 3 < 4
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 3 < 4)
308	302, 5, 1, 307, 8	ltletrd 11065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 < 𝐴)
309	301, 302, 1, 305, 308	lttrd 11066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e < 𝐴)
310	301, 1, 309	ltled 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → e ≤ 𝐴)
311	301, 1	lenltd 11051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312	310, 311	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ¬ 𝐴 < e)
313		loglt1b 25694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
314	39, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315	312, 314	mtbird 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ¬ (log‘𝐴) < 1)
316	38, 40	lenltd 11051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317	315, 316	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 1 ≤ (log‘𝐴))
318		10nn 12382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ;10 ∈ ℕ
319	318	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ;10 ∈ ℕ)
320		nnledivrp 12771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((;10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
321	319, 130, 320	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
322	317, 321	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ≤ ;10)
323	288, 287, 291, 322	leadd1dd 11519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
324	38, 55	gtned 11040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≠ 1)
325	37, 15, 1, 9, 324	relogbcld 39908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ)
326	325, 91	reexpcld 13809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
327	42, 55	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328		logbgt0b 25848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
329	39, 327, 328	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
330	99, 329	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 0 < (2 logb 𝐴))
331	325, 330	elrpd 12698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332	331, 239	rpexpcld 13890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333	332	rpne0d 12706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334	287, 326, 333	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335	334, 37	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336		sq2 13842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (2↑2) = 4
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2↑2) = 4)
338	337, 5	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ∈ ℝ)
339	5, 338	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ∈ ℝ)
340	325	resqcld 13893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
341	5, 340	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342	325	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℂ)
343	342	exp1d 13787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344	343	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) = (;10 / (2 logb 𝐴)))
345	344	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 / (2 logb 𝐴)) + 2))
346	345, 335	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347	287	rehalfcld 12150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
348	347, 37	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ∈ ℝ)
349	344, 334	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ∈ ℝ)
350	287, 37, 17	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
351	272	nn0ge0i 12190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 0 ≤ ;10
352	351	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 0 ≤ ;10)
353	42, 324, 87	relogbexpd 39909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
354	353	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 = (2 logb (2↑2)))
355	337	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356	354, 355	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 2 = (2 logb 4))
357	37	leidd 11471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 ≤ 2)
358	87, 357, 5, 7, 1, 9, 8	logblebd 39911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359	356, 358	eqbrtrd 5092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≤ (2 logb 𝐴))
360	42, 331, 287, 352, 359	lediv2ad 12723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ≤ (;10 / 2))
361	349, 350, 37, 360	leadd1dd 11519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ ((;10 / 2) + 2))
362		1nn 11914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 1 ∈ ℕ
363		6nn0 12184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 6 ∈ ℕ0
364		2nn0 12180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 2 ∈ ℕ0
365	27, 364	nn0addcli 12200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ∈ ℕ0
366		5p2e7 12059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (5 + 2) = 7
367		7re 11996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 7 ∈ ℝ
368	367, 364	nn0addge1i 12211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ 7 ≤ (7 + 2)
369		7p2e9 12064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (7 + 2) = 9
370	368, 369	breqtri 5095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 7 ≤ 9
371	366, 370	eqbrtri 5091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ≤ 9
372	362, 363, 365, 371	declei 12402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (5 + 2) ≤ ;16
373	372	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) ≤ ;16)
374	206, 13, 274, 17	ldiv 11739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((5 · 2) = ;10 ↔ 5 = (;10 / 2)))
375	269, 374	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 5 = (;10 / 2))
376	375	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) = ((;10 / 2) + 2))
377		4t4e16 12465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (4 · 4) = ;16
378	377	eqcomi 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ;16 = (4 · 4)
379	378	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → ;16 = (4 · 4))
380	337	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 4 = (2↑2))
381	380	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (4 · 4) = (4 · (2↑2)))
382	379, 381	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ;16 = (4 · (2↑2)))
383	373, 376, 382	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ≤ (4 · (2↑2)))
384	346, 348, 339, 361, 383	letrd 11062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385	345, 384	eqbrtrd 5092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
386	3, 5, 7	ltled 11053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → 0 ≤ 4)
387	364	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ ℕ0)
388	37, 325, 387, 124, 359	leexp1ad 39907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389	338, 340, 5, 386, 388	lemul2ad 11845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390	335, 339, 341, 385, 389	letrd 11062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
391	37, 326	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392	391	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393	326	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394	274, 392, 393, 333	divdird 11719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396	395	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398	397	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399	398, 180	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400	399	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
401	396, 400	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
402	394, 401	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
403	402	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404		2p1e3 12045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 + 1) = 3
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 + 1) = 3)
406	302	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 3 ∈ ℂ)
407	406, 53, 13	subadd2d 11281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408	405, 407	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (3 − 1) = 2)
409	408	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 2 = (3 − 1))
410	409	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411	410	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
412	3, 330	gtned 11040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ≠ 0)
413	342, 412, 239, 296	expsubd 13803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414	413	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415	411, 414	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 4 ∈ ℂ)
417	325, 112	reexpcld 13809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418	417	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419	416, 418, 393, 333	divassd 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420	419	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421	415, 420	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422	390, 403, 421	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423	287, 391	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
424	5, 417	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425	423, 424, 332	lediv1d 12747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)) ↔ ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1))))
426	422, 425	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
427	87	uzidd 12527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ (ℤ≥‘2))
428	427, 39	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+))
429		relogbval 25827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431	430	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432	431	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433	432	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) = (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434	430	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
435	12, 18, 26, 112	expdivd 13806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436	434, 435	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437	436	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438	426, 433, 437	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439	292, 293, 299, 323, 438	letrd 11062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
440	12	exp1d 13787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441	440	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442	441	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 / (log‘𝐴)) = (;10 / ((log‘𝐴)↑1)))
443	13, 156, 281, 282	divassd 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
444	12, 18, 26, 91	expdivd 13806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445	444	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446	445	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447	443, 446	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448	447	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449	442, 448	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450	113	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
451	18, 112	expcld 13792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℂ)
452	416, 450, 451, 297	divassd 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453	452	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454	439, 449, 453	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455	285, 454	eqbrtrd 5092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456	281, 282	dividd 11679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457	456	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458	457	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461	460	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463	462, 451, 297	divcld 11681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464	463	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465	464	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466	455, 461, 465	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) ∈ ℂ)
468	467	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = (;10 / ((log‘𝐴)↑1)))
469	468	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · 1))
470	18, 26	dividd 11679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2) / (log‘2)) = 1)
471	470	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = ((log‘2) / (log‘2)))
472	471	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473	469, 472	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474	274, 156, 18, 18, 247, 26	divmuldivd 11722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475	473, 474	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
476	18	exp1d 13787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑1) = (log‘2))
477	476	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478		df-2 11966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 2 = (1 + 1)
479	478	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 2 = (1 + 1))
480	479	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
481	18, 91, 91	expaddd 13794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482	480, 481	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483	482	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484	477, 483	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (log‘2) = ((log‘2)↑1))
487	486	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488	471, 487	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489	488	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490	476, 18	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
491	476, 26	eqnetrd 3010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
492	462, 451, 18, 490, 297, 491	divmuldivd 11722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494	466, 485, 493	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496	156, 18, 247, 26	mulne0d 11557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497	274, 18, 495, 496	div23d 11718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498	277, 18, 155, 88	div23d 11718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499	497, 498	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
502	18, 91, 112	expaddd 13794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503	501, 502	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504	503	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505	504	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508	287, 507, 496	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509	508	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510	509, 278, 18	adddird 10931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))) = (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)))
512	18, 26, 212	expne0d 13798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
513	462, 18, 117, 512	div23d 11718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514	506, 511, 513	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516	515, 85, 88	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517	508, 516	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518	114, 115, 120	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519	517, 518, 135	lemul1d 12744	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ↔ (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2))))
520	514, 519	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)))
521	280, 520	eqbrtrd 5092	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
523	53, 277, 155, 88	div12d 11717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524	522, 523	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))))
525	462	mulid1d 10923	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526	525	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527	526	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528	521, 524, 527	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . . 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 11679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
530	529	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 1 = (𝐴 / 𝐴))
531	530	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
532	2, 2, 495, 11, 496	divdiv1d 11712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533	531, 532	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534	533	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536	530	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537	536	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538	535, 537	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539	534, 538	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . . 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 11716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541	528, 539, 540	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
542	2, 495	mulcomd 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543	156, 18, 2	mulassd 10929	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544	542, 543	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545	544	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546	545	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
547	2, 2, 155, 11, 88	divdiv1d 11712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
548	2, 155	mulcomd 10927	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549	548	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550	547, 549	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551	550	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552	546, 551	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) = ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))))
553		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554	530	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555	553, 554	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556	555	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557	541, 552, 556	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558	156, 261	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559	156, 261, 247, 262	mulne0d 11557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560	274, 558, 2, 559	div32d 11704	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561	560	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562	155, 2	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563	155, 2, 88, 11	mulne0d 11557	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564	277, 562, 2, 563	div32d 11704	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565	564	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566	561, 565	oveq12d 7273	. . . . . . . . . . . . . . . . . . . . . . 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 11712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
568	2, 117	mulcomd 10927	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569	568	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570	567, 569	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571	570	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572	557, 566, 571	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
573	43, 1	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
574	92, 573	remulcld 10936	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575	287, 574, 559	redivcld 11733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576	575	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577	157, 94	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578	577	recnd 10934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579	576, 578, 2	adddird 10931	. . . . . . . . . . . . . . . . . . . . . . 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 2744	. . . . . . . . . . . . . . . . . . . . . 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 13792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582	416, 581	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583	117, 2	mulcld 10926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584	117, 2, 512, 11	mulne0d 11557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585	582, 583, 2, 584	div32d 11704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586	585	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587	572, 580, 586	3brtr3d 5101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588	575, 577	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589	588, 122, 39	lemul1d 12744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ↔ (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴)))
590	587, 589	mpbird 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
591	271, 590	eqbrtrd 5092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592	267, 591	eqbrtrd 5092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593	259, 592	eqbrtrd 5092	. . . . . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . 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 5092	. . . . . . . . . . . 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 5092	. . . . . . . . . . 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 5092	. . . . . . . . . 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 5092	. . . . . . . . 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 5092	. . . . . . . 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 5092	. . . . . . 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 5092	. . . . . 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 5092	. . . . 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 5092	. . . 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 11062	. . 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 5092	. 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 583	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610	609	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611	610	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612	611	oveq1d 7270	. . . . . . 7 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613	612	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614	613	oveq2d 7271	. . . . 5 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615		5cn 11991	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
616	615	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℂ)
617	616, 207	mulcld 10926	. . . . . . . . . . . . 13 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618	617	mulid1d 10923	. . . . . . . . . . . 12 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619	618	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621		df-5 11969	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 = (4 + 1)
622	621	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 5 = (4 + 1))
623	622	oveq2d 7271	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
624	18, 91, 77	expaddd 13794	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625	623, 624	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626	476	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627	625, 626	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628	627	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629	620, 628	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630	117, 18, 2	mulassd 10929	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631	629, 630	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
632	18, 2	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633	632	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634	631, 633	eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635	619, 634	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
636	2, 18	mulcld 10926	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
637	2, 18, 11, 26	mulne0d 11557	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638	186, 117, 53, 636, 120, 637	divmuldivd 11722	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639	638	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640	635, 639	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641	206, 207, 117, 120	divassd 11716	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642	641	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643	640, 642	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
644	12, 18, 26, 77	expdivd 13806	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645	644	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646	645	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647	646	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648	643, 647	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649	610	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650	649	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651	650	oveq1d 7270	. . . . . . 7 ⊢ (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652	648, 651	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653	342, 77	expcld 13792	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654	616, 653	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
655	39	rpne0d 12706	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
656	2, 18, 655, 26	mulne0d 11557	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657	636, 656	reccld 11674	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658	654, 657	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659	658	addid1d 11105	. . . . . . 7 ⊢ (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660	659	eqcomd 2744	. . . . . 6 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661	652, 660	eqtrd 2778	. . . . 5 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662	614, 661	oveq12d 7273	. . . 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 7271	. . 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 12030	. . . . . . 7 ⊢ 1 = (2 − 1)
665	664	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 = (2 − 1))
666	665	oveq2d 7271	. . . . 5 ⊢ (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667	666	oveq1d 7270	. . . 4 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668	667	oveq2d 7271	. . 3 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669	663, 668	oveq12d 7273	. 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 11988	. . . . 5 ⊢ 4 ∈ ℂ
671	670	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
672	671, 117, 581, 2, 120, 655	divmuldivd 11722	. . 3 ⊢ (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673	672	eqcomd 2744	. 2 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674	608, 669, 673	3brtr3d 5101	1 ⊢ (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108   class class class wbr 5070  ‘cfv 6418  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940   ≤ cle 10941   − cmin 11135  -cneg 11136   / cdiv 11562  ℕcn 11903  2c2 11958  3c3 11959  4c4 11960  5c5 11961  6c6 11962  7c7 11963  9c9 11965  ℕ₀cn0 12163  ℤcz 12249  ;cdc 12366  ℤ_≥cuz 12511  ℝ⁺crp 12659  ↑cexp 13710  eceu 15700  logclog 25615   log_b clogb 25819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880  ax-addf 10881  ax-mulf 10882

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-om 7688  df-1st 7804  df-2nd 7805  df-supp 7949  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-er 8456  df-map 8575  df-pm 8576  df-ixp 8644  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fsupp 9059  df-fi 9100  df-sup 9131  df-inf 9132  df-oi 9199  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973  df-n0 12164  df-z 12250  df-dec 12367  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ioo 13012  df-ioc 13013  df-ico 13014  df-icc 13015  df-fz 13169  df-fzo 13312  df-fl 13440  df-mod 13518  df-seq 13650  df-exp 13711  df-fac 13916  df-bc 13945  df-hash 13973  df-shft 14706  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-limsup 15108  df-clim 15125  df-rlim 15126  df-sum 15326  df-ef 15705  df-e 15706  df-sin 15707  df-cos 15708  df-pi 15710  df-struct 16776  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868  df-plusg 16901  df-mulr 16902  df-starv 16903  df-sca 16904  df-vsca 16905  df-ip 16906  df-tset 16907  df-ple 16908  df-ds 16910  df-unif 16911  df-hom 16912  df-cco 16913  df-rest 17050  df-topn 17051  df-0g 17069  df-gsum 17070  df-topgen 17071  df-pt 17072  df-prds 17075  df-xrs 17130  df-qtop 17135  df-imas 17136  df-xps 17138  df-mre 17212  df-mrc 17213  df-acs 17215  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-submnd 18346  df-mulg 18616  df-cntz 18838  df-cmn 19303  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-fbas 20507  df-fg 20508  df-cnfld 20511  df-top 21951  df-topon 21968  df-topsp 21990  df-bases 22004  df-cld 22078  df-ntr 22079  df-cls 22080  df-nei 22157  df-lp 22195  df-perf 22196  df-cn 22286  df-cnp 22287  df-haus 22374  df-tx 22621  df-hmeo 22814  df-fil 22905  df-fm 22997  df-flim 22998  df-flf 22999  df-xms 23381  df-ms 23382  df-tms 23383  df-cncf 23947  df-limc 24935  df-dv 24936  df-log 25617  df-cxp 25618  df-logb 25820

This theorem is referenced by:  aks4d1p1p5  40011