Theorem aks4d1p1p7

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

	Ref	Expression
Hypotheses	aks4d1p1p7.1	$$⊢\phi \to A\in ℝ$$
	aks4d1p1p7.2	$$⊢\phi \to 4\le A$$
Assertion	aks4d1p1p7	$$⊢\phi \to 2\left(\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}\right)\left(5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^{2-1}}{A}\right)\le \left(\frac{4}{{\log 2}^4}\right)\left(\frac{{\log A}^3}{A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p7.1	$$⊢\phi \to A\in ℝ$$
2		aks4d1p1p7.2	$$⊢\phi \to 4\le A$$
3	1	recnd	$$⊢\phi \to A\in ℂ$$
4		0red	$$⊢\phi \to 0\in ℝ$$
5		4re	$$⊢4\in ℝ$$
6	5	a1i	$$⊢\phi \to 4\in ℝ$$
7		4pos	$$⊢0<4$$
8	7	a1i	$$⊢\phi \to 0<4$$
9	4 6 1 8 2	ltletrd	$$⊢\phi \to 0<A$$
10	4 9	ltned	$$⊢\phi \to 0\ne A$$
11	10	necomd	$$⊢\phi \to A\ne 0$$
12	3 11	logcld	$$⊢\phi \to \log A\in ℂ$$
13		2cnd	$$⊢\phi \to 2\in ℂ$$
14		2pos	$$⊢0<2$$
15	14	a1i	$$⊢\phi \to 0<2$$
16	4 15	ltned	$$⊢\phi \to 0\ne 2$$
17	16	necomd	$$⊢\phi \to 2\ne 0$$
18	13 17	logcld	$$⊢\phi \to \log 2\in ℂ$$
19		1lt2	$$⊢1<2$$
20		2rp	$$⊢2\in {ℝ}^{+}$$
21		loggt0b	$$⊢2\in {ℝ}^{+}\to \left(0<\log 2\leftrightarrow 1<2\right)$$
22	20 21	ax-mp	$$⊢0<\log 2\leftrightarrow 1<2$$
23	19 22	mpbir	$$⊢0<\log 2$$
24	23	a1i	$$⊢\phi \to 0<\log 2$$
25	4 24	ltned	$$⊢\phi \to 0\ne \log 2$$
26	25	necomd	$$⊢\phi \to \log 2\ne 0$$
27		5nn0	$$⊢5\in {\mathbb{N}}_0$$
28	27	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
29	12 18 26 28	expdivd	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^5=\frac{{\log A}^5}{{\log 2}^5}$$
30	29	oveq1d	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^5+1=\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1$$
31	30	oveq1d	$$⊢\phi \to \left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2=\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2$$
32	31	oveq2d	$$⊢\phi \to \frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}=\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}$$
33	32	oveq1d	$$⊢\phi \to \left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
34	33	oveq2d	$$⊢\phi \to 2\left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
35	34	oveq1d	$$⊢\phi \to 2\left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)=2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)$$
36		2re	$$⊢2\in ℝ$$
37	36	a1i	$$⊢\phi \to 2\in ℝ$$
38		1red	$$⊢\phi \to 1\in ℝ$$
39	1 9	elrpd	$$⊢\phi \to A\in {ℝ}^{+}$$
40	39	relogcld	$$⊢\phi \to \log A\in ℝ$$
41	40 28	reexpcld	$$⊢\phi \to {\log A}^5\in ℝ$$
42	20	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
43	42	relogcld	$$⊢\phi \to \log 2\in ℝ$$
44	43 28	reexpcld	$$⊢\phi \to {\log 2}^5\in ℝ$$
45	28	nn0zd	$$⊢\phi \to 5\in \mathbb{Z}$$
46	18 26 45	expne0d	$$⊢\phi \to {\log 2}^5\ne 0$$
47	41 44 46	redivcld	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}\in ℝ$$
48	47 38	readdcld	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\in ℝ$$
49	48 43	remulcld	$$⊢\phi \to \left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2\in ℝ$$
50	12 28	expcld	$$⊢\phi \to {\log A}^5\in ℂ$$
51	18 28	expcld	$$⊢\phi \to {\log 2}^5\in ℂ$$
52	50 51 46	divcld	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}\in ℂ$$
53		1cnd	$$⊢\phi \to 1\in ℂ$$
54	52 53	addcld	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\in ℂ$$
55	19	a1i	$$⊢\phi \to 1<2$$
56	37 55	rplogcld	$$⊢\phi \to \log 2\in {ℝ}^{+}$$
57	56 45	rpexpcld	$$⊢\phi \to {\log 2}^5\in {ℝ}^{+}$$
58		1re	$$⊢1\in ℝ$$
59		3nn0	$$⊢3\in {\mathbb{N}}_0$$
60	58 59	nn0addge2i	$$⊢1\le 3+1$$
61	60	a1i	$$⊢\phi \to 1\le 3+1$$
62		df-4	$$⊢4=3+1$$
63	61 62	breqtrrdi	$$⊢\phi \to 1\le 4$$
64	38 6 1 63 2	letrd	$$⊢\phi \to 1\le A$$
65	1 64	logge0d	$$⊢\phi \to 0\le \log A$$
66	40 28 65	expge0d	$$⊢\phi \to 0\le {\log A}^5$$
67	41 57 66	divge0d	$$⊢\phi \to 0\le \frac{{\log A}^5}{{\log 2}^5}$$
68	47	ltp1d	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}<\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1$$
69	4 47 48 67 68	lelttrd	$$⊢\phi \to 0<\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1$$
70	4 69	ltned	$$⊢\phi \to 0\ne \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1$$
71	70	necomd	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\ne 0$$
72	54 18 71 26	mulne0d	$$⊢\phi \to \left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2\ne 0$$
73	38 49 72	redivcld	$$⊢\phi \to \frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\in ℝ$$
74		5re	$$⊢5\in ℝ$$
75	74	a1i	$$⊢\phi \to 5\in ℝ$$
76		4nn0	$$⊢4\in {\mathbb{N}}_0$$
77	76	a1i	$$⊢\phi \to 4\in {\mathbb{N}}_0$$
78	40 77	reexpcld	$$⊢\phi \to {\log A}^4\in ℝ$$
79	75 78	remulcld	$$⊢\phi \to 5{\log A}^4\in ℝ$$
80	44 1	remulcld	$$⊢\phi \to {\log 2}^{5}A\in ℝ$$
81	51 3 46 11	mulne0d	$$⊢\phi \to {\log 2}^{5}A\ne 0$$
82	79 80 81	redivcld	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}\in ℝ$$
83	73 82	remulcld	$$⊢\phi \to \left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\in ℝ$$
84	37 83	remulcld	$$⊢\phi \to 2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\in ℝ$$
85	43	resqcld	$$⊢\phi \to {\log 2}^2\in ℝ$$
86		2z	$$⊢2\in \mathbb{Z}$$
87	86	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
88	18 26 87	expne0d	$$⊢\phi \to {\log 2}^2\ne 0$$
89	37 85 88	redivcld	$$⊢\phi \to \frac{2}{{\log 2}^2}\in ℝ$$
90		1nn0	$$⊢1\in {\mathbb{N}}_0$$
91	90	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
92	40 91	reexpcld	$$⊢\phi \to {\log A}^1\in ℝ$$
93	92 1 11	redivcld	$$⊢\phi \to \frac{{\log A}^1}{A}\in ℝ$$
94	89 93	remulcld	$$⊢\phi \to \left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\in ℝ$$
95	84 94	readdcld	$$⊢\phi \to 2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\in ℝ$$
96	47 43	remulcld	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2\in ℝ$$
97		1lt4	$$⊢1<4$$
98	97	a1i	$$⊢\phi \to 1<4$$
99	38 6 1 98 2	ltletrd	$$⊢\phi \to 1<A$$
100		loggt0b	$$⊢A\in {ℝ}^{+}\to \left(0<\log A\leftrightarrow 1<A\right)$$
101	39 100	syl	$$⊢\phi \to \left(0<\log A\leftrightarrow 1<A\right)$$
102	99 101	mpbird	$$⊢\phi \to 0<\log A$$
103	4 102	ltned	$$⊢\phi \to 0\ne \log A$$
104	103	necomd	$$⊢\phi \to \log A\ne 0$$
105	12 104 45	expne0d	$$⊢\phi \to {\log A}^5\ne 0$$
106	50 51 105 46	divne0d	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}\ne 0$$
107	52 18 106 26	mulne0d	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2\ne 0$$
108	38 96 107	redivcld	$$⊢\phi \to \frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\in ℝ$$
109	108 82	remulcld	$$⊢\phi \to \left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\in ℝ$$
110	37 109	remulcld	$$⊢\phi \to 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\in ℝ$$
111	110 94	readdcld	$$⊢\phi \to 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\in ℝ$$
112	59	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
113	40 112	reexpcld	$$⊢\phi \to {\log A}^3\in ℝ$$
114	6 113	remulcld	$$⊢\phi \to 4{\log A}^3\in ℝ$$
115	43 77	reexpcld	$$⊢\phi \to {\log 2}^4\in ℝ$$
116	115 1	remulcld	$$⊢\phi \to {\log 2}^{4}A\in ℝ$$
117	18 77	expcld	$$⊢\phi \to {\log 2}^4\in ℂ$$
118		4z	$$⊢4\in \mathbb{Z}$$
119	118	a1i	$$⊢\phi \to 4\in \mathbb{Z}$$
120	18 26 119	expne0d	$$⊢\phi \to {\log 2}^4\ne 0$$
121	117 3 120 11	mulne0d	$$⊢\phi \to {\log 2}^{4}A\ne 0$$
122	114 116 121	redivcld	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^{4}A}\in ℝ$$
123		0le2	$$⊢0\le 2$$
124	123	a1i	$$⊢\phi \to 0\le 2$$
125	57 39	rpmulcld	$$⊢\phi \to {\log 2}^{5}A\in {ℝ}^{+}$$
126	28	nn0ge0d	$$⊢\phi \to 0\le 5$$
127	40 77 65	expge0d	$$⊢\phi \to 0\le {\log A}^4$$
128	75 78 126 127	mulge0d	$$⊢\phi \to 0\le 5{\log A}^4$$
129	79 125 128	divge0d	$$⊢\phi \to 0\le \frac{5{\log A}^4}{{\log 2}^{5}A}$$
130	1 99	rplogcld	$$⊢\phi \to \log A\in {ℝ}^{+}$$
131	130 45	rpexpcld	$$⊢\phi \to {\log A}^5\in {ℝ}^{+}$$
132	131 57	rpdivcld	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}\in {ℝ}^{+}$$
133	132 56	rpmulcld	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2\in {ℝ}^{+}$$
134	24 22	sylib	$$⊢\phi \to 1<2$$
135	37 134	rplogcld	$$⊢\phi \to \log 2\in {ℝ}^{+}$$
136	135 45	rpexpcld	$$⊢\phi \to {\log 2}^5\in {ℝ}^{+}$$
137	41 136 66	divge0d	$$⊢\phi \to 0\le \frac{{\log A}^5}{{\log 2}^5}$$
138	47 137	ge0p1rpd	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\in {ℝ}^{+}$$
139	138 135	rpmulcld	$$⊢\phi \to \left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2\in {ℝ}^{+}$$
140		0le1	$$⊢0\le 1$$
141	140	a1i	$$⊢\phi \to 0\le 1$$
142	135	rpred	$$⊢\phi \to \log 2\in ℝ$$
143	135	rpge0d	$$⊢\phi \to 0\le \log 2$$
144	47	lep1d	$$⊢\phi \to \frac{{\log A}^5}{{\log 2}^5}\le \left(\frac{{\log A}^5}{{\log 2}^5}\right)+1$$
145	47 48 142 143 144	lemul1ad	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2\le \left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2$$
146	133 139 38 141 145	lediv2ad	$$⊢\phi \to \frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\le \frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}$$
147	73 108 82 129 146	lemul1ad	$$⊢\phi \to \left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\le \left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
148	83 109 37 124 147	lemul2ad	$$⊢\phi \to 2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)\le 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
149	84 110 94 148	leadd1dd	$$⊢\phi \to 2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\le 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)$$
150	50 18 51 46	div23d	$$⊢\phi \to \frac{{\log A}^5\log 2}{{\log 2}^5}=\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2$$
151	150	eqcomd	$$⊢\phi \to \left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2=\frac{{\log A}^5\log 2}{{\log 2}^5}$$
152	151	oveq2d	$$⊢\phi \to \frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}=\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}$$
153	152	oveq1d	$$⊢\phi \to \left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
154	153	oveq2d	$$⊢\phi \to 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
155	18	sqcld	$$⊢\phi \to {\log 2}^2\in ℂ$$
156	12 91	expcld	$$⊢\phi \to {\log A}^1\in ℂ$$
157	13 155 156 3 88 11	divmuldivd	$$⊢\phi \to \left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)=\frac{2{\log A}^1}{{\log 2}^{2}A}$$
158	154 157	oveq12d	$$⊢\phi \to 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)=2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
159	50 18	mulcld	$$⊢\phi \to {\log A}^5\log 2\in ℂ$$
160	50 18 105 26	mulne0d	$$⊢\phi \to {\log A}^5\log 2\ne 0$$
161	53 159 51 160 46	divdiv2d	$$⊢\phi \to \frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}=\frac{1{\log 2}^5}{{\log A}^5\log 2}$$
162	161	oveq1d	$$⊢\phi \to \left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
163	162	oveq2d	$$⊢\phi \to 2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
164	53 51	mulcld	$$⊢\phi \to 1{\log 2}^5\in ℂ$$
165	164 159 160	divcld	$$⊢\phi \to \frac{1{\log 2}^5}{{\log A}^5\log 2}\in ℂ$$
166	82	recnd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}\in ℂ$$
167	13 165 166	mulassd	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
168	167	eqcomd	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
169	163 168	eqtrd	$$⊢\phi \to 2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
170	169	oveq1d	$$⊢\phi \to 2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
171	13 164 159 160	divassd	$$⊢\phi \to \frac{21{\log 2}^5}{{\log A}^5\log 2}=2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)$$
172	171	eqcomd	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)=\frac{21{\log 2}^5}{{\log A}^5\log 2}$$
173	172	oveq1d	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{21{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
174	173	oveq1d	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{21{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
175	13 53 51	mulassd	$$⊢\phi \to 2\cdot 1{\log 2}^5=21{\log 2}^5$$
176	175	eqcomd	$$⊢\phi \to 21{\log 2}^5=2\cdot 1{\log 2}^5$$
177	176	oveq1d	$$⊢\phi \to \frac{21{\log 2}^5}{{\log A}^5\log 2}=\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}$$
178	177	oveq1d	$$⊢\phi \to \left(\frac{21{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
179	178	oveq1d	$$⊢\phi \to \left(\frac{21{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
180	13	mulid1d	$$⊢\phi \to 2\cdot 1=2$$
181	180	oveq1d	$$⊢\phi \to 2\cdot 1{\log 2}^5=2{\log 2}^5$$
182	181	oveq1d	$$⊢\phi \to \frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}=\frac{2{\log 2}^5}{{\log A}^5\log 2}$$
183	182	oveq1d	$$⊢\phi \to \left(\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{2{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)$$
184	183	oveq1d	$$⊢\phi \to \left(\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{2{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
185	13 51	mulcld	$$⊢\phi \to 2{\log 2}^5\in ℂ$$
186	79	recnd	$$⊢\phi \to 5{\log A}^4\in ℂ$$
187	51 3	mulcld	$$⊢\phi \to {\log 2}^{5}A\in ℂ$$
188	185 159 186 187 160 81	divmuldivd	$$⊢\phi \to \left(\frac{2{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}$$
189	188	oveq1d	$$⊢\phi \to \left(\frac{2{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
190	50 18 187	mulassd	$$⊢\phi \to {\log A}^5\log 2{\log 2}^{5}A={\log A}^5\log 2{\log 2}^{5}A$$
191	190	oveq2d	$$⊢\phi \to \frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}=\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}$$
192	191	oveq1d	$$⊢\phi \to \left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
193	185 186	mulcomd	$$⊢\phi \to 2{\log 2}^{5}5{\log A}^4=5{\log A}^{4}2{\log 2}^5$$
194	18 51 3	mulassd	$$⊢\phi \to \log 2{\log 2}^{5}A=\log 2{\log 2}^{5}A$$
195	194	eqcomd	$$⊢\phi \to \log 2{\log 2}^{5}A=\log 2{\log 2}^{5}A$$
196	195	oveq2d	$$⊢\phi \to {\log A}^5\log 2{\log 2}^{5}A={\log A}^5\log 2{\log 2}^{5}A$$
197	193 196	oveq12d	$$⊢\phi \to \frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}=\frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}$$
198	197	oveq1d	$$⊢\phi \to \left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
199	18 51	mulcld	$$⊢\phi \to \log 2{\log 2}^5\in ℂ$$
200	199 3	mulcld	$$⊢\phi \to \log 2{\log 2}^{5}A\in ℂ$$
201	18 51 26 46	mulne0d	$$⊢\phi \to \log 2{\log 2}^5\ne 0$$
202	199 3 201 11	mulne0d	$$⊢\phi \to \log 2{\log 2}^{5}A\ne 0$$
203	186 50 185 200 105 202	divmuldivd	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)=\frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}$$
204	203	eqcomd	$$⊢\phi \to \frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}=\left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)$$
205	204	oveq1d	$$⊢\phi \to \left(\frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
206	75	recnd	$$⊢\phi \to 5\in ℂ$$
207	78	recnd	$$⊢\phi \to {\log A}^4\in ℂ$$
208	206 207 50 105	divassd	$$⊢\phi \to \frac{5{\log A}^4}{{\log A}^5}=5\left(\frac{{\log A}^4}{{\log A}^5}\right)$$
209	194	oveq2d	$$⊢\phi \to \frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}=\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}$$
210	208 209	oveq12d	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)=5\left(\frac{{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)$$
211	210	oveq1d	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=5\left(\frac{{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
212	77	nn0zd	$$⊢\phi \to 4\in \mathbb{Z}$$
213	12 104 45 212	expsubd	$$⊢\phi \to {\log A}^{4-5}=\frac{{\log A}^4}{{\log A}^5}$$
214	213	eqcomd	$$⊢\phi \to \frac{{\log A}^4}{{\log A}^5}={\log A}^{4-5}$$
215		4p1e5	$$⊢4+1=5$$
216	74	recni	$$⊢5\in ℂ$$
217	5	recni	$$⊢4\in ℂ$$
218		ax-1cn	$$⊢1\in ℂ$$
219	216 217 218	subaddi	$$⊢5-4=1\leftrightarrow 4+1=5$$
220	215 219	mpbir	$$⊢5-4=1$$
221	220	a1i	$$⊢\phi \to 5-4=1$$
222	53	subid1d	$$⊢\phi \to 1-0=1$$
223	221 222	eqtr4d	$$⊢\phi \to 5-4=1-0$$
224	206 217	jctir	$$⊢\phi \to \left(5\in ℂ\wedge 4\in ℂ\right)$$
225		0cnd	$$⊢\phi \to 0\in ℂ$$
226	53 225	jca	$$⊢\phi \to \left(1\in ℂ\wedge 0\in ℂ\right)$$
227		subeqrev	$$⊢\left(\left(5\in ℂ\wedge 4\in ℂ\right)\wedge \left(1\in ℂ\wedge 0\in ℂ\right)\right)\to \left(5-4=1-0\leftrightarrow 4-5=0-1\right)$$
228	224 226 227	syl2anc	$$⊢\phi \to \left(5-4=1-0\leftrightarrow 4-5=0-1\right)$$
229	223 228	mpbid	$$⊢\phi \to 4-5=0-1$$
230		df-neg	$$⊢-1=0-1$$
231	229 230	eqtr4di	$$⊢\phi \to 4-5=-1$$
232	231	oveq2d	$$⊢\phi \to {\log A}^{4-5}={\log A}^{-1}$$
233	214 232	eqtrd	$$⊢\phi \to \frac{{\log A}^4}{{\log A}^5}={\log A}^{-1}$$
234	233	oveq2d	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log A}^5}\right)=5{\log A}^{-1}$$
235	13 18 51 187 26 81	divmuldivd	$$⊢\phi \to \left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)=\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}$$
236	235	eqcomd	$$⊢\phi \to \frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}=\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)$$
237	234 236	oveq12d	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)=5{\log A}^{-1}\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)$$
238	237	oveq1d	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=5{\log A}^{-1}\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
239		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
240	12 104 239	expnegd	$$⊢\phi \to {\log A}^{-1}=\frac{1}{{\log A}^1}$$
241	240	oveq2d	$$⊢\phi \to 5{\log A}^{-1}=5\left(\frac{1}{{\log A}^1}\right)$$
242	51 51 3 46 11	divdiv1d	$$⊢\phi \to \frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}=\frac{{\log 2}^5}{{\log 2}^{5}A}$$
243	242	eqcomd	$$⊢\phi \to \frac{{\log 2}^5}{{\log 2}^{5}A}=\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}$$
244	243	oveq2d	$$⊢\phi \to \left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)=\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)$$
245	241 244	oveq12d	$$⊢\phi \to 5{\log A}^{-1}\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)=5\left(\frac{1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)$$
246	245	oveq1d	$$⊢\phi \to 5{\log A}^{-1}\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=5\left(\frac{1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
247	12 104 239	expne0d	$$⊢\phi \to {\log A}^1\ne 0$$
248	206 53 156 247	divassd	$$⊢\phi \to \frac{5\cdot 1}{{\log A}^1}=5\left(\frac{1}{{\log A}^1}\right)$$
249	248	eqcomd	$$⊢\phi \to 5\left(\frac{1}{{\log A}^1}\right)=\frac{5\cdot 1}{{\log A}^1}$$
250	51 46	dividd	$$⊢\phi \to \frac{{\log 2}^5}{{\log 2}^5}=1$$
251	250	oveq1d	$$⊢\phi \to \frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}=\frac{1}{A}$$
252	251	oveq2d	$$⊢\phi \to \left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)=\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)$$
253	249 252	oveq12d	$$⊢\phi \to 5\left(\frac{1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)=\left(\frac{5\cdot 1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)$$
254	253	oveq1d	$$⊢\phi \to 5\left(\frac{1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{5\cdot 1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
255	206	mulid1d	$$⊢\phi \to 5\cdot 1=5$$
256	255	oveq1d	$$⊢\phi \to \frac{5\cdot 1}{{\log A}^1}=\frac{5}{{\log A}^1}$$
257	13 18 53 3 26 11	divmuldivd	$$⊢\phi \to \left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)=\frac{2\cdot 1}{\log 2A}$$
258	256 257	oveq12d	$$⊢\phi \to \left(\frac{5\cdot 1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)=\left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)$$
259	258	oveq1d	$$⊢\phi \to \left(\frac{5\cdot 1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
260	180 13	eqeltrd	$$⊢\phi \to 2\cdot 1\in ℂ$$
261	18 3	mulcld	$$⊢\phi \to \log 2A\in ℂ$$
262	18 3 26 11	mulne0d	$$⊢\phi \to \log 2A\ne 0$$
263	206 156 260 261 247 262	divmuldivd	$$⊢\phi \to \left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)=\frac{52\cdot 1}{{\log A}^1\log 2A}$$
264	180	oveq2d	$$⊢\phi \to 52\cdot 1=5\cdot 2$$
265	264	oveq1d	$$⊢\phi \to \frac{52\cdot 1}{{\log A}^1\log 2A}=\frac{5\cdot 2}{{\log A}^1\log 2A}$$
266	263 265	eqtrd	$$⊢\phi \to \left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)=\frac{5\cdot 2}{{\log A}^1\log 2A}$$
267	266	oveq1d	$$⊢\phi \to \left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{5\cdot 2}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
268		5t2e10	$$⊢5\cdot 2=10$$
269	268	a1i	$$⊢\phi \to 5\cdot 2=10$$
270	269	oveq1d	$$⊢\phi \to \frac{5\cdot 2}{{\log A}^1\log 2A}=\frac{10}{{\log A}^1\log 2A}$$
271	270	oveq1d	$$⊢\phi \to \left(\frac{5\cdot 2}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)=\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)$$
272		10nn0	$$⊢10\in {\mathbb{N}}_0$$
273	272	nn0cni	$$⊢10\in ℂ$$
274	273	a1i	$$⊢\phi \to 10\in ℂ$$
275	274	mulid1d	$$⊢\phi \to 10\cdot 1=10$$
276	275	oveq1d	$$⊢\phi \to \frac{10\cdot 1}{{\log A}^1\log 2}=\frac{10}{{\log A}^1\log 2}$$
277	13 156	mulcld	$$⊢\phi \to 2{\log A}^1\in ℂ$$
278	277 155 88	divcld	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^2}\in ℂ$$
279	278	mulid2d	$$⊢\phi \to 1\left(\frac{2{\log A}^1}{{\log 2}^2}\right)=\frac{2{\log A}^1}{{\log 2}^2}$$
280	276 279	oveq12d	$$⊢\phi \to \left(\frac{10\cdot 1}{{\log A}^1\log 2}\right)+1\left(\frac{2{\log A}^1}{{\log 2}^2}\right)=\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)$$
281	18 91	expcld	$$⊢\phi \to {\log 2}^1\in ℂ$$
282	18 26 239	expne0d	$$⊢\phi \to {\log 2}^1\ne 0$$
283	277 281 282	divcld	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^1}\in ℂ$$
284	283	mulid1d	$$⊢\phi \to \left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1=\frac{2{\log A}^1}{{\log 2}^1}$$
285	284	oveq2d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1=\left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)$$
286		10re	$$⊢10\in ℝ$$
287	286	a1i	$$⊢\phi \to 10\in ℝ$$
288	287 40 104	redivcld	$$⊢\phi \to \frac{10}{\log A}\in ℝ$$
289	40 43 26	redivcld	$$⊢\phi \to \frac{\log A}{\log 2}\in ℝ$$
290	289 91	reexpcld	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^1\in ℝ$$
291	37 290	remulcld	$$⊢\phi \to 2{\left(\frac{\log A}{\log 2}\right)}^1\in ℝ$$
292	288 291	readdcld	$$⊢\phi \to \left(\frac{10}{\log A}\right)+2{\left(\frac{\log A}{\log 2}\right)}^1\in ℝ$$
293	287 291	readdcld	$$⊢\phi \to 10+2{\left(\frac{\log A}{\log 2}\right)}^1\in ℝ$$
294	43 112	reexpcld	$$⊢\phi \to {\log 2}^3\in ℝ$$
295		3z	$$⊢3\in \mathbb{Z}$$
296	295	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
297	18 26 296	expne0d	$$⊢\phi \to {\log 2}^3\ne 0$$
298	113 294 297	redivcld	$$⊢\phi \to \frac{{\log A}^3}{{\log 2}^3}\in ℝ$$
299	6 298	remulcld	$$⊢\phi \to 4\left(\frac{{\log A}^3}{{\log 2}^3}\right)\in ℝ$$
300		ere	$$⊢\mathrm{e}\in ℝ$$
301	300	a1i	$$⊢\phi \to \mathrm{e}\in ℝ$$
302	112	nn0red	$$⊢\phi \to 3\in ℝ$$
303		egt2lt3	$$⊢\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$$
304	303	simpri	$$⊢\mathrm{e}<3$$
305	304	a1i	$$⊢\phi \to \mathrm{e}<3$$
306		3lt4	$$⊢3<4$$
307	306	a1i	$$⊢\phi \to 3<4$$
308	302 6 1 307 2	ltletrd	$$⊢\phi \to 3<A$$
309	301 302 1 305 308	lttrd	$$⊢\phi \to \mathrm{e}<A$$
310	301 1 309	ltled	$$⊢\phi \to \mathrm{e}\le A$$
311	301 1	lenltd	$$⊢\phi \to \left(\mathrm{e}\le A\leftrightarrow \neg A<\mathrm{e}\right)$$
312	310 311	mpbid	$$⊢\phi \to \neg A<\mathrm{e}$$
313		loglt1b	$$⊢A\in {ℝ}^{+}\to \left(\log A<1\leftrightarrow A<\mathrm{e}\right)$$
314	39 313	syl	$$⊢\phi \to \left(\log A<1\leftrightarrow A<\mathrm{e}\right)$$
315	312 314	mtbird	$$⊢\phi \to \neg \log A<1$$
316	38 40	lenltd	$$⊢\phi \to \left(1\le \log A\leftrightarrow \neg \log A<1\right)$$
317	315 316	mpbird	$$⊢\phi \to 1\le \log A$$
318		10nn	$$⊢10\in \mathbb{N}$$
319	318	a1i	$$⊢\phi \to 10\in \mathbb{N}$$
320		nnledivrp	$$⊢\left(10\in \mathbb{N}\wedge \log A\in {ℝ}^{+}\right)\to \left(1\le \log A\leftrightarrow \frac{10}{\log A}\le 10\right)$$
321	319 130 320	syl2anc	$$⊢\phi \to \left(1\le \log A\leftrightarrow \frac{10}{\log A}\le 10\right)$$
322	317 321	mpbid	$$⊢\phi \to \frac{10}{\log A}\le 10$$
323	288 287 291 322	leadd1dd	$$⊢\phi \to \left(\frac{10}{\log A}\right)+2{\left(\frac{\log A}{\log 2}\right)}^1\le 10+2{\left(\frac{\log A}{\log 2}\right)}^1$$
324	38 55	gtned	$$⊢\phi \to 2\ne 1$$
325	37 15 1 9 324	relogbcld	$$⊢\phi \to {\log }_{2}A\in ℝ$$
326	325 91	reexpcld	$$⊢\phi \to {{\log }_{2}A}^1\in ℝ$$
327	42 55	jca	$$⊢\phi \to \left(2\in {ℝ}^{+}\wedge 1<2\right)$$
328		logbgt0b	$$⊢\left(A\in {ℝ}^{+}\wedge \left(2\in {ℝ}^{+}\wedge 1<2\right)\right)\to \left(0<{\log }_{2}A\leftrightarrow 1<A\right)$$
329	39 327 328	syl2anc	$$⊢\phi \to \left(0<{\log }_{2}A\leftrightarrow 1<A\right)$$
330	99 329	mpbird	$$⊢\phi \to 0<{\log }_{2}A$$
331	325 330	elrpd	$$⊢\phi \to {\log }_{2}A\in {ℝ}^{+}$$
332	331 239	rpexpcld	$$⊢\phi \to {{\log }_{2}A}^1\in {ℝ}^{+}$$
333	332	rpne0d	$$⊢\phi \to {{\log }_{2}A}^1\ne 0$$
334	287 326 333	redivcld	$$⊢\phi \to \frac{10}{{{\log }_{2}A}^1}\in ℝ$$
335	334 37	readdcld	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2\in ℝ$$
336		sq2	$$⊢2^2=4$$
337	336	a1i	$$⊢\phi \to 2^2=4$$
338	337 6	eqeltrd	$$⊢\phi \to 2^2\in ℝ$$
339	6 338	remulcld	$$⊢\phi \to 42^2\in ℝ$$
340	325	resqcld	$$⊢\phi \to {{\log }_{2}A}^2\in ℝ$$
341	6 340	remulcld	$$⊢\phi \to 4{{\log }_{2}A}^2\in ℝ$$
342	325	recnd	$$⊢\phi \to {\log }_{2}A\in ℂ$$
343	342	exp1d	$$⊢\phi \to {{\log }_{2}A}^1={\log }_{2}A$$
344	343	oveq2d	$$⊢\phi \to \frac{10}{{{\log }_{2}A}^1}=\frac{10}{{\log }_{2}A}$$
345	344	oveq1d	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2=\left(\frac{10}{{\log }_{2}A}\right)+2$$
346	345 335	eqeltrrd	$$⊢\phi \to \left(\frac{10}{{\log }_{2}A}\right)+2\in ℝ$$
347	287	rehalfcld	$$⊢\phi \to \frac{10}{2}\in ℝ$$
348	347 37	readdcld	$$⊢\phi \to \left(\frac{10}{2}\right)+2\in ℝ$$
349	344 334	eqeltrrd	$$⊢\phi \to \frac{10}{{\log }_{2}A}\in ℝ$$
350	287 37 17	redivcld	$$⊢\phi \to \frac{10}{2}\in ℝ$$
351	272	nn0ge0i	$$⊢0\le 10$$
352	351	a1i	$$⊢\phi \to 0\le 10$$
353	42 324 87	relogbexpd	$$⊢\phi \to {\log }_2{2}^2=2$$
354	353	eqcomd	$$⊢\phi \to 2={\log }_2{2}^2$$
355	337	oveq2d	$$⊢\phi \to {\log }_2{2}^2={\log }_{2}4$$
356	354 355	eqtrd	$$⊢\phi \to 2={\log }_{2}4$$
357	37	leidd	$$⊢\phi \to 2\le 2$$
358	87 357 6 8 1 9 2	logblebd	$$⊢\phi \to {\log }_{2}4\le {\log }_{2}A$$
359	356 358	eqbrtrd	$$⊢\phi \to 2\le {\log }_{2}A$$
360	42 331 287 352 359	lediv2ad	$$⊢\phi \to \frac{10}{{\log }_{2}A}\le \frac{10}{2}$$
361	349 350 37 360	leadd1dd	$$⊢\phi \to \left(\frac{10}{{\log }_{2}A}\right)+2\le \left(\frac{10}{2}\right)+2$$
362		1nn	$$⊢1\in \mathbb{N}$$
363		6nn0	$$⊢6\in {\mathbb{N}}_0$$
364		2nn0	$$⊢2\in {\mathbb{N}}_0$$
365	27 364	nn0addcli	$$⊢5+2\in {\mathbb{N}}_0$$
366		5p2e7	$$⊢5+2=7$$
367		7re	$$⊢7\in ℝ$$
368	367 364	nn0addge1i	$$⊢7\le 7+2$$
369		7p2e9	$$⊢7+2=9$$
370	368 369	breqtri	$$⊢7\le 9$$
371	366 370	eqbrtri	$$⊢5+2\le 9$$
372	362 363 365 371	declei	$$⊢5+2\le 16$$
373	372	a1i	$$⊢\phi \to 5+2\le 16$$
374	206 13 274 17	ldiv	$$⊢\phi \to \left(5\cdot 2=10\leftrightarrow 5=\frac{10}{2}\right)$$
375	269 374	mpbid	$$⊢\phi \to 5=\frac{10}{2}$$
376	375	oveq1d	$$⊢\phi \to 5+2=\left(\frac{10}{2}\right)+2$$
377		4t4e16	$$⊢4\cdot 4=16$$
378	377	eqcomi	$$⊢16=4\cdot 4$$
379	378	a1i	$$⊢\phi \to 16=4\cdot 4$$
380	337	eqcomd	$$⊢\phi \to 4=2^2$$
381	380	oveq2d	$$⊢\phi \to 4\cdot 4=42^2$$
382	379 381	eqtrd	$$⊢\phi \to 16=42^2$$
383	373 376 382	3brtr3d	$$⊢\phi \to \left(\frac{10}{2}\right)+2\le 42^2$$
384	346 348 339 361 383	letrd	$$⊢\phi \to \left(\frac{10}{{\log }_{2}A}\right)+2\le 42^2$$
385	345 384	eqbrtrd	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2\le 42^2$$
386	4 6 8	ltled	$$⊢\phi \to 0\le 4$$
387	364	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
388	37 325 387 124 359	leexp1ad	$$⊢\phi \to 2^2\le {{\log }_{2}A}^2$$
389	338 340 6 386 388	lemul2ad	$$⊢\phi \to 42^2\le 4{{\log }_{2}A}^2$$
390	335 339 341 385 389	letrd	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2\le 4{{\log }_{2}A}^2$$
391	37 326	remulcld	$$⊢\phi \to 2{{\log }_{2}A}^1\in ℝ$$
392	391	recnd	$$⊢\phi \to 2{{\log }_{2}A}^1\in ℂ$$
393	326	recnd	$$⊢\phi \to {{\log }_{2}A}^1\in ℂ$$
394	274 392 393 333	divdird	$$⊢\phi \to \frac{10+2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}=\left(\frac{10}{{{\log }_{2}A}^1}\right)+\left(\frac{2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)$$
395	13 393 393 333	divassd	$$⊢\phi \to \frac{2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}=2\left(\frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)$$
396	395	oveq2d	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+\left(\frac{2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)=\left(\frac{10}{{{\log }_{2}A}^1}\right)+2\left(\frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)$$
397	393 333	dividd	$$⊢\phi \to \frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}=1$$
398	397	oveq2d	$$⊢\phi \to 2\left(\frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)=2\cdot 1$$
399	398 180	eqtrd	$$⊢\phi \to 2\left(\frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)=2$$
400	399	oveq2d	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2\left(\frac{{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)=\left(\frac{10}{{{\log }_{2}A}^1}\right)+2$$
401	396 400	eqtrd	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+\left(\frac{2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\right)=\left(\frac{10}{{{\log }_{2}A}^1}\right)+2$$
402	394 401	eqtrd	$$⊢\phi \to \frac{10+2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}=\left(\frac{10}{{{\log }_{2}A}^1}\right)+2$$
403	402	eqcomd	$$⊢\phi \to \left(\frac{10}{{{\log }_{2}A}^1}\right)+2=\frac{10+2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}$$
404		2p1e3	$$⊢2+1=3$$
405	404	a1i	$$⊢\phi \to 2+1=3$$
406	302	recnd	$$⊢\phi \to 3\in ℂ$$
407	406 53 13	subadd2d	$$⊢\phi \to \left(3-1=2\leftrightarrow 2+1=3\right)$$
408	405 407	mpbird	$$⊢\phi \to 3-1=2$$
409	408	eqcomd	$$⊢\phi \to 2=3-1$$
410	409	oveq2d	$$⊢\phi \to {{\log }_{2}A}^2={{\log }_{2}A}^{3-1}$$
411	410	oveq2d	$$⊢\phi \to 4{{\log }_{2}A}^2=4{{\log }_{2}A}^{3-1}$$
412	4 330	gtned	$$⊢\phi \to {\log }_{2}A\ne 0$$
413	342 412 239 296	expsubd	$$⊢\phi \to {{\log }_{2}A}^{3-1}=\frac{{{\log }_{2}A}^3}{{{\log }_{2}A}^1}$$
414	413	oveq2d	$$⊢\phi \to 4{{\log }_{2}A}^{3-1}=4\left(\frac{{{\log }_{2}A}^3}{{{\log }_{2}A}^1}\right)$$
415	411 414	eqtrd	$$⊢\phi \to 4{{\log }_{2}A}^2=4\left(\frac{{{\log }_{2}A}^3}{{{\log }_{2}A}^1}\right)$$
416	217	a1i	$$⊢\phi \to 4\in ℂ$$
417	325 112	reexpcld	$$⊢\phi \to {{\log }_{2}A}^3\in ℝ$$
418	417	recnd	$$⊢\phi \to {{\log }_{2}A}^3\in ℂ$$
419	416 418 393 333	divassd	$$⊢\phi \to \frac{4{{\log }_{2}A}^3}{{{\log }_{2}A}^1}=4\left(\frac{{{\log }_{2}A}^3}{{{\log }_{2}A}^1}\right)$$
420	419	eqcomd	$$⊢\phi \to 4\left(\frac{{{\log }_{2}A}^3}{{{\log }_{2}A}^1}\right)=\frac{4{{\log }_{2}A}^3}{{{\log }_{2}A}^1}$$
421	415 420	eqtrd	$$⊢\phi \to 4{{\log }_{2}A}^2=\frac{4{{\log }_{2}A}^3}{{{\log }_{2}A}^1}$$
422	390 403 421	3brtr3d	$$⊢\phi \to \frac{10+2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\le \frac{4{{\log }_{2}A}^3}{{{\log }_{2}A}^1}$$
423	287 391	readdcld	$$⊢\phi \to 10+2{{\log }_{2}A}^1\in ℝ$$
424	6 417	remulcld	$$⊢\phi \to 4{{\log }_{2}A}^3\in ℝ$$
425	423 424 332	lediv1d	$$⊢\phi \to \left(10+2{{\log }_{2}A}^1\le 4{{\log }_{2}A}^3\leftrightarrow \frac{10+2{{\log }_{2}A}^1}{{{\log }_{2}A}^1}\le \frac{4{{\log }_{2}A}^3}{{{\log }_{2}A}^1}\right)$$
426	422 425	mpbird	$$⊢\phi \to 10+2{{\log }_{2}A}^1\le 4{{\log }_{2}A}^3$$
427	87	uzidd	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 2}$$
428	427 39	jca	$$⊢\phi \to \left(2\in {\mathbb{Z}}_{\ge 2}\wedge A\in {ℝ}^{+}\right)$$
429		relogbval	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge A\in {ℝ}^{+}\right)\to {\log }_{2}A=\frac{\log A}{\log 2}$$
430	428 429	syl	$$⊢\phi \to {\log }_{2}A=\frac{\log A}{\log 2}$$
431	430	oveq1d	$$⊢\phi \to {{\log }_{2}A}^1={\left(\frac{\log A}{\log 2}\right)}^1$$
432	431	oveq2d	$$⊢\phi \to 2{{\log }_{2}A}^1=2{\left(\frac{\log A}{\log 2}\right)}^1$$
433	432	oveq2d	$$⊢\phi \to 10+2{{\log }_{2}A}^1=10+2{\left(\frac{\log A}{\log 2}\right)}^1$$
434	430	oveq1d	$$⊢\phi \to {{\log }_{2}A}^3={\left(\frac{\log A}{\log 2}\right)}^3$$
435	12 18 26 112	expdivd	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^3=\frac{{\log A}^3}{{\log 2}^3}$$
436	434 435	eqtrd	$$⊢\phi \to {{\log }_{2}A}^3=\frac{{\log A}^3}{{\log 2}^3}$$
437	436	oveq2d	$$⊢\phi \to 4{{\log }_{2}A}^3=4\left(\frac{{\log A}^3}{{\log 2}^3}\right)$$
438	426 433 437	3brtr3d	$$⊢\phi \to 10+2{\left(\frac{\log A}{\log 2}\right)}^1\le 4\left(\frac{{\log A}^3}{{\log 2}^3}\right)$$
439	292 293 299 323 438	letrd	$$⊢\phi \to \left(\frac{10}{\log A}\right)+2{\left(\frac{\log A}{\log 2}\right)}^1\le 4\left(\frac{{\log A}^3}{{\log 2}^3}\right)$$
440	12	exp1d	$$⊢\phi \to {\log A}^1=\log A$$
441	440	eqcomd	$$⊢\phi \to \log A={\log A}^1$$
442	441	oveq2d	$$⊢\phi \to \frac{10}{\log A}=\frac{10}{{\log A}^1}$$
443	13 156 281 282	divassd	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^1}=2\left(\frac{{\log A}^1}{{\log 2}^1}\right)$$
444	12 18 26 91	expdivd	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^1=\frac{{\log A}^1}{{\log 2}^1}$$
445	444	eqcomd	$$⊢\phi \to \frac{{\log A}^1}{{\log 2}^1}={\left(\frac{\log A}{\log 2}\right)}^1$$
446	445	oveq2d	$$⊢\phi \to 2\left(\frac{{\log A}^1}{{\log 2}^1}\right)=2{\left(\frac{\log A}{\log 2}\right)}^1$$
447	443 446	eqtrd	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^1}=2{\left(\frac{\log A}{\log 2}\right)}^1$$
448	447	eqcomd	$$⊢\phi \to 2{\left(\frac{\log A}{\log 2}\right)}^1=\frac{2{\log A}^1}{{\log 2}^1}$$
449	442 448	oveq12d	$$⊢\phi \to \left(\frac{10}{\log A}\right)+2{\left(\frac{\log A}{\log 2}\right)}^1=\left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)$$
450	113	recnd	$$⊢\phi \to {\log A}^3\in ℂ$$
451	18 112	expcld	$$⊢\phi \to {\log 2}^3\in ℂ$$
452	416 450 451 297	divassd	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^3}=4\left(\frac{{\log A}^3}{{\log 2}^3}\right)$$
453	452	eqcomd	$$⊢\phi \to 4\left(\frac{{\log A}^3}{{\log 2}^3}\right)=\frac{4{\log A}^3}{{\log 2}^3}$$
454	439 449 453	3brtr3d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)\le \frac{4{\log A}^3}{{\log 2}^3}$$
455	285 454	eqbrtrd	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1\le \frac{4{\log A}^3}{{\log 2}^3}$$
456	281 282	dividd	$$⊢\phi \to \frac{{\log 2}^1}{{\log 2}^1}=1$$
457	456	eqcomd	$$⊢\phi \to 1=\frac{{\log 2}^1}{{\log 2}^1}$$
458	457	oveq2d	$$⊢\phi \to \left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1=\left(\frac{2{\log A}^1}{{\log 2}^1}\right)\left(\frac{{\log 2}^1}{{\log 2}^1}\right)$$
459	277 281 281 281 282 282	divmuldivd	$$⊢\phi \to \left(\frac{2{\log A}^1}{{\log 2}^1}\right)\left(\frac{{\log 2}^1}{{\log 2}^1}\right)=\frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}$$
460	458 459	eqtrd	$$⊢\phi \to \left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1=\frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}$$
461	460	oveq2d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1}{{\log 2}^1}\right)\cdot 1=\left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}\right)$$
462	416 450	mulcld	$$⊢\phi \to 4{\log A}^3\in ℂ$$
463	462 451 297	divcld	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^3}\in ℂ$$
464	463	mulid1d	$$⊢\phi \to \left(\frac{4{\log A}^3}{{\log 2}^3}\right)\cdot 1=\frac{4{\log A}^3}{{\log 2}^3}$$
465	464	eqcomd	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^3}=\left(\frac{4{\log A}^3}{{\log 2}^3}\right)\cdot 1$$
466	455 461 465	3brtr3d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}\right)\le \left(\frac{4{\log A}^3}{{\log 2}^3}\right)\cdot 1$$
467	274 156 247	divcld	$$⊢\phi \to \frac{10}{{\log A}^1}\in ℂ$$
468	467	mulid1d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)\cdot 1=\frac{10}{{\log A}^1}$$
469	468	eqcomd	$$⊢\phi \to \frac{10}{{\log A}^1}=\left(\frac{10}{{\log A}^1}\right)\cdot 1$$
470	18 26	dividd	$$⊢\phi \to \frac{\log 2}{\log 2}=1$$
471	470	eqcomd	$$⊢\phi \to 1=\frac{\log 2}{\log 2}$$
472	471	oveq2d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)\cdot 1=\left(\frac{10}{{\log A}^1}\right)\left(\frac{\log 2}{\log 2}\right)$$
473	469 472	eqtrd	$$⊢\phi \to \frac{10}{{\log A}^1}=\left(\frac{10}{{\log A}^1}\right)\left(\frac{\log 2}{\log 2}\right)$$
474	274 156 18 18 247 26	divmuldivd	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)\left(\frac{\log 2}{\log 2}\right)=\frac{10\log 2}{{\log A}^1\log 2}$$
475	473 474	eqtrd	$$⊢\phi \to \frac{10}{{\log A}^1}=\frac{10\log 2}{{\log A}^1\log 2}$$
476	18	exp1d	$$⊢\phi \to {\log 2}^1=\log 2$$
477	476	oveq2d	$$⊢\phi \to 2{\log A}^1{\log 2}^1=2{\log A}^1\log 2$$
478		df-2	$$⊢2=1+1$$
479	478	a1i	$$⊢\phi \to 2=1+1$$
480	479	oveq2d	$$⊢\phi \to {\log 2}^2={\log 2}^{1+1}$$
481	18 91 91	expaddd	$$⊢\phi \to {\log 2}^{1+1}={\log 2}^1{\log 2}^1$$
482	480 481	eqtrd	$$⊢\phi \to {\log 2}^2={\log 2}^1{\log 2}^1$$
483	482	eqcomd	$$⊢\phi \to {\log 2}^1{\log 2}^1={\log 2}^2$$
484	477 483	oveq12d	$$⊢\phi \to \frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}=\frac{2{\log A}^1\log 2}{{\log 2}^2}$$
485	475 484	oveq12d	$$⊢\phi \to \left(\frac{10}{{\log A}^1}\right)+\left(\frac{2{\log A}^1{\log 2}^1}{{\log 2}^1{\log 2}^1}\right)=\left(\frac{10\log 2}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1\log 2}{{\log 2}^2}\right)$$
486	476	eqcomd	$$⊢\phi \to \log 2={\log 2}^1$$
487	486	oveq2d	$$⊢\phi \to \frac{\log 2}{\log 2}=\frac{\log 2}{{\log 2}^1}$$
488	471 487	eqtrd	$$⊢\phi \to 1=\frac{\log 2}{{\log 2}^1}$$
489	488	oveq2d	$$⊢\phi \to \left(\frac{4{\log A}^3}{{\log 2}^3}\right)\cdot 1=\left(\frac{4{\log A}^3}{{\log 2}^3}\right)\left(\frac{\log 2}{{\log 2}^1}\right)$$
490	476 18	eqeltrd	$$⊢\phi \to {\log 2}^1\in ℂ$$
491	476 26	eqnetrd	$$⊢\phi \to {\log 2}^1\ne 0$$
492	462 451 18 490 297 491	divmuldivd	$$⊢\phi \to \left(\frac{4{\log A}^3}{{\log 2}^3}\right)\left(\frac{\log 2}{{\log 2}^1}\right)=\frac{4{\log A}^3\log 2}{{\log 2}^3{\log 2}^1}$$
493	489 492	eqtrd	$$⊢\phi \to \left(\frac{4{\log A}^3}{{\log 2}^3}\right)\cdot 1=\frac{4{\log A}^3\log 2}{{\log 2}^3{\log 2}^1}$$
494	466 485 493	3brtr3d	$$⊢\phi \to \left(\frac{10\log 2}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1\log 2}{{\log 2}^2}\right)\le \frac{4{\log A}^3\log 2}{{\log 2}^3{\log 2}^1}$$
495	156 18	mulcld	$$⊢\phi \to {\log A}^1\log 2\in ℂ$$
496	156 18 247 26	mulne0d	$$⊢\phi \to {\log A}^1\log 2\ne 0$$
497	274 18 495 496	div23d	$$⊢\phi \to \frac{10\log 2}{{\log A}^1\log 2}=\left(\frac{10}{{\log A}^1\log 2}\right)\log 2$$
498	277 18 155 88	div23d	$$⊢\phi \to \frac{2{\log A}^1\log 2}{{\log 2}^2}=\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\log 2$$
499	497 498	oveq12d	$$⊢\phi \to \left(\frac{10\log 2}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1\log 2}{{\log 2}^2}\right)=\left(\frac{10}{{\log A}^1\log 2}\right)\log 2+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\log 2$$
500	62	a1i	$$⊢\phi \to 4=3+1$$
501	500	oveq2d	$$⊢\phi \to {\log 2}^4={\log 2}^{3+1}$$
502	18 91 112	expaddd	$$⊢\phi \to {\log 2}^{3+1}={\log 2}^3{\log 2}^1$$
503	501 502	eqtrd	$$⊢\phi \to {\log 2}^4={\log 2}^3{\log 2}^1$$
504	503	eqcomd	$$⊢\phi \to {\log 2}^3{\log 2}^1={\log 2}^4$$
505	504	oveq2d	$$⊢\phi \to \frac{4{\log A}^3\log 2}{{\log 2}^3{\log 2}^1}=\frac{4{\log A}^3\log 2}{{\log 2}^4}$$
506	494 499 505	3brtr3d	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2}\right)\log 2+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\log 2\le \frac{4{\log A}^3\log 2}{{\log 2}^4}$$
507	92 43	remulcld	$$⊢\phi \to {\log A}^1\log 2\in ℝ$$
508	287 507 496	redivcld	$$⊢\phi \to \frac{10}{{\log A}^1\log 2}\in ℝ$$
509	508	recnd	$$⊢\phi \to \frac{10}{{\log A}^1\log 2}\in ℂ$$
510	509 278 18	adddird	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\right)\log 2=\left(\frac{10}{{\log A}^1\log 2}\right)\log 2+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\log 2$$
511	510	eqcomd	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2}\right)\log 2+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\log 2=\left(\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\right)\log 2$$
512	18 26 212	expne0d	$$⊢\phi \to {\log 2}^4\ne 0$$
513	462 18 117 512	div23d	$$⊢\phi \to \frac{4{\log A}^3\log 2}{{\log 2}^4}=\left(\frac{4{\log A}^3}{{\log 2}^4}\right)\log 2$$
514	506 511 513	3brtr3d	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\right)\log 2\le \left(\frac{4{\log A}^3}{{\log 2}^4}\right)\log 2$$
515	37 92	remulcld	$$⊢\phi \to 2{\log A}^1\in ℝ$$
516	515 85 88	redivcld	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^2}\in ℝ$$
517	508 516	readdcld	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\in ℝ$$
518	114 115 120	redivcld	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^4}\in ℝ$$
519	517 518 135	lemul1d	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\le \frac{4{\log A}^3}{{\log 2}^4}\leftrightarrow \left(\left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\right)\log 2\le \left(\frac{4{\log A}^3}{{\log 2}^4}\right)\log 2\right)$$
520	514 519	mpbird	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2}\right)+\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\le \frac{4{\log A}^3}{{\log 2}^4}$$
521	280 520	eqbrtrd	$$⊢\phi \to \left(\frac{10\cdot 1}{{\log A}^1\log 2}\right)+1\left(\frac{2{\log A}^1}{{\log 2}^2}\right)\le \frac{4{\log A}^3}{{\log 2}^4}$$
522	274 53 495 496	divassd	$$⊢\phi \to \frac{10\cdot 1}{{\log A}^1\log 2}=10\left(\frac{1}{{\log A}^1\log 2}\right)$$
523	53 277 155 88	div12d	$$⊢\phi \to 1\left(\frac{2{\log A}^1}{{\log 2}^2}\right)=2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)$$
524	522 523	oveq12d	$$⊢\phi \to \left(\frac{10\cdot 1}{{\log A}^1\log 2}\right)+1\left(\frac{2{\log A}^1}{{\log 2}^2}\right)=10\left(\frac{1}{{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)$$
525	462	mulid1d	$$⊢\phi \to 4{\log A}^3\cdot 1=4{\log A}^3$$
526	525	eqcomd	$$⊢\phi \to 4{\log A}^3=4{\log A}^3\cdot 1$$
527	526	oveq1d	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^4}=\frac{4{\log A}^3\cdot 1}{{\log 2}^4}$$
528	521 524 527	3brtr3d	$$⊢\phi \to 10\left(\frac{1}{{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)\le \frac{4{\log A}^3\cdot 1}{{\log 2}^4}$$
529	3 11	dividd	$$⊢\phi \to \frac{A}{A}=1$$
530	529	eqcomd	$$⊢\phi \to 1=\frac{A}{A}$$
531	530	oveq1d	$$⊢\phi \to \frac{1}{{\log A}^1\log 2}=\frac{\frac{A}{A}}{{\log A}^1\log 2}$$
532	3 3 495 11 496	divdiv1d	$$⊢\phi \to \frac{\frac{A}{A}}{{\log A}^1\log 2}=\frac{A}{A{\log A}^1\log 2}$$
533	531 532	eqtrd	$$⊢\phi \to \frac{1}{{\log A}^1\log 2}=\frac{A}{A{\log A}^1\log 2}$$
534	533	oveq2d	$$⊢\phi \to 10\left(\frac{1}{{\log A}^1\log 2}\right)=10\left(\frac{A}{A{\log A}^1\log 2}\right)$$
535		eqidd	$$⊢\phi \to 2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)=2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)$$
536	530	oveq1d	$$⊢\phi \to \frac{1}{{\log 2}^2}=\frac{\frac{A}{A}}{{\log 2}^2}$$
537	536	oveq2d	$$⊢\phi \to 2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)=2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)$$
538	535 537	eqtrd	$$⊢\phi \to 2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)=2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)$$
539	534 538	oveq12d	$$⊢\phi \to 10\left(\frac{1}{{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{1}{{\log 2}^2}\right)=10\left(\frac{A}{A{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)$$
540	462 53 117 512	divassd	$$⊢\phi \to \frac{4{\log A}^3\cdot 1}{{\log 2}^4}=4{\log A}^3\left(\frac{1}{{\log 2}^4}\right)$$
541	528 539 540	3brtr3d	$$⊢\phi \to 10\left(\frac{A}{A{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)\le 4{\log A}^3\left(\frac{1}{{\log 2}^4}\right)$$
542	3 495	mulcomd	$$⊢\phi \to A{\log A}^1\log 2={\log A}^1\log 2A$$
543	156 18 3	mulassd	$$⊢\phi \to {\log A}^1\log 2A={\log A}^1\log 2A$$
544	542 543	eqtrd	$$⊢\phi \to A{\log A}^1\log 2={\log A}^1\log 2A$$
545	544	oveq2d	$$⊢\phi \to \frac{A}{A{\log A}^1\log 2}=\frac{A}{{\log A}^1\log 2A}$$
546	545	oveq2d	$$⊢\phi \to 10\left(\frac{A}{A{\log A}^1\log 2}\right)=10\left(\frac{A}{{\log A}^1\log 2A}\right)$$
547	3 3 155 11 88	divdiv1d	$$⊢\phi \to \frac{\frac{A}{A}}{{\log 2}^2}=\frac{A}{A{\log 2}^2}$$
548	3 155	mulcomd	$$⊢\phi \to A{\log 2}^2={\log 2}^{2}A$$
549	548	oveq2d	$$⊢\phi \to \frac{A}{A{\log 2}^2}=\frac{A}{{\log 2}^{2}A}$$
550	547 549	eqtrd	$$⊢\phi \to \frac{\frac{A}{A}}{{\log 2}^2}=\frac{A}{{\log 2}^{2}A}$$
551	550	oveq2d	$$⊢\phi \to 2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)=2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)$$
552	546 551	oveq12d	$$⊢\phi \to 10\left(\frac{A}{A{\log A}^1\log 2}\right)+2{\log A}^1\left(\frac{\frac{A}{A}}{{\log 2}^2}\right)=10\left(\frac{A}{{\log A}^1\log 2A}\right)+2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)$$
553		eqidd	$$⊢\phi \to \frac{1}{{\log 2}^4}=\frac{1}{{\log 2}^4}$$
554	530	oveq1d	$$⊢\phi \to \frac{1}{{\log 2}^4}=\frac{\frac{A}{A}}{{\log 2}^4}$$
555	553 554	eqtrd	$$⊢\phi \to \frac{1}{{\log 2}^4}=\frac{\frac{A}{A}}{{\log 2}^4}$$
556	555	oveq2d	$$⊢\phi \to 4{\log A}^3\left(\frac{1}{{\log 2}^4}\right)=4{\log A}^3\left(\frac{\frac{A}{A}}{{\log 2}^4}\right)$$
557	541 552 556	3brtr3d	$$⊢\phi \to 10\left(\frac{A}{{\log A}^1\log 2A}\right)+2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)\le 4{\log A}^3\left(\frac{\frac{A}{A}}{{\log 2}^4}\right)$$
558	156 261	mulcld	$$⊢\phi \to {\log A}^1\log 2A\in ℂ$$
559	156 261 247 262	mulne0d	$$⊢\phi \to {\log A}^1\log 2A\ne 0$$
560	274 558 3 559	div32d	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2A}\right)A=10\left(\frac{A}{{\log A}^1\log 2A}\right)$$
561	560	eqcomd	$$⊢\phi \to 10\left(\frac{A}{{\log A}^1\log 2A}\right)=\left(\frac{10}{{\log A}^1\log 2A}\right)A$$
562	155 3	mulcld	$$⊢\phi \to {\log 2}^{2}A\in ℂ$$
563	155 3 88 11	mulne0d	$$⊢\phi \to {\log 2}^{2}A\ne 0$$
564	277 562 3 563	div32d	$$⊢\phi \to \left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A=2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)$$
565	564	eqcomd	$$⊢\phi \to 2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)=\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A$$
566	561 565	oveq12d	$$⊢\phi \to 10\left(\frac{A}{{\log A}^1\log 2A}\right)+2{\log A}^1\left(\frac{A}{{\log 2}^{2}A}\right)=\left(\frac{10}{{\log A}^1\log 2A}\right)A+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A$$
567	3 3 117 11 512	divdiv1d	$$⊢\phi \to \frac{\frac{A}{A}}{{\log 2}^4}=\frac{A}{A{\log 2}^4}$$
568	3 117	mulcomd	$$⊢\phi \to A{\log 2}^4={\log 2}^{4}A$$
569	568	oveq2d	$$⊢\phi \to \frac{A}{A{\log 2}^4}=\frac{A}{{\log 2}^{4}A}$$
570	567 569	eqtrd	$$⊢\phi \to \frac{\frac{A}{A}}{{\log 2}^4}=\frac{A}{{\log 2}^{4}A}$$
571	570	oveq2d	$$⊢\phi \to 4{\log A}^3\left(\frac{\frac{A}{A}}{{\log 2}^4}\right)=4{\log A}^3\left(\frac{A}{{\log 2}^{4}A}\right)$$
572	557 566 571	3brtr3d	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2A}\right)A+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A\le 4{\log A}^3\left(\frac{A}{{\log 2}^{4}A}\right)$$
573	43 1	remulcld	$$⊢\phi \to \log 2A\in ℝ$$
574	92 573	remulcld	$$⊢\phi \to {\log A}^1\log 2A\in ℝ$$
575	287 574 559	redivcld	$$⊢\phi \to \frac{10}{{\log A}^1\log 2A}\in ℝ$$
576	575	recnd	$$⊢\phi \to \frac{10}{{\log A}^1\log 2A}\in ℂ$$
577	157 94	eqeltrrd	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^{2}A}\in ℝ$$
578	577	recnd	$$⊢\phi \to \frac{2{\log A}^1}{{\log 2}^{2}A}\in ℂ$$
579	576 578 3	adddird	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\right)A=\left(\frac{10}{{\log A}^1\log 2A}\right)A+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A$$
580	579	eqcomd	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2A}\right)A+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)A=\left(\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\right)A$$
581	12 112	expcld	$$⊢\phi \to {\log A}^3\in ℂ$$
582	416 581	mulcld	$$⊢\phi \to 4{\log A}^3\in ℂ$$
583	117 3	mulcld	$$⊢\phi \to {\log 2}^{4}A\in ℂ$$
584	117 3 512 11	mulne0d	$$⊢\phi \to {\log 2}^{4}A\ne 0$$
585	582 583 3 584	div32d	$$⊢\phi \to \left(\frac{4{\log A}^3}{{\log 2}^{4}A}\right)A=4{\log A}^3\left(\frac{A}{{\log 2}^{4}A}\right)$$
586	585	eqcomd	$$⊢\phi \to 4{\log A}^3\left(\frac{A}{{\log 2}^{4}A}\right)=\left(\frac{4{\log A}^3}{{\log 2}^{4}A}\right)A$$
587	572 580 586	3brtr3d	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\right)A\le \left(\frac{4{\log A}^3}{{\log 2}^{4}A}\right)A$$
588	575 577	readdcld	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\in ℝ$$
589	588 122 39	lemul1d	$$⊢\phi \to \left(\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}\leftrightarrow \left(\left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\right)A\le \left(\frac{4{\log A}^3}{{\log 2}^{4}A}\right)A\right)$$
590	587 589	mpbird	$$⊢\phi \to \left(\frac{10}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
591	271 590	eqbrtrd	$$⊢\phi \to \left(\frac{5\cdot 2}{{\log A}^1\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
592	267 591	eqbrtrd	$$⊢\phi \to \left(\frac{5}{{\log A}^1}\right)\left(\frac{2\cdot 1}{\log 2A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
593	259 592	eqbrtrd	$$⊢\phi \to \left(\frac{5\cdot 1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{1}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
594	254 593	eqbrtrd	$$⊢\phi \to 5\left(\frac{1}{{\log A}^1}\right)\left(\frac{2}{\log 2}\right)\left(\frac{\frac{{\log 2}^5}{{\log 2}^5}}{A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
595	246 594	eqbrtrd	$$⊢\phi \to 5{\log A}^{-1}\left(\frac{2}{\log 2}\right)\left(\frac{{\log 2}^5}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
596	238 595	eqbrtrd	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
597	211 596	eqbrtrd	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log A}^5}\right)\left(\frac{2{\log 2}^5}{\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
598	205 597	eqbrtrd	$$⊢\phi \to \left(\frac{5{\log A}^{4}2{\log 2}^5}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
599	198 598	eqbrtrd	$$⊢\phi \to \left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
600	192 599	eqbrtrd	$$⊢\phi \to \left(\frac{2{\log 2}^{5}5{\log A}^4}{{\log A}^5\log 2{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
601	189 600	eqbrtrd	$$⊢\phi \to \left(\frac{2{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
602	184 601	eqbrtrd	$$⊢\phi \to \left(\frac{2\cdot 1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
603	179 602	eqbrtrd	$$⊢\phi \to \left(\frac{21{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
604	174 603	eqbrtrd	$$⊢\phi \to 2\left(\frac{1{\log 2}^5}{{\log A}^5\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
605	170 604	eqbrtrd	$$⊢\phi \to 2\left(\frac{1}{\frac{{\log A}^5\log 2}{{\log 2}^5}}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2{\log A}^1}{{\log 2}^{2}A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
606	158 605	eqbrtrd	$$⊢\phi \to 2\left(\frac{1}{\left(\frac{{\log A}^5}{{\log 2}^5}\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
607	95 111 122 149 606	letrd	$$⊢\phi \to 2\left(\frac{1}{\left(\left(\frac{{\log A}^5}{{\log 2}^5}\right)+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
608	35 607	eqbrtrd	$$⊢\phi \to 2\left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)\le \frac{4{\log A}^3}{{\log 2}^{4}A}$$
609	427 39 429	syl2anc	$$⊢\phi \to {\log }_{2}A=\frac{\log A}{\log 2}$$
610	609	eqcomd	$$⊢\phi \to \frac{\log A}{\log 2}={\log }_{2}A$$
611	610	oveq1d	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^5={{\log }_{2}A}^5$$
612	611	oveq1d	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^5+1={{\log }_{2}A}^5+1$$
613	612	oveq1d	$$⊢\phi \to \left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2=\left({{\log }_{2}A}^5+1\right)\log 2$$
614	613	oveq2d	$$⊢\phi \to \frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}=\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}$$
615		5cn	$$⊢5\in ℂ$$
616	615	a1i	$$⊢\phi \to 5\in ℂ$$
617	616 207	mulcld	$$⊢\phi \to 5{\log A}^4\in ℂ$$
618	617	mulid1d	$$⊢\phi \to 5{\log A}^4\cdot 1=5{\log A}^4$$
619	618	eqcomd	$$⊢\phi \to 5{\log A}^4=5{\log A}^4\cdot 1$$
620		eqidd	$$⊢\phi \to {\log 2}^{5}A={\log 2}^{5}A$$
621		df-5	$$⊢5=4+1$$
622	621	a1i	$$⊢\phi \to 5=4+1$$
623	622	oveq2d	$$⊢\phi \to {\log 2}^5={\log 2}^{4+1}$$
624	18 91 77	expaddd	$$⊢\phi \to {\log 2}^{4+1}={\log 2}^4{\log 2}^1$$
625	623 624	eqtrd	$$⊢\phi \to {\log 2}^5={\log 2}^4{\log 2}^1$$
626	476	oveq2d	$$⊢\phi \to {\log 2}^4{\log 2}^1={\log 2}^4\log 2$$
627	625 626	eqtrd	$$⊢\phi \to {\log 2}^5={\log 2}^4\log 2$$
628	627	oveq1d	$$⊢\phi \to {\log 2}^{5}A={\log 2}^4\log 2A$$
629	620 628	eqtrd	$$⊢\phi \to {\log 2}^{5}A={\log 2}^4\log 2A$$
630	117 18 3	mulassd	$$⊢\phi \to {\log 2}^4\log 2A={\log 2}^4\log 2A$$
631	629 630	eqtrd	$$⊢\phi \to {\log 2}^{5}A={\log 2}^4\log 2A$$
632	18 3	mulcomd	$$⊢\phi \to \log 2A=A\log 2$$
633	632	oveq2d	$$⊢\phi \to {\log 2}^4\log 2A={\log 2}^{4}A\log 2$$
634	631 633	eqtrd	$$⊢\phi \to {\log 2}^{5}A={\log 2}^{4}A\log 2$$
635	619 634	oveq12d	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=\frac{5{\log A}^4\cdot 1}{{\log 2}^{4}A\log 2}$$
636	3 18	mulcld	$$⊢\phi \to A\log 2\in ℂ$$
637	3 18 11 26	mulne0d	$$⊢\phi \to A\log 2\ne 0$$
638	186 117 53 636 120 637	divmuldivd	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)=\frac{5{\log A}^4\cdot 1}{{\log 2}^{4}A\log 2}$$
639	638	eqcomd	$$⊢\phi \to \frac{5{\log A}^4\cdot 1}{{\log 2}^{4}A\log 2}=\left(\frac{5{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)$$
640	635 639	eqtrd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=\left(\frac{5{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)$$
641	206 207 117 120	divassd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^4}=5\left(\frac{{\log A}^4}{{\log 2}^4}\right)$$
642	641	oveq1d	$$⊢\phi \to \left(\frac{5{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)=5\left(\frac{{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)$$
643	640 642	eqtrd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=5\left(\frac{{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)$$
644	12 18 26 77	expdivd	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^4=\frac{{\log A}^4}{{\log 2}^4}$$
645	644	eqcomd	$$⊢\phi \to \frac{{\log A}^4}{{\log 2}^4}={\left(\frac{\log A}{\log 2}\right)}^4$$
646	645	oveq2d	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log 2}^4}\right)=5{\left(\frac{\log A}{\log 2}\right)}^4$$
647	646	oveq1d	$$⊢\phi \to 5\left(\frac{{\log A}^4}{{\log 2}^4}\right)\left(\frac{1}{A\log 2}\right)=5{\left(\frac{\log A}{\log 2}\right)}^4\left(\frac{1}{A\log 2}\right)$$
648	643 647	eqtrd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=5{\left(\frac{\log A}{\log 2}\right)}^4\left(\frac{1}{A\log 2}\right)$$
649	610	oveq1d	$$⊢\phi \to {\left(\frac{\log A}{\log 2}\right)}^4={{\log }_{2}A}^4$$
650	649	oveq2d	$$⊢\phi \to 5{\left(\frac{\log A}{\log 2}\right)}^4=5{{\log }_{2}A}^4$$
651	650	oveq1d	$$⊢\phi \to 5{\left(\frac{\log A}{\log 2}\right)}^4\left(\frac{1}{A\log 2}\right)=5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)$$
652	648 651	eqtrd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)$$
653	342 77	expcld	$$⊢\phi \to {{\log }_{2}A}^4\in ℂ$$
654	616 653	mulcld	$$⊢\phi \to 5{{\log }_{2}A}^4\in ℂ$$
655	39	rpne0d	$$⊢\phi \to A\ne 0$$
656	3 18 655 26	mulne0d	$$⊢\phi \to A\log 2\ne 0$$
657	636 656	reccld	$$⊢\phi \to \frac{1}{A\log 2}\in ℂ$$
658	654 657	mulcld	$$⊢\phi \to 5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)\in ℂ$$
659	658	addid1d	$$⊢\phi \to 5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0=5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)$$
660	659	eqcomd	$$⊢\phi \to 5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)=5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0$$
661	652 660	eqtrd	$$⊢\phi \to \frac{5{\log A}^4}{{\log 2}^{5}A}=5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0$$
662	614 661	oveq12d	$$⊢\phi \to \left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=\left(\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}\right)\left(5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0\right)$$
663	662	oveq2d	$$⊢\phi \to 2\left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)=2\left(\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}\right)\left(5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0\right)$$
664		1e2m1	$$⊢1=2-1$$
665	664	a1i	$$⊢\phi \to 1=2-1$$
666	665	oveq2d	$$⊢\phi \to {\log A}^1={\log A}^{2-1}$$
667	666	oveq1d	$$⊢\phi \to \frac{{\log A}^1}{A}=\frac{{\log A}^{2-1}}{A}$$
668	667	oveq2d	$$⊢\phi \to \left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)=\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^{2-1}}{A}\right)$$
669	663 668	oveq12d	$$⊢\phi \to 2\left(\frac{1}{\left({\left(\frac{\log A}{\log 2}\right)}^5+1\right)\log 2}\right)\left(\frac{5{\log A}^4}{{\log 2}^{5}A}\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^1}{A}\right)=2\left(\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}\right)\left(5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^{2-1}}{A}\right)$$
670		4cn	$$⊢4\in ℂ$$
671	670	a1i	$$⊢\phi \to 4\in ℂ$$
672	671 117 581 3 120 655	divmuldivd	$$⊢\phi \to \left(\frac{4}{{\log 2}^4}\right)\left(\frac{{\log A}^3}{A}\right)=\frac{4{\log A}^3}{{\log 2}^{4}A}$$
673	672	eqcomd	$$⊢\phi \to \frac{4{\log A}^3}{{\log 2}^{4}A}=\left(\frac{4}{{\log 2}^4}\right)\left(\frac{{\log A}^3}{A}\right)$$
674	608 669 673	3brtr3d	$$⊢\phi \to 2\left(\frac{1}{\left({{\log }_{2}A}^5+1\right)\log 2}\right)\left(5{{\log }_{2}A}^4\left(\frac{1}{A\log 2}\right)+0\right)+\left(\frac{2}{{\log 2}^2}\right)\left(\frac{{\log A}^{2-1}}{A}\right)\le \left(\frac{4}{{\log 2}^4}\right)\left(\frac{{\log A}^3}{A}\right)$$