Theorem aks4d1p1p7 40089

Description: Bound of intermediary of inequality step. (Contributed by metakunt, 19-Aug-2024.)

Hypotheses

Ref	Expression
aks4d1p1p7.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
aks4d1p1p7.2	⊢ (𝜑 → 4 ≤ 𝐴)

Assertion

Ref	Expression
aks4d1p1p7	⊢ (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))

Proof of Theorem aks4d1p1p7

Step	Hyp	Ref	Expression
1		aks4d1p1p7.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2	1	recnd 11012	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		0red 10987	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
4		4re 12066	. . . . . . . . . . . . . . 15 ⊢ 4 ∈ ℝ
5	4	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ∈ ℝ)
6		4pos 12089	. . . . . . . . . . . . . . 15 ⊢ 0 < 4
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 4)
8		aks4d1p1p7.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 4 ≤ 𝐴)
9	3, 5, 1, 7, 8	ltletrd 11144	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝐴)
10	3, 9	ltned 11120	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 𝐴)
11	10	necomd 3000	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
12	2, 11	logcld 25735	. . . . . . . . . 10 ⊢ (𝜑 → (log‘𝐴) ∈ ℂ)
13		2cnd 12060	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
14		2pos 12085	. . . . . . . . . . . . . 14 ⊢ 0 < 2
15	14	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 2)
16	3, 15	ltned 11120	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ 2)
17	16	necomd 3000	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≠ 0)
18	13, 17	logcld 25735	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ∈ ℂ)
19		1lt2 12153	. . . . . . . . . . . . . 14 ⊢ 1 < 2
20		2rp 12744	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
21		loggt0b 25796	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℝ+ → (0 < (log‘2) ↔ 1 < 2))
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 11120	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≠ (log‘2))
26	25	necomd 3000	. . . . . . . . . 10 ⊢ (𝜑 → (log‘2) ≠ 0)
27		5nn0 12262	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ0
28	27	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 5 ∈ ℕ0)
29	12, 18, 26, 28	expdivd 13887	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = (((log‘𝐴)↑5) / ((log‘2)↑5)))
30	29	oveq1d 7299	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
31	30	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
32	31	oveq2d 7300	. . . . . 6 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))))
33	32	oveq1d 7299	. . . . 5 ⊢ (𝜑 → ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
34	33	oveq2d 7300	. . . 4 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))))
35	34	oveq1d 7299	. . 3 ⊢ (𝜑 → ((2 · ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))))
36		2re 12056	. . . . . . 7 ⊢ 2 ∈ ℝ
37	36	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
38		1red 10985	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
39	1, 9	elrpd 12778	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
40	39	relogcld 25787	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ)
41	40, 28	reexpcld 13890	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ)
42	20	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℝ+)
43	42	relogcld 25787	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ)
44	43, 28	reexpcld 13890	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ)
45	28	nn0zd 12433	. . . . . . . . . . . 12 ⊢ (𝜑 → 5 ∈ ℤ)
46	18, 26, 45	expne0d 13879	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ≠ 0)
47	41, 44, 46	redivcld 11812	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ)
48	47, 38	readdcld 11013	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ)
49	48, 43	remulcld 11014	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ)
50	12, 28	expcld 13873	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℂ)
51	18, 28	expcld 13873	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℂ)
52	50, 51, 46	divcld 11760	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℂ)
53		1cnd 10979	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℂ)
54	52, 53	addcld 11003	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℂ)
55	19	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 2)
56	37, 55	rplogcld 25793	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
57	56, 45	rpexpcld 13971	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
58		1re 10984	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
59		3nn0 12260	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ0
60	58, 59	nn0addge2i 12291	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ≤ (3 + 1)
61	60	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ (3 + 1))
62		df-4 12047	. . . . . . . . . . . . . . . . 17 ⊢ 4 = (3 + 1)
63	61, 62	breqtrrdi 5117	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ≤ 4)
64	38, 5, 1, 63, 8	letrd 11141	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ≤ 𝐴)
65	1, 64	logge0d 25794	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (log‘𝐴))
66	40, 28, 65	expge0d 13891	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑5))
67	41, 57, 66	divge0d 12821	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
68	47	ltp1d 11914	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
69	3, 47, 48, 67, 68	lelttrd 11142	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
70	3, 69	ltned 11120	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≠ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
71	70	necomd 3000	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ≠ 0)
72	54, 18, 71, 26	mulne0d 11636	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ≠ 0)
73	38, 49, 72	redivcld 11812	. . . . . . 7 ⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) ∈ ℝ)
74		5re 12069	. . . . . . . . . 10 ⊢ 5 ∈ ℝ
75	74	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 5 ∈ ℝ)
76		4nn0 12261	. . . . . . . . . . 11 ⊢ 4 ∈ ℕ0
77	76	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ∈ ℕ0)
78	40, 77	reexpcld 13890	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℝ)
79	75, 78	remulcld 11014	. . . . . . . 8 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℝ)
80	44, 1	remulcld 11014	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ)
81	51, 2, 46, 11	mulne0d 11636	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ≠ 0)
82	79, 80, 81	redivcld 11812	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℝ)
83	73, 82	remulcld 11014	. . . . . 6 ⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
84	37, 83	remulcld 11014	. . . . 5 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
85	43	resqcld 13974	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℝ)
86		2z 12361	. . . . . . . . 9 ⊢ 2 ∈ ℤ
87	86	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℤ)
88	18, 26, 87	expne0d 13879	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ≠ 0)
89	37, 85, 88	redivcld 11812	. . . . . 6 ⊢ (𝜑 → (2 / ((log‘2)↑2)) ∈ ℝ)
90		1nn0 12258	. . . . . . . . 9 ⊢ 1 ∈ ℕ0
91	90	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℕ0)
92	40, 91	reexpcld 13890	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℝ)
93	92, 1, 11	redivcld 11812	. . . . . 6 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ)
94	89, 93	remulcld 11014	. . . . 5 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ)
95	84, 94	readdcld 11013	. . . 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 11014	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ)
97		1lt4 12158	. . . . . . . . . . . . . . . 16 ⊢ 1 < 4
98	97	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 < 4)
99	38, 5, 1, 98, 8	ltletrd 11144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 < 𝐴)
100		loggt0b 25796	. . . . . . . . . . . . . . 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 11120	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≠ (log‘𝐴))
104	103	necomd 3000	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ≠ 0)
105	12, 104, 45	expne0d 13879	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ≠ 0)
106	50, 51, 105, 46	divne0d 11776	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≠ 0)
107	52, 18, 106, 26	mulne0d 11636	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≠ 0)
108	38, 96, 107	redivcld 11812	. . . . . . 7 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) ∈ ℝ)
109	108, 82	remulcld 11014	. . . . . 6 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ∈ ℝ)
110	37, 109	remulcld 11014	. . . . 5 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ∈ ℝ)
111	110, 94	readdcld 11013	. . . 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 13890	. . . . . 6 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℝ)
114	5, 113	remulcld 11014	. . . . 5 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℝ)
115	43, 77	reexpcld 13890	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℝ)
116	115, 1	remulcld 11014	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℝ)
117	18, 77	expcld 13873	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ∈ ℂ)
118		4z 12363	. . . . . . . 8 ⊢ 4 ∈ ℤ
119	118	a1i 11	. . . . . . 7 ⊢ (𝜑 → 4 ∈ ℤ)
120	18, 26, 119	expne0d 13879	. . . . . 6 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
121	117, 2, 120, 11	mulne0d 11636	. . . . 5 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
122	114, 116, 121	redivcld 11812	. . . 4 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ∈ ℝ)
123		0le2 12084	. . . . . . 7 ⊢ 0 ≤ 2
124	123	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ≤ 2)
125	57, 39	rpmulcld 12797	. . . . . . . 8 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℝ+)
126	28	nn0ge0d 12305	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 5)
127	40, 77, 65	expge0d 13891	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑4))
128	75, 78, 126, 127	mulge0d 11561	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (5 · ((log‘𝐴)↑4)))
129	79, 125, 128	divge0d 12821	. . . . . . 7 ⊢ (𝜑 → 0 ≤ ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))
130	1, 99	rplogcld 25793	. . . . . . . . . . 11 ⊢ (𝜑 → (log‘𝐴) ∈ ℝ+)
131	130, 45	rpexpcld 13971	. . . . . . . . . 10 ⊢ (𝜑 → ((log‘𝐴)↑5) ∈ ℝ+)
132	131, 57	rpdivcld 12798	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ∈ ℝ+)
133	132, 56	rpmulcld 12797	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ∈ ℝ+)
134	24, 22	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → 1 < 2)
135	37, 134	rplogcld 25793	. . . . . . . . . . . 12 ⊢ (𝜑 → (log‘2) ∈ ℝ+)
136	135, 45	rpexpcld 13971	. . . . . . . . . . 11 ⊢ (𝜑 → ((log‘2)↑5) ∈ ℝ+)
137	41, 136, 66	divge0d 12821	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) / ((log‘2)↑5)))
138	47, 137	ge0p1rpd 12811	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) ∈ ℝ+)
139	138, 135	rpmulcld 12797	. . . . . . . 8 ⊢ (𝜑 → (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)) ∈ ℝ+)
140		0le1 11507	. . . . . . . . 9 ⊢ 0 ≤ 1
141	140	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
142	135	rpred 12781	. . . . . . . . 9 ⊢ (𝜑 → (log‘2) ∈ ℝ)
143	135	rpge0d 12785	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (log‘2))
144	47	lep1d 11915	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴)↑5) / ((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1))
145	47, 48, 142, 143, 144	lemul1ad 11923	. . . . . . . 8 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2)))
146	133, 139, 38, 141, 145	lediv2ad 12803	. . . . . . 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 11923	. . . . . 6 ⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) ≤ ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
148	83, 109, 37, 124, 147	lemul2ad 11924	. . . . 5 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) ≤ (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))))
149	84, 110, 94, 148	leadd1dd 11598	. . . 4 ⊢ (𝜑 → ((2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ≤ ((2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))))
150	50, 18, 51, 46	div23d 11797	. . . . . . . . . 10 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)))
151	150	eqcomd 2745	. . . . . . . . 9 ⊢ (𝜑 → ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5)))
152	151	oveq2d 7300	. . . . . . . 8 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))))
153	152	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
154	153	oveq2d 7300	. . . . . 6 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = (2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))))
155	18	sqcld 13871	. . . . . . 7 ⊢ (𝜑 → ((log‘2)↑2) ∈ ℂ)
156	12, 91	expcld 13873	. . . . . . 7 ⊢ (𝜑 → ((log‘𝐴)↑1) ∈ ℂ)
157	13, 155, 156, 2, 88, 11	divmuldivd 11801	. . . . . 6 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)))
158	154, 157	oveq12d 7302	. . . . 5 ⊢ (𝜑 → ((2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
159	50, 18	mulcld 11004	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ∈ ℂ)
160	50, 18, 105, 26	mulne0d 11636	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴)↑5) · (log‘2)) ≠ 0)
161	53, 159, 51, 160, 46	divdiv2d 11792	. . . . . . . . . 10 ⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) = ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
162	161	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
163	162	oveq2d 7300	. . . . . . . 8 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = (2 · (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))))
164	53, 51	mulcld 11004	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · ((log‘2)↑5)) ∈ ℂ)
165	164, 159, 160	divcld 11760	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈ ℂ)
166	82	recnd 11012	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) ∈ ℂ)
167	13, 165, 166	mulassd 11007	. . . . . . . . 9 ⊢ (𝜑 → ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = (2 · (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))))
168	167	eqcomd 2745	. . . . . . . 8 ⊢ (𝜑 → (2 · (((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
169	163, 168	eqtrd 2779	. . . . . . 7 ⊢ (𝜑 → (2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
170	169	oveq1d 7299	. . . . . 6 ⊢ (𝜑 → ((2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
171	13, 164, 159, 160	divassd 11795	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))))
172	171	eqcomd 2745	. . . . . . . . 9 ⊢ (𝜑 → (2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))))
173	172	oveq1d 7299	. . . . . . . 8 ⊢ (𝜑 → ((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = (((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
174	173	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → (((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
175	13, 53, 51	mulassd 11007	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · (1 · ((log‘2)↑5))))
176	175	eqcomd 2745	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · (1 · ((log‘2)↑5))) = ((2 · 1) · ((log‘2)↑5)))
177	176	oveq1d 7299	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
178	177	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → (((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = ((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
179	178	oveq1d 7299	. . . . . . . 8 ⊢ (𝜑 → ((((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
180	13	mulid1d 11001	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 1) = 2)
181	180	oveq1d 7299	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 1) · ((log‘2)↑5)) = (2 · ((log‘2)↑5)))
182	181	oveq1d 7299	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))))
183	182	oveq1d 7299	. . . . . . . . . 10 ⊢ (𝜑 → ((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = (((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))))
184	183	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → (((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
185	13, 51	mulcld 11004	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · ((log‘2)↑5)) ∈ ℂ)
186	79	recnd 11012	. . . . . . . . . . . 12 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
187	51, 2	mulcld 11004	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) ∈ ℂ)
188	185, 159, 186, 187, 160, 81	divmuldivd 11801	. . . . . . . . . . 11 ⊢ (𝜑 → (((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = (((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴))))
189	188	oveq1d 7299	. . . . . . . . . 10 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
190	50, 18, 187	mulassd 11007	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))))
191	190	oveq2d 7300	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴))) = (((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴)))))
192	191	oveq1d 7299	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
193	185, 186	mulcomd 11005	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))))
194	18, 51, 2	mulassd 11007	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) = ((log‘2) · (((log‘2)↑5) · 𝐴)))
195	194	eqcomd 2745	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2) · (((log‘2)↑5) · 𝐴)) = (((log‘2) · ((log‘2)↑5)) · 𝐴))
196	195	oveq2d 7300	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴)))
197	193, 196	oveq12d 7302	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴)))) = (((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))))
198	197	oveq1d 7299	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
199	18, 51	mulcld 11004	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ∈ ℂ)
200	199, 2	mulcld 11004	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ∈ ℂ)
201	18, 51, 26, 46	mulne0d 11636	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2) · ((log‘2)↑5)) ≠ 0)
202	199, 2, 201, 11	mulne0d 11636	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2) · ((log‘2)↑5)) · 𝐴) ≠ 0)
203	186, 50, 185, 200, 105, 202	divmuldivd 11801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))) = (((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))))
204	203	eqcomd 2745	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))) = (((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))))
205	204	oveq1d 7299	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
206	75	recnd 11012	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 5 ∈ ℂ)
207	78	recnd 11012	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘𝐴)↑4) ∈ ℂ)
208	206, 207, 50, 105	divassd 11795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) = (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))))
209	194	oveq2d 7300	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴)) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
210	208, 209	oveq12d 7302	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))) = ((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴)))))
211	210	oveq1d 7299	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
212	77	nn0zd 12433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 4 ∈ ℤ)
213	12, 104, 45, 212	expsubd 13884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))
214	213	eqcomd 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 − 5)))
215		4p1e5 12128	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 + 1) = 5
216	74	recni 10998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℂ
217	4	recni 10998	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℂ
218		ax-1cn 10938	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 1 ∈ ℂ
219	216, 217, 218	subaddi 11317	. . . . . . . . . . . . . . . . . . . . . . . . 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 11330	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 − 0) = 1)
223	221, 222	eqtr4d 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 − 4) = (1 − 0))
224	206, 217	jctir 521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (5 ∈ ℂ ∧ 4 ∈ ℂ))
225		0cnd 10977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 ∈ ℂ)
226	53, 225	jca 512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 ∈ ℂ ∧ 0 ∈ ℂ))
227		subeqrev 11406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((5 ∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈ ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
228	224, 226, 227	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0 − 1)))
229	223, 228	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (4 − 5) = (0 − 1))
230		df-neg 11217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -1 = (0 − 1)
231	229, 230	eqtr4di 2797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (4 − 5) = -1)
232	231	oveq2d 7300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) = ((log‘𝐴)↑-1))
233	214, 232	eqtrd 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1))
234	233	oveq2d 7300	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) = (5 · ((log‘𝐴)↑-1)))
235	13, 18, 51, 187, 26, 81	divmuldivd 11801	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))))
236	235	eqcomd 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))))
237	234, 236	oveq12d 7302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴)))) = ((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))))
238	237	oveq1d 7299	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
239		1zzd 12360	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 1 ∈ ℤ)
240	12, 104, 239	expnegd 13880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((log‘𝐴)↑-1) = (1 / ((log‘𝐴)↑1)))
241	240	oveq2d 7300	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (5 · ((log‘𝐴)↑-1)) = (5 · (1 / ((log‘𝐴)↑1))))
242	51, 51, 2, 46, 11	divdiv1d 11791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))
243	242	eqcomd 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))
244	243	oveq2d 7300	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)))
245	241, 244	oveq12d 7302	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))) = ((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))))
246	245	oveq1d 7299	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
247	12, 104, 239	expne0d 13879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((log‘𝐴)↑1) ≠ 0)
248	206, 53, 156, 247	divassd 11795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 · (1 / ((log‘𝐴)↑1))))
249	248	eqcomd 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (5 · (1 / ((log‘𝐴)↑1))) = ((5 · 1) / ((log‘𝐴)↑1)))
250	51, 46	dividd 11758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((log‘2)↑5) / ((log‘2)↑5)) = 1)
251	250	oveq1d 7299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴) = (1 / 𝐴))
252	251	oveq2d 7300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 / 𝐴)))
253	249, 252	oveq12d 7302	. . . . . . . . . . . . . . . . . 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 7299	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
255	206	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (5 · 1) = 5)
256	255	oveq1d 7299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 · 1) / ((log‘𝐴)↑1)) = (5 / ((log‘𝐴)↑1)))
257	13, 18, 53, 2, 26, 11	divmuldivd 11801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 / (log‘2)) · (1 / 𝐴)) = ((2 · 1) / ((log‘2) · 𝐴)))
258	256, 257	oveq12d 7302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))))
259	258	oveq1d 7299	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
260	180, 13	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · 1) ∈ ℂ)
261	18, 2	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℂ)
262	18, 2, 26, 11	mulne0d 11636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((log‘2) · 𝐴) ≠ 0)
263	206, 156, 260, 261, 247, 262	divmuldivd 11801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
264	180	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · (2 · 1)) = (5 · 2))
265	264	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · (2 · 1)) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
266	263, 265	eqtrd 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
267	266	oveq1d 7299	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
268		5t2e10 12546	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (5 · 2) = ;10
269	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (5 · 2) = ;10)
270	269	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) = (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
271	270	oveq1d 7299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))))
272		10nn0 12464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ;10 ∈ ℕ0
273	272	nn0cni 12254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ;10 ∈ ℂ
274	273	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ;10 ∈ ℂ)
275	274	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (;10 · 1) = ;10)
276	275	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 / (((log‘𝐴)↑1) · (log‘2))))
277	13, 156	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℂ)
278	277, 155, 88	divcld 11760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℂ)
279	278	mulid2d 11002	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
280	276, 279	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))))
281	18, 91	expcld 13873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
282	18, 26, 239	expne0d 13879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
283	277, 281, 282	divcld 11760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) ∈ ℂ)
284	283	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
285	284	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
286		10re 12465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ;10 ∈ ℝ
287	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ;10 ∈ ℝ)
288	287, 40, 104	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ∈ ℝ)
289	40, 43, 26	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) ∈ ℝ)
290	289, 91	reexpcld 13890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) ∈ ℝ)
291	37, 290	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) ∈ ℝ)
292	288, 291	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
293	287, 291	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈ ℝ)
294	43, 112	reexpcld 13890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℝ)
295		3z 12362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 3 ∈ ℤ
296	295	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → 3 ∈ ℤ)
297	18, 26, 296	expne0d 13879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘2)↑3) ≠ 0)
298	113, 294, 297	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘𝐴)↑3) / ((log‘2)↑3)) ∈ ℝ)
299	5, 298	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) ∈ ℝ)
300		ere 15807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ e ∈ ℝ
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e ∈ ℝ)
302	112	nn0red 12303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 ∈ ℝ)
303		egt2lt3 15924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (2 < e ∧ e < 3)
304	303	simpri 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ e < 3
305	304	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → e < 3)
306		3lt4 12156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 3 < 4
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 3 < 4)
308	302, 5, 1, 307, 8	ltletrd 11144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 3 < 𝐴)
309	301, 302, 1, 305, 308	lttrd 11145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → e < 𝐴)
310	301, 1, 309	ltled 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → e ≤ 𝐴)
311	301, 1	lenltd 11130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e))
312	310, 311	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ¬ 𝐴 < e)
313		loglt1b 25798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
314	39, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e))
315	312, 314	mtbird 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ¬ (log‘𝐴) < 1)
316	38, 40	lenltd 11130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1))
317	315, 316	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → 1 ≤ (log‘𝐴))
318		10nn 12462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ;10 ∈ ℕ
319	318	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ;10 ∈ ℕ)
320		nnledivrp 12851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((;10 ∈ ℕ ∧ (log‘𝐴) ∈ ℝ+) → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
321	319, 130, 320	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10))
322	317, 321	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / (log‘𝐴)) ≤ ;10)
323	288, 287, 291, 322	leadd1dd 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
324	38, 55	gtned 11119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≠ 1)
325	37, 15, 1, 9, 324	relogbcld 39988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ)
326	325, 91	reexpcld 13890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ)
327	42, 55	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 ∈ ℝ+ ∧ 1 < 2))
328		logbgt0b 25952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝐴 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
329	39, 327, 328	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (0 < (2 logb 𝐴) ↔ 1 < 𝐴))
330	99, 329	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 0 < (2 logb 𝐴))
331	325, 330	elrpd 12778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℝ+)
332	331, 239	rpexpcld 13971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℝ+)
333	332	rpne0d 12786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ≠ 0)
334	287, 326, 333	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) ∈ ℝ)
335	334, 37	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ∈ ℝ)
336		sq2 13923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (2↑2) = 4
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2↑2) = 4)
338	337, 5	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ∈ ℝ)
339	5, 338	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ∈ ℝ)
340	325	resqcld 13974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((2 logb 𝐴)↑2) ∈ ℝ)
341	5, 340	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) ∈ ℝ)
342	325	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 logb 𝐴) ∈ ℂ)
343	342	exp1d 13868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (2 logb 𝐴))
344	343	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) = (;10 / (2 logb 𝐴)))
345	344	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 / (2 logb 𝐴)) + 2))
346	345, 335	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ∈ ℝ)
347	287	rehalfcld 12229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
348	347, 37	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ∈ ℝ)
349	344, 334	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ∈ ℝ)
350	287, 37, 17	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / 2) ∈ ℝ)
351	272	nn0ge0i 12269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 0 ≤ ;10
352	351	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 0 ≤ ;10)
353	42, 324, 87	relogbexpd 39989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝜑 → (2 logb (2↑2)) = 2)
354	353	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 = (2 logb (2↑2)))
355	337	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → (2 logb (2↑2)) = (2 logb 4))
356	354, 355	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 2 = (2 logb 4))
357	37	leidd 11550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 2 ≤ 2)
358	87, 357, 5, 7, 1, 9, 8	logblebd 39991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 logb 4) ≤ (2 logb 𝐴))
359	356, 358	eqbrtrd 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 2 ≤ (2 logb 𝐴))
360	42, 331, 287, 352, 359	lediv2ad 12803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (;10 / (2 logb 𝐴)) ≤ (;10 / 2))
361	349, 350, 37, 360	leadd1dd 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ ((;10 / 2) + 2))
362		1nn 11993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 1 ∈ ℕ
363		6nn0 12263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ 6 ∈ ℕ0
364		2nn0 12259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 2 ∈ ℕ0
365	27, 364	nn0addcli 12279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ∈ ℕ0
366		5p2e7 12138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (5 + 2) = 7
367		7re 12075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 7 ∈ ℝ
368	367, 364	nn0addge1i 12290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ 7 ≤ (7 + 2)
369		7p2e9 12143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (7 + 2) = 9
370	368, 369	breqtri 5100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 7 ≤ 9
371	366, 370	eqbrtri 5096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (5 + 2) ≤ 9
372	362, 363, 365, 371	declei 12482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (5 + 2) ≤ ;16
373	372	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) ≤ ;16)
374	206, 13, 274, 17	ldiv 11818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((5 · 2) = ;10 ↔ 5 = (;10 / 2)))
375	269, 374	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → 5 = (;10 / 2))
376	375	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (5 + 2) = ((;10 / 2) + 2))
377		4t4e16 12545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (4 · 4) = ;16
378	377	eqcomi 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ;16 = (4 · 4)
379	378	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → ;16 = (4 · 4))
380	337	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → 4 = (2↑2))
381	380	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (4 · 4) = (4 · (2↑2)))
382	379, 381	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ;16 = (4 · (2↑2)))
383	373, 376, 382	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / 2) + 2) ≤ (4 · (2↑2)))
384	346, 348, 339, 361, 383	letrd 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ (4 · (2↑2)))
385	345, 384	eqbrtrd 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · (2↑2)))
386	3, 5, 7	ltled 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → 0 ≤ 4)
387	364	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ ℕ0)
388	37, 325, 387, 124, 359	leexp1ad 39987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2↑2) ≤ ((2 logb 𝐴)↑2))
389	338, 340, 5, 386, 388	lemul2ad 11924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (2↑2)) ≤ (4 · ((2 logb 𝐴)↑2)))
390	335, 339, 341, 385, 389	letrd 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2 logb 𝐴)↑2)))
391	37, 326	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℝ)
392	391	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) ∈ ℂ)
393	326	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈ ℂ)
394	274, 392, 393, 333	divdird 11798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)) = (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))))
396	395	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)) = 1)
398	397	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = (2 · 1))
399	398, 180	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1))) = 2)
400	399	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2 logb 𝐴)↑1) / ((2 logb 𝐴)↑1)))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
401	396, 400	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
402	394, 401	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) = ((;10 / ((2 logb 𝐴)↑1)) + 2))
403	402	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)))
404		2p1e3 12124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (2 + 1) = 3
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → (2 + 1) = 3)
406	302	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝜑 → 3 ∈ ℂ)
407	406, 53, 13	subadd2d 11360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝜑 → ((3 − 1) = 2 ↔ (2 + 1) = 3))
408	405, 407	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝜑 → (3 − 1) = 2)
409	408	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → 2 = (3 − 1))
410	409	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb 𝐴)↑(3 − 1)))
411	410	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · ((2 logb 𝐴)↑(3 − 1))))
412	3, 330	gtned 11119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → (2 logb 𝐴) ≠ 0)
413	342, 412, 239, 296	expsubd 13884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))
414	413	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑(3 − 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
415	411, 414	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
416	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 4 ∈ ℂ)
417	325, 112	reexpcld 13890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℝ)
418	417	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈ ℂ)
419	416, 418, 393, 333	divassd 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))))
420	419	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1))) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
421	415, 420	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑2)) = ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
422	390, 403, 421	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1)))
423	287, 391	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ∈ ℝ)
424	5, 417	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) ∈ ℝ)
425	423, 424, 332	lediv1d 12827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)) ↔ ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1))))
426	422, 425	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2 logb 𝐴)↑3)))
427	87	uzidd 12607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝜑 → 2 ∈ (ℤ≥‘2))
428	427, 39	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝜑 → (2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+))
429		relogbval 25931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((2 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
430	428, 429	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
431	430	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) / (log‘2))↑1))
432	431	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · ((2 logb 𝐴)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
433	432	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) = (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))))
434	430	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) / (log‘2))↑3))
435	12, 18, 26, 112	expdivd 13887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
436	434, 435	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) / ((log‘2)↑3)))
437	436	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (4 · ((2 logb 𝐴)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
438	426, 433, 437	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
439	292, 293, 299, 323, 438	letrd 11141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
440	12	exp1d 13868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴))
441	440	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1))
442	441	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (;10 / (log‘𝐴)) = (;10 / ((log‘𝐴)↑1)))
443	13, 156, 281, 282	divassd 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))))
444	12, 18, 26, 91	expdivd 13887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) = (((log‘𝐴)↑1) / ((log‘2)↑1)))
445	444	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝜑 → (((log‘𝐴)↑1) / ((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1))
446	445	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝜑 → (2 · (((log‘𝐴)↑1) / ((log‘2)↑1))) = (2 · (((log‘𝐴) / (log‘2))↑1)))
447	443, 446	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) = (2 · (((log‘𝐴) / (log‘2))↑1)))
448	447	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (2 · (((log‘𝐴) / (log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)))
449	442, 448	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))))
450	113	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
451	18, 112	expcld 13873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2)↑3) ∈ ℂ)
452	416, 450, 451, 297	divassd 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))))
453	452	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (4 · (((log‘𝐴)↑3) / ((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
454	439, 449, 453	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
455	285, 454	eqbrtrd 5097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
456	281, 282	dividd 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (((log‘2)↑1) / ((log‘2)↑1)) = 1)
457	456	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = (((log‘2)↑1) / ((log‘2)↑1)))
458	457	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · (((log‘2)↑1) / ((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
460	458, 459	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1))))
461	460	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1)))))
462	416, 450	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
463	462, 451, 297	divcld 11760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) ∈ ℂ)
464	463	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)))
465	464	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1))
466	455, 461, 465	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) ∈ ℂ)
468	467	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = (;10 / ((log‘𝐴)↑1)))
469	468	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · 1))
470	18, 26	dividd 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → ((log‘2) / (log‘2)) = 1)
471	470	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → 1 = ((log‘2) / (log‘2)))
472	471	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
473	469, 472	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))))
474	274, 156, 18, 18, 247, 26	divmuldivd 11801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · ((log‘2) / (log‘2))) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
475	473, 474	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))))
476	18	exp1d 13868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑1) = (log‘2))
477	476	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) · (log‘2)))
478		df-2 12045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ 2 = (1 + 1)
479	478	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝜑 → 2 = (1 + 1))
480	479	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑2) = ((log‘2)↑(1 + 1)))
481	18, 91, 91	expaddd 13875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → ((log‘2)↑(1 + 1)) = (((log‘2)↑1) · ((log‘2)↑1)))
482	480, 481	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2)↑2) = (((log‘2)↑1) · ((log‘2)↑1)))
483	482	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘2)↑1) · ((log‘2)↑1)) = ((log‘2)↑2))
484	477, 483	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1)) / (((log‘2)↑1) · ((log‘2)↑1)))) = (((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2))))
486	476	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (log‘2) = ((log‘2)↑1))
487	486	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → ((log‘2) / (log‘2)) = ((log‘2) / ((log‘2)↑1)))
488	471, 487	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 1 = ((log‘2) / ((log‘2)↑1)))
489	488	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))))
490	476, 18	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ∈ ℂ)
491	476, 26	eqnetrd 3012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑1) ≠ 0)
492	462, 451, 18, 490, 297, 491	divmuldivd 11801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
494	466, 485, 493	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2))) ≤ (((4 · ((log‘𝐴)↑3)) · (log‘2)) / (((log‘2)↑3) · ((log‘2)↑1))))
495	156, 18	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℂ)
496	156, 18, 247, 26	mulne0d 11636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ≠ 0)
497	274, 18, 495, 496	div23d 11797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → ((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) = ((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)))
498	277, 18, 155, 88	div23d 11797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2)) = (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2)))
499	497, 498	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (((;10 · (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) / ((log‘2)↑2))) = (((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))))
500	62	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → 4 = (3 + 1))
501	500	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑4) = ((log‘2)↑(3 + 1)))
502	18, 91, 112	expaddd 13875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → ((log‘2)↑(3 + 1)) = (((log‘2)↑3) · ((log‘2)↑1)))
503	501, 502	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → ((log‘2)↑4) = (((log‘2)↑3) · ((log‘2)↑1)))
504	503	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (((log‘2)↑3) · ((log‘2)↑1)) = ((log‘2)↑4))
505	504	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))) ≤ (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)))
507	92, 43	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (((log‘𝐴)↑1) · (log‘2)) ∈ ℝ)
508	287, 507, 496	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℝ)
509	508	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈ ℂ)
510	509, 278, 18	adddird 11009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) = (((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))))
511	510	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) · (log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) · (log‘2))) = (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)))
512	18, 26, 212	expne0d 13879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((log‘2)↑4) ≠ 0)
513	462, 18, 117, 512	div23d 11797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · (log‘2)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2)))
514	506, 511, 513	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (2 · ((log‘𝐴)↑1)) ∈ ℝ)
516	515, 85, 88	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)) ∈ ℝ)
517	508, 516	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈ ℝ)
518	114, 115, 120	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ∈ ℝ)
519	517, 518, 135	lemul1d 12824	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤ ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ↔ (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) · (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) · (log‘2))))
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 5097	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))))
523	53, 277, 155, 88	div12d 11796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
524	522, 523	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1 · ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) = ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))))
525	462	mulid1d 11001	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · 1) = (4 · ((log‘𝐴)↑3)))
526	525	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) = ((4 · ((log‘𝐴)↑3)) · 1))
527	526	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)))
528	521, 524, 527	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . . 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 11758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
530	529	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 1 = (𝐴 / 𝐴))
531	530	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))))
532	2, 2, 495, 11, 496	divdiv1d 11791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
533	531, 532	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))))
534	533	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))))
535		eqidd 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))))
536	530	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 / ((log‘2)↑2)) = ((𝐴 / 𝐴) / ((log‘2)↑2)))
537	536	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
538	535, 537	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))))
539	534, 538	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 / ((log‘2)↑2)))) = ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))))
540	462, 53, 117, 512	divassd 11795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) · 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
541	528, 539, 540	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))))
542	2, 495	mulcomd 11005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = ((((log‘𝐴)↑1) · (log‘2)) · 𝐴))
543	156, 18, 2	mulassd 11007	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ((((log‘𝐴)↑1) · (log‘2)) · 𝐴) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
544	542, 543	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) = (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))
545	544	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))))
546	545	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
547	2, 2, 155, 11, 88	divdiv1d 11791	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 · ((log‘2)↑2))))
548	2, 155	mulcomd 11005	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐴 · ((log‘2)↑2)) = (((log‘2)↑2) · 𝐴))
549	548	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2) · 𝐴)))
550	547, 549	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2) · 𝐴)))
551	550	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
552	546, 551	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) = ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))))
553		eqidd 2740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = (1 / ((log‘2)↑4)))
554	530	oveq1d 7299	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
555	553, 554	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / ((log‘2)↑4)) = ((𝐴 / 𝐴) / ((log‘2)↑4)))
556	555	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
557	541, 552, 556	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))))
558	156, 261	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℂ)
559	156, 261, 247, 262	mulne0d 11636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ≠ 0)
560	274, 558, 2, 559	div32d 11783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))))
561	560	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴)))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴))
562	155, 2	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ∈ ℂ)
563	155, 2, 88, 11	mulne0d 11636	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘2)↑2) · 𝐴) ≠ 0)
564	277, 562, 2, 563	div32d 11783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))))
565	564	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴))
566	561, 565	oveq12d 7302	. . . . . . . . . . . . . . . . . . . . . . 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 11791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 · ((log‘2)↑4))))
568	2, 117	mulcomd 11005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 · ((log‘2)↑4)) = (((log‘2)↑4) · 𝐴))
569	568	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4) · 𝐴)))
570	567, 569	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4) · 𝐴)))
571	570	oveq2d 7300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
572	557, 566, 571	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) · 𝐴) + (((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
573	43, 1	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((log‘2) · 𝐴) ∈ ℝ)
574	92, 573	remulcld 11014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (((log‘𝐴)↑1) · ((log‘2) · 𝐴)) ∈ ℝ)
575	287, 574, 559	redivcld 11812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℝ)
576	575	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) ∈ ℂ)
577	157, 94	eqeltrrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℝ)
578	577	recnd 11012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴)) ∈ ℂ)
579	576, 578, 2	adddird 11009	. . . . . . . . . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . . . . . . . . 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 13873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((log‘𝐴)↑3) ∈ ℂ)
582	416, 581	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · ((log‘𝐴)↑3)) ∈ ℂ)
583	117, 2	mulcld 11004	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ∈ ℂ)
584	117, 2, 512, 11	mulne0d 11636	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((log‘2)↑4) · 𝐴) ≠ 0)
585	582, 583, 2, 584	div32d 11783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))))
586	585	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
587	572, 580, 586	3brtr3d 5106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴))
588	575, 577	readdcld 11013	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ∈ ℝ)
589	588, 122, 39	lemul1d 12824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) ↔ (((;10 / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) · 𝐴)))
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 5097	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((5 · 2) / (((log‘𝐴)↑1) · ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
592	267, 591	eqbrtrd 5097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 · 1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
593	259, 592	eqbrtrd 5097	. . . . . . . . . . . . . . . . 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 5097	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((5 · (1 / ((log‘𝐴)↑1))) · ((2 / (log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
595	246, 594	eqbrtrd 5097	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑-1)) · ((2 / (log‘2)) · (((log‘2)↑5) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
596	238, 595	eqbrtrd 5097	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2 · ((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
597	211, 596	eqbrtrd 5097	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 · ((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
598	205, 597	eqbrtrd 5097	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((5 · ((log‘𝐴)↑4)) · (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) · ((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
599	198, 598	eqbrtrd 5097	. . . . . . . . . . 11 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) · (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
600	192, 599	eqbrtrd 5097	. . . . . . . . . 10 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) · (log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
601	189, 600	eqbrtrd 5097	. . . . . . . . 9 ⊢ (𝜑 → ((((2 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
602	184, 601	eqbrtrd 5097	. . . . . . . 8 ⊢ (𝜑 → (((((2 · 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
603	179, 602	eqbrtrd 5097	. . . . . . 7 ⊢ (𝜑 → ((((2 · (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
604	174, 603	eqbrtrd 5097	. . . . . 6 ⊢ (𝜑 → (((2 · ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
605	170, 604	eqbrtrd 5097	. . . . 5 ⊢ (𝜑 → ((2 · ((1 / ((((log‘𝐴)↑5) · (log‘2)) / ((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) / (((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
606	158, 605	eqbrtrd 5097	. . . 4 ⊢ (𝜑 → ((2 · ((1 / ((((log‘𝐴)↑5) / ((log‘2)↑5)) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
607	95, 111, 122, 149, 606	letrd 11141	. . 3 ⊢ (𝜑 → ((2 · ((1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
608	35, 607	eqbrtrd 5097	. 2 ⊢ (𝜑 → ((2 · ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
609	427, 39, 429	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) / (log‘2)))
610	609	eqcomd 2745	. . . . . . . . 9 ⊢ (𝜑 → ((log‘𝐴) / (log‘2)) = (2 logb 𝐴))
611	610	oveq1d 7299	. . . . . . . 8 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2 logb 𝐴)↑5))
612	611	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1) = (((2 logb 𝐴)↑5) + 1))
613	612	oveq1d 7299	. . . . . 6 ⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2)) = ((((2 logb 𝐴)↑5) + 1) · (log‘2)))
614	613	oveq2d 7300	. . . . 5 ⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))))
615		5cn 12070	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
616	615	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 5 ∈ ℂ)
617	616, 207	mulcld 11004	. . . . . . . . . . . . 13 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) ∈ ℂ)
618	617	mulid1d 11001	. . . . . . . . . . . 12 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) · 1) = (5 · ((log‘𝐴)↑4)))
619	618	eqcomd 2745	. . . . . . . . . . 11 ⊢ (𝜑 → (5 · ((log‘𝐴)↑4)) = ((5 · ((log‘𝐴)↑4)) · 1))
620		eqidd 2740	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑5) · 𝐴))
621		df-5 12048	. . . . . . . . . . . . . . . . . . 19 ⊢ 5 = (4 + 1)
622	621	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 5 = (4 + 1))
623	622	oveq2d 7300	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑5) = ((log‘2)↑(4 + 1)))
624	18, 91, 77	expaddd 13875	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((log‘2)↑(4 + 1)) = (((log‘2)↑4) · ((log‘2)↑1)))
625	623, 624	eqtrd 2779	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · ((log‘2)↑1)))
626	476	oveq2d 7300	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2)↑1)) = (((log‘2)↑4) · (log‘2)))
627	625, 626	eqtrd 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((log‘2)↑5) = (((log‘2)↑4) · (log‘2)))
628	627	oveq1d 7299	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
629	620, 628	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = ((((log‘2)↑4) · (log‘2)) · 𝐴))
630	117, 18, 2	mulassd 11007	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((log‘2)↑4) · (log‘2)) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
631	629, 630	eqtrd 2779	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · ((log‘2) · 𝐴)))
632	18, 2	mulcomd 11005	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((log‘2) · 𝐴) = (𝐴 · (log‘2)))
633	632	oveq2d 7300	. . . . . . . . . . . 12 ⊢ (𝜑 → (((log‘2)↑4) · ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 · (log‘2))))
634	631, 633	eqtrd 2779	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘2)↑5) · 𝐴) = (((log‘2)↑4) · (𝐴 · (log‘2))))
635	619, 634	oveq12d 7302	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
636	2, 18	mulcld 11004	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ∈ ℂ)
637	2, 18, 11, 26	mulne0d 11636	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
638	186, 117, 53, 636, 120, 637	divmuldivd 11801	. . . . . . . . . . 11 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))))
639	638	eqcomd 2745	. . . . . . . . . 10 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) · 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
640	635, 639	eqtrd 2779	. . . . . . . . 9 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))))
641	206, 207, 117, 120	divassd 11795	. . . . . . . . . 10 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))))
642	641	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → (((5 · ((log‘𝐴)↑4)) / ((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
643	640, 642	eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))))
644	12, 18, 26, 77	expdivd 13887	. . . . . . . . . . 11 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = (((log‘𝐴)↑4) / ((log‘2)↑4)))
645	644	eqcomd 2745	. . . . . . . . . 10 ⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4))
646	645	oveq2d 7300	. . . . . . . . 9 ⊢ (𝜑 → (5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) = (5 · (((log‘𝐴) / (log‘2))↑4)))
647	646	oveq1d 7299	. . . . . . . 8 ⊢ (𝜑 → ((5 · (((log‘𝐴)↑4) / ((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
648	643, 647	eqtrd 2779	. . . . . . 7 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))))
649	610	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2 logb 𝐴)↑4))
650	649	oveq2d 7300	. . . . . . . 8 ⊢ (𝜑 → (5 · (((log‘𝐴) / (log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4)))
651	650	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → ((5 · (((log‘𝐴) / (log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
652	648, 651	eqtrd 2779	. . . . . 6 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
653	342, 77	expcld 13873	. . . . . . . . . 10 ⊢ (𝜑 → ((2 logb 𝐴)↑4) ∈ ℂ)
654	616, 653	mulcld 11004	. . . . . . . . 9 ⊢ (𝜑 → (5 · ((2 logb 𝐴)↑4)) ∈ ℂ)
655	39	rpne0d 12786	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 0)
656	2, 18, 655, 26	mulne0d 11636	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · (log‘2)) ≠ 0)
657	636, 656	reccld 11753	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝐴 · (log‘2))) ∈ ℂ)
658	654, 657	mulcld 11004	. . . . . . . 8 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) ∈ ℂ)
659	658	addid1d 11184	. . . . . . 7 ⊢ (𝜑 → (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))))
660	659	eqcomd 2745	. . . . . 6 ⊢ (𝜑 → ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
661	652, 660	eqtrd 2779	. . . . 5 ⊢ (𝜑 → ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))
662	614, 661	oveq12d 7302	. . . 4 ⊢ (𝜑 → ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴))) = ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0)))
663	662	oveq2d 7300	. . 3 ⊢ (𝜑 → (2 · ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) = (2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))))
664		1e2m1 12109	. . . . . . 7 ⊢ 1 = (2 − 1)
665	664	a1i 11	. . . . . 6 ⊢ (𝜑 → 1 = (2 − 1))
666	665	oveq2d 7300	. . . . 5 ⊢ (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 − 1)))
667	666	oveq1d 7299	. . . 4 ⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴))
668	667	oveq2d 7300	. . 3 ⊢ (𝜑 → ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))
669	663, 668	oveq12d 7302	. 2 ⊢ (𝜑 → ((2 · ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1) · (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))))
670		4cn 12067	. . . . 5 ⊢ 4 ∈ ℂ
671	670	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
672	671, 117, 581, 2, 120, 655	divmuldivd 11801	. . 3 ⊢ (𝜑 → ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)))
673	672	eqcomd 2745	. 2 ⊢ (𝜑 → ((4 · ((log‘𝐴)↑3)) / (((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))
674	608, 669, 673	3brtr3d 5106	1 ⊢ (𝜑 → ((2 · ((1 / ((((2 logb 𝐴)↑5) + 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) + 0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴))) ≤ ((4 / ((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6437  (class class class)co 7284  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881   + caddc 10883   · cmul 10885   < clt 11018   ≤ cle 11019   − cmin 11214  -cneg 11215   / cdiv 11641  ℕcn 11982  2c2 12037  3c3 12038  4c4 12039  5c5 12040  6c6 12041  7c7 12042  9c9 12044  ℕ₀cn0 12242  ℤcz 12328  ;cdc 12446  ℤ_≥cuz 12591  ℝ⁺crp 12739  ↑cexp 13791  eceu 15781  logclog 25719   log_b clogb 25923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-inf2 9408  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958  ax-addf 10959  ax-mulf 10960

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-iin 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-isom 6446  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-of 7542  df-om 7722  df-1st 7840  df-2nd 7841  df-supp 7987  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-1o 8306  df-2o 8307  df-er 8507  df-map 8626  df-pm 8627  df-ixp 8695  df-en 8743  df-dom 8744  df-sdom 8745  df-fin 8746  df-fsupp 9138  df-fi 9179  df-sup 9210  df-inf 9211  df-oi 9278  df-card 9706  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-3 12046  df-4 12047  df-5 12048  df-6 12049  df-7 12050  df-8 12051  df-9 12052  df-n0 12243  df-z 12329  df-dec 12447  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ioo 13092  df-ioc 13093  df-ico 13094  df-icc 13095  df-fz 13249  df-fzo 13392  df-fl 13521  df-mod 13599  df-seq 13731  df-exp 13792  df-fac 13997  df-bc 14026  df-hash 14054  df-shft 14787  df-cj 14819  df-re 14820  df-im 14821  df-sqrt 14955  df-abs 14956  df-limsup 15189  df-clim 15206  df-rlim 15207  df-sum 15407  df-ef 15786  df-e 15787  df-sin 15788  df-cos 15789  df-pi 15791  df-struct 16857  df-sets 16874  df-slot 16892  df-ndx 16904  df-base 16922  df-ress 16951  df-plusg 16984  df-mulr 16985  df-starv 16986  df-sca 16987  df-vsca 16988  df-ip 16989  df-tset 16990  df-ple 16991  df-ds 16993  df-unif 16994  df-hom 16995  df-cco 16996  df-rest 17142  df-topn 17143  df-0g 17161  df-gsum 17162  df-topgen 17163  df-pt 17164  df-prds 17167  df-xrs 17222  df-qtop 17227  df-imas 17228  df-xps 17230  df-mre 17304  df-mrc 17305  df-acs 17307  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-submnd 18440  df-mulg 18710  df-cntz 18932  df-cmn 19397  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-fbas 20603  df-fg 20604  df-cnfld 20607  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-cld 22179  df-ntr 22180  df-cls 22181  df-nei 22258  df-lp 22296  df-perf 22297  df-cn 22387  df-cnp 22388  df-haus 22475  df-tx 22722  df-hmeo 22915  df-fil 23006  df-fm 23098  df-flim 23099  df-flf 23100  df-xms 23482  df-ms 23483  df-tms 23484  df-cncf 24050  df-limc 25039  df-dv 25040  df-log 25721  df-cxp 25722  df-logb 25924

This theorem is referenced by:  aks4d1p1p5  40090