Theorem aks4d1p1p4

Description: Technical step for inequality. The hard work is in to prove the final hypothesis. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p4.1	$$⊢\phi \to N\in \mathbb{N}$$
	aks4d1p1p4.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p1p4.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p1p4.4	$$⊢\phi \to 3\le N$$
	aks4d1p1p4.5	$$⊢C={\log }_2\left({{\log }_{2}N}^5+1\right)$$
	aks4d1p1p4.6	$$⊢D={{\log }_{2}N}^2$$
	aks4d1p1p4.7	$$⊢E={{\log }_{2}N}^4$$
	aks4d1p1p4.8	$$⊢\phi \to 2C+D\le E$$
Assertion	aks4d1p1p4	$$⊢\phi \to A<2^B$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p4.1	$$⊢\phi \to N\in \mathbb{N}$$
2		aks4d1p1p4.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p1p4.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		aks4d1p1p4.4	$$⊢\phi \to 3\le N$$
5		aks4d1p1p4.5	$$⊢C={\log }_2\left({{\log }_{2}N}^5+1\right)$$
6		aks4d1p1p4.6	$$⊢D={{\log }_{2}N}^2$$
7		aks4d1p1p4.7	$$⊢E={{\log }_{2}N}^4$$
8		aks4d1p1p4.8	$$⊢\phi \to 2C+D\le E$$
9	1	nnred	$$⊢\phi \to N\in ℝ$$
10		2re	$$⊢2\in ℝ$$
11	10	a1i	$$⊢\phi \to 2\in ℝ$$
12		2pos	$$⊢0<2$$
13	12	a1i	$$⊢\phi \to 0<2$$
14	1	nngt0d	$$⊢\phi \to 0<N$$
15		1red	$$⊢\phi \to 1\in ℝ$$
16		1lt2	$$⊢1<2$$
17	16	a1i	$$⊢\phi \to 1<2$$
18	15 17	ltned	$$⊢\phi \to 1\ne 2$$
19	18	necomd	$$⊢\phi \to 2\ne 1$$
20	11 13 9 14 19	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
21		5nn0	$$⊢5\in {\mathbb{N}}_0$$
22	21	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
23	20 22	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
24		ceilcl	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
25	23 24	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
26	25	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
27	3	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
28	27	eleq1d	$$⊢\phi \to \left(B\in ℝ\leftrightarrow ⌈{{\log }_{2}N}^5⌉\in ℝ\right)$$
29	26 28	mpbird	$$⊢\phi \to B\in ℝ$$
30		0red	$$⊢\phi \to 0\in ℝ$$
31		7re	$$⊢7\in ℝ$$
32	31	a1i	$$⊢\phi \to 7\in ℝ$$
33		7pos	$$⊢0<7$$
34	33	a1i	$$⊢\phi \to 0<7$$
35	9 4	3lexlogpow5ineq3	$$⊢\phi \to 7<{{\log }_{2}N}^5$$
36	32 23 35	ltled	$$⊢\phi \to 7\le {{\log }_{2}N}^5$$
37		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
38	23 37	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
39	38 27	breqtrrd	$$⊢\phi \to {{\log }_{2}N}^5\le B$$
40	32 23 29 36 39	letrd	$$⊢\phi \to 7\le B$$
41	30 32 29 34 40	ltletrd	$$⊢\phi \to 0<B$$
42	11 13 29 41 19	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
43	42	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
44	30 15	readdcld	$$⊢\phi \to 0+1\in ℝ$$
45	43	zred	$$⊢\phi \to ⌊{\log }_{2}B⌋\in ℝ$$
46	45 15	readdcld	$$⊢\phi \to ⌊{\log }_{2}B⌋+1\in ℝ$$
47	11 13 11 13 19	relogbcld	$$⊢\phi \to {\log }_{2}2\in ℝ$$
48	15	leidd	$$⊢\phi \to 1\le 1$$
49		1cnd	$$⊢\phi \to 1\in ℂ$$
50	49	addid2d	$$⊢\phi \to 0+1=1$$
51	11	recnd	$$⊢\phi \to 2\in ℂ$$
52	30 13	gtned	$$⊢\phi \to 2\ne 0$$
53		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
54	51 52 19 53	syl3anc	$$⊢\phi \to {\log }_{2}2=1$$
55	54	eqcomd	$$⊢\phi \to 1={\log }_{2}2$$
56	55	eqcomd	$$⊢\phi \to {\log }_{2}2=1$$
57	50 56	breq12d	$$⊢\phi \to \left(0+1\le {\log }_{2}2\leftrightarrow 1\le 1\right)$$
58	48 57	mpbird	$$⊢\phi \to 0+1\le {\log }_{2}2$$
59		5re	$$⊢5\in ℝ$$
60	59	a1i	$$⊢\phi \to 5\in ℝ$$
61	11 60	readdcld	$$⊢\phi \to 2+5\in ℝ$$
62	10 21	nn0addge1i	$$⊢2\le 2+5$$
63	62	a1i	$$⊢\phi \to 2\le 2+5$$
64	10	recni	$$⊢2\in ℂ$$
65		5cn	$$⊢5\in ℂ$$
66	64 65	addcomi	$$⊢2+5=5+2$$
67		5p2e7	$$⊢5+2=7$$
68	66 67	eqtri	$$⊢2+5=7$$
69	68	a1i	$$⊢\phi \to 2+5=7$$
70	32	leidd	$$⊢\phi \to 7\le 7$$
71	69 70	eqbrtrd	$$⊢\phi \to 2+5\le 7$$
72	11 61 32 63 71	letrd	$$⊢\phi \to 2\le 7$$
73	11 32 29 72 40	letrd	$$⊢\phi \to 2\le B$$
74		2z	$$⊢2\in \mathbb{Z}$$
75	74	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
76	75	uzidd	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 2}$$
77		2rp	$$⊢2\in {ℝ}^{+}$$
78	77	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
79	29 41	elrpd	$$⊢\phi \to B\in {ℝ}^{+}$$
80		logbleb	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 2\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(2\le B\leftrightarrow {\log }_{2}2\le {\log }_{2}B\right)$$
81	76 78 79 80	syl3anc	$$⊢\phi \to \left(2\le B\leftrightarrow {\log }_{2}2\le {\log }_{2}B\right)$$
82	73 81	mpbid	$$⊢\phi \to {\log }_{2}2\le {\log }_{2}B$$
83	44 47 42 58 82	letrd	$$⊢\phi \to 0+1\le {\log }_{2}B$$
84		fllep1	$$⊢{\log }_{2}B\in ℝ\to {\log }_{2}B\le ⌊{\log }_{2}B⌋+1$$
85	42 84	syl	$$⊢\phi \to {\log }_{2}B\le ⌊{\log }_{2}B⌋+1$$
86	44 42 46 83 85	letrd	$$⊢\phi \to 0+1\le ⌊{\log }_{2}B⌋+1$$
87	30 45 15	leadd1d	$$⊢\phi \to \left(0\le ⌊{\log }_{2}B⌋\leftrightarrow 0+1\le ⌊{\log }_{2}B⌋+1\right)$$
88	86 87	mpbird	$$⊢\phi \to 0\le ⌊{\log }_{2}B⌋$$
89	43 88	jca	$$⊢\phi \to \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
90		elnn0z	$$⊢⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
91	89 90	sylibr	$$⊢\phi \to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
92	9 91	reexpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in ℝ$$
93		fzfid	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
94	9	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in ℝ$$
95		elfznn	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in \mathbb{N}$$
96	95	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \mathbb{N}$$
97	96	nnnn0d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
98	94 97	reexpcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in ℝ$$
99		1red	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in ℝ$$
100	98 99	resubcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in ℝ$$
101	93 100	fprodrecl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in ℝ$$
102	92 101	remulcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in ℝ$$
103	2	a1i	$$⊢\phi \to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
104	103	eleq1d	$$⊢\phi \to \left(A\in ℝ\leftrightarrow N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in ℝ\right)$$
105	102 104	mpbird	$$⊢\phi \to A\in ℝ$$
106	7	a1i	$$⊢\phi \to E={{\log }_{2}N}^4$$
107	106	oveq2d	$$⊢\phi \to N^E=N^{{{\log }_{2}N}^4}$$
108		2cnd	$$⊢\phi \to 2\in ℂ$$
109	78	rpne0d	$$⊢\phi \to 2\ne 0$$
110	109 19	nelprd	$$⊢\phi \to \neg 2\in \left\{0,1\right\}$$
111	108 110	eldifd	$$⊢\phi \to 2\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
112	9	recnd	$$⊢\phi \to N\in ℂ$$
113	30 14	ltned	$$⊢\phi \to 0\ne N$$
114		necom	$$⊢0\ne N\leftrightarrow N\ne 0$$
115	114	imbi2i	$$⊢\left(\phi \to 0\ne N\right)\leftrightarrow \left(\phi \to N\ne 0\right)$$
116	113 115	mpbi	$$⊢\phi \to N\ne 0$$
117	116	neneqd	$$⊢\phi \to \neg N=0$$
118		c0ex	$$⊢0\in \mathrm{V}$$
119	118	elsn2	$$⊢N\in \left\{0\right\}\leftrightarrow N=0$$
120	117 119	sylnibr	$$⊢\phi \to \neg N\in \left\{0\right\}$$
121	112 120	eldifd	$$⊢\phi \to N\in \left(ℂ\setminus \left\{0\right\}\right)$$
122		cxplogb	$$⊢\left(2\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge N\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to 2^{{\log }_{2}N}=N$$
123	111 121 122	syl2anc	$$⊢\phi \to 2^{{\log }_{2}N}=N$$
124	123	eqcomd	$$⊢\phi \to N=2^{{\log }_{2}N}$$
125	124	oveq1d	$$⊢\phi \to N^{{{\log }_{2}N}^4}={\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}$$
126		eqidd	$$⊢\phi \to {\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}={\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}$$
127	125 126	eqtrd	$$⊢\phi \to N^{{{\log }_{2}N}^4}={\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}$$
128	107 127	eqtrd	$$⊢\phi \to N^E={\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}$$
129	106	eqcomd	$$⊢\phi \to {{\log }_{2}N}^4=E$$
130		4nn0	$$⊢4\in {\mathbb{N}}_0$$
131	130	a1i	$$⊢\phi \to 4\in {\mathbb{N}}_0$$
132	20 131	reexpcld	$$⊢\phi \to {{\log }_{2}N}^4\in ℝ$$
133	106	eleq1d	$$⊢\phi \to \left(E\in ℝ\leftrightarrow {{\log }_{2}N}^4\in ℝ\right)$$
134	132 133	mpbird	$$⊢\phi \to E\in ℝ$$
135	134	recnd	$$⊢\phi \to E\in ℂ$$
136	129 135	eqeltrd	$$⊢\phi \to {{\log }_{2}N}^4\in ℂ$$
137	78 20 136	cxpmuld	$$⊢\phi \to 2^{{\log }_{2}N{{\log }_{2}N}^4}={\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}$$
138	137	eqcomd	$$⊢\phi \to {\left(2^{{\log }_{2}N}\right)}^{{{\log }_{2}N}^4}=2^{{\log }_{2}N{{\log }_{2}N}^4}$$
139	128 138	eqtrd	$$⊢\phi \to N^E=2^{{\log }_{2}N{{\log }_{2}N}^4}$$
140	20	recnd	$$⊢\phi \to {\log }_{2}N\in ℂ$$
141	140	exp1d	$$⊢\phi \to {{\log }_{2}N}^1={\log }_{2}N$$
142	141	eqcomd	$$⊢\phi \to {\log }_{2}N={{\log }_{2}N}^1$$
143	142	oveq1d	$$⊢\phi \to {\log }_{2}N{{\log }_{2}N}^4={{\log }_{2}N}^1{{\log }_{2}N}^4$$
144		1nn0	$$⊢1\in {\mathbb{N}}_0$$
145	144	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
146	140 131 145	expaddd	$$⊢\phi \to {{\log }_{2}N}^{1+4}={{\log }_{2}N}^1{{\log }_{2}N}^4$$
147	146	eqcomd	$$⊢\phi \to {{\log }_{2}N}^1{{\log }_{2}N}^4={{\log }_{2}N}^{1+4}$$
148	143 147	eqtrd	$$⊢\phi \to {\log }_{2}N{{\log }_{2}N}^4={{\log }_{2}N}^{1+4}$$
149	148	oveq2d	$$⊢\phi \to 2^{{\log }_{2}N{{\log }_{2}N}^4}=2^{{{\log }_{2}N}^{1+4}}$$
150	139 149	eqtrd	$$⊢\phi \to N^E=2^{{{\log }_{2}N}^{1+4}}$$
151		4cn	$$⊢4\in ℂ$$
152		ax-1cn	$$⊢1\in ℂ$$
153		4p1e5	$$⊢4+1=5$$
154	151 152 153	addcomli	$$⊢1+4=5$$
155	154	a1i	$$⊢\phi \to 1+4=5$$
156	155	oveq2d	$$⊢\phi \to {{\log }_{2}N}^{1+4}={{\log }_{2}N}^5$$
157	156	oveq2d	$$⊢\phi \to 2^{{{\log }_{2}N}^{1+4}}=2^{{{\log }_{2}N}^5}$$
158	150 157	eqtrd	$$⊢\phi \to N^E=2^{{{\log }_{2}N}^5}$$
159		3re	$$⊢3\in ℝ$$
160	159	a1i	$$⊢\phi \to 3\in ℝ$$
161		0le1	$$⊢0\le 1$$
162	161	a1i	$$⊢\phi \to 0\le 1$$
163		1lt3	$$⊢1<3$$
164	163	a1i	$$⊢\phi \to 1<3$$
165	15 160 164	ltled	$$⊢\phi \to 1\le 3$$
166	30 15 160 162 165	letrd	$$⊢\phi \to 0\le 3$$
167	30 160 9 166 4	letrd	$$⊢\phi \to 0\le N$$
168	9 167 134	recxpcld	$$⊢\phi \to N^E\in ℝ$$
169	158 168	eqeltrrd	$$⊢\phi \to 2^{{{\log }_{2}N}^5}\in ℝ$$
170	27	eleq1d	$$⊢\phi \to \left(B\in \mathbb{Z}\leftrightarrow ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}\right)$$
171	25 170	mpbird	$$⊢\phi \to B\in \mathbb{Z}$$
172	30 29 41	ltled	$$⊢\phi \to 0\le B$$
173	171 172	jca	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge 0\le B\right)$$
174		elnn0z	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{Z}\wedge 0\le B\right)$$
175	173 174	sylibr	$$⊢\phi \to B\in {\mathbb{N}}_0$$
176	11 175	reexpcld	$$⊢\phi \to 2^B\in ℝ$$
177	9 14	elrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
178	23 15	readdcld	$$⊢\phi \to {{\log }_{2}N}^5+1\in ℝ$$
179	22	nn0zd	$$⊢\phi \to 5\in \mathbb{Z}$$
180		logb1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}1=0$$
181	51 52 19 180	syl3anc	$$⊢\phi \to {\log }_{2}1=0$$
182	181 30	eqeltrd	$$⊢\phi \to {\log }_{2}1\in ℝ$$
183	30	leidd	$$⊢\phi \to 0\le 0$$
184	181	eqcomd	$$⊢\phi \to 0={\log }_{2}1$$
185	183 184	breqtrd	$$⊢\phi \to 0\le {\log }_{2}1$$
186	15 160 9 164 4	ltletrd	$$⊢\phi \to 1<N$$
187		1rp	$$⊢1\in {ℝ}^{+}$$
188	187	a1i	$$⊢\phi \to 1\in {ℝ}^{+}$$
189		logblt	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 1\in {ℝ}^{+}\wedge N\in {ℝ}^{+}\right)\to \left(1<N\leftrightarrow {\log }_{2}1<{\log }_{2}N\right)$$
190	76 188 177 189	syl3anc	$$⊢\phi \to \left(1<N\leftrightarrow {\log }_{2}1<{\log }_{2}N\right)$$
191	186 190	mpbid	$$⊢\phi \to {\log }_{2}1<{\log }_{2}N$$
192	30 182 20 185 191	lelttrd	$$⊢\phi \to 0<{\log }_{2}N$$
193	20 179 192	3jca	$$⊢\phi \to \left({\log }_{2}N\in ℝ\wedge 5\in \mathbb{Z}\wedge 0<{\log }_{2}N\right)$$
194		expgt0	$$⊢\left({\log }_{2}N\in ℝ\wedge 5\in \mathbb{Z}\wedge 0<{\log }_{2}N\right)\to 0<{{\log }_{2}N}^5$$
195	193 194	syl	$$⊢\phi \to 0<{{\log }_{2}N}^5$$
196		ltp1	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5<{{\log }_{2}N}^5+1$$
197	23 196	syl	$$⊢\phi \to {{\log }_{2}N}^5<{{\log }_{2}N}^5+1$$
198	30 23 178 195 197	lttrd	$$⊢\phi \to 0<{{\log }_{2}N}^5+1$$
199	11 13 178 198 19	relogbcld	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)\in ℝ$$
200	5	a1i	$$⊢\phi \to C={\log }_2\left({{\log }_{2}N}^5+1\right)$$
201	200	eleq1d	$$⊢\phi \to \left(C\in ℝ\leftrightarrow {\log }_2\left({{\log }_{2}N}^5+1\right)\in ℝ\right)$$
202	199 201	mpbird	$$⊢\phi \to C\in ℝ$$
203	20	resqcld	$$⊢\phi \to {{\log }_{2}N}^2\in ℝ$$
204	6	a1i	$$⊢\phi \to D={{\log }_{2}N}^2$$
205	204	eleq1d	$$⊢\phi \to \left(D\in ℝ\leftrightarrow {{\log }_{2}N}^2\in ℝ\right)$$
206	203 205	mpbird	$$⊢\phi \to D\in ℝ$$
207	206	rehalfcld	$$⊢\phi \to \frac{D}{2}\in ℝ$$
208	202 207	readdcld	$$⊢\phi \to C+\left(\frac{D}{2}\right)\in ℝ$$
209	134 11 109	redivcld	$$⊢\phi \to \frac{E}{2}\in ℝ$$
210	208 209	readdcld	$$⊢\phi \to C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)\in ℝ$$
211	177 210	rpcxpcld	$$⊢\phi \to N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}\in {ℝ}^{+}$$
212	211	rpred	$$⊢\phi \to N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}\in ℝ$$
213	1 2 3 4	aks4d1p1p2	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)}$$
214	129	oveq1d	$$⊢\phi \to \frac{{{\log }_{2}N}^4}{2}=\frac{E}{2}$$
215	214	oveq2d	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)={\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{E}{2}\right)$$
216	200	eqcomd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)=C$$
217	216	oveq1d	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)=C+\left(\frac{{{\log }_{2}N}^2}{2}\right)$$
218	204	eqcomd	$$⊢\phi \to {{\log }_{2}N}^2=D$$
219	218	oveq1d	$$⊢\phi \to \frac{{{\log }_{2}N}^2}{2}=\frac{D}{2}$$
220	219	oveq2d	$$⊢\phi \to C+\left(\frac{{{\log }_{2}N}^2}{2}\right)=C+\left(\frac{D}{2}\right)$$
221	217 220	eqtrd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)=C+\left(\frac{D}{2}\right)$$
222	221	oveq1d	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{E}{2}\right)=C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)$$
223	215 222	eqtrd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)=C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)$$
224	223	oveq2d	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)}=N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}$$
225	213 224	breqtrd	$$⊢\phi \to A<N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}$$
226	202	recnd	$$⊢\phi \to C\in ℂ$$
227	226 108 109	divcan3d	$$⊢\phi \to \frac{2C}{2}=C$$
228	227	eqcomd	$$⊢\phi \to C=\frac{2C}{2}$$
229	228	oveq1d	$$⊢\phi \to C+\left(\frac{D}{2}\right)=\left(\frac{2C}{2}\right)+\left(\frac{D}{2}\right)$$
230	11 202	remulcld	$$⊢\phi \to 2C\in ℝ$$
231	230	recnd	$$⊢\phi \to 2C\in ℂ$$
232	206	recnd	$$⊢\phi \to D\in ℂ$$
233	231 232 51 109	divdird	$$⊢\phi \to \frac{2C+D}{2}=\left(\frac{2C}{2}\right)+\left(\frac{D}{2}\right)$$
234	233	eqcomd	$$⊢\phi \to \left(\frac{2C}{2}\right)+\left(\frac{D}{2}\right)=\frac{2C+D}{2}$$
235	229 234	eqtrd	$$⊢\phi \to C+\left(\frac{D}{2}\right)=\frac{2C+D}{2}$$
236	230 206	readdcld	$$⊢\phi \to 2C+D\in ℝ$$
237	236 134 78	lediv1d	$$⊢\phi \to \left(2C+D\le E\leftrightarrow \frac{2C+D}{2}\le \frac{E}{2}\right)$$
238	8 237	mpbid	$$⊢\phi \to \frac{2C+D}{2}\le \frac{E}{2}$$
239	235 238	eqbrtrd	$$⊢\phi \to C+\left(\frac{D}{2}\right)\le \frac{E}{2}$$
240	208 209 209 239	leadd1dd	$$⊢\phi \to C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)\le \left(\frac{E}{2}\right)+\left(\frac{E}{2}\right)$$
241	135	2halvesd	$$⊢\phi \to \left(\frac{E}{2}\right)+\left(\frac{E}{2}\right)=E$$
242	240 241	breqtrd	$$⊢\phi \to C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)\le E$$
243	9 186 210 134	cxpled	$$⊢\phi \to \left(C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)\le E\leftrightarrow N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}\le N^E\right)$$
244	242 243	mpbid	$$⊢\phi \to N^{C+\left(\frac{D}{2}\right)+\left(\frac{E}{2}\right)}\le N^E$$
245	105 212 168 225 244	ltletrd	$$⊢\phi \to A<N^E$$
246	245 158	breqtrd	$$⊢\phi \to A<2^{{{\log }_{2}N}^5}$$
247		1le2	$$⊢1\le 2$$
248	247	a1i	$$⊢\phi \to 1\le 2$$
249	175	nn0red	$$⊢\phi \to B\in ℝ$$
250	27	eqcomd	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉=B$$
251	38 250	breqtrd	$$⊢\phi \to {{\log }_{2}N}^5\le B$$
252	11 248 23 249 251	cxplead	$$⊢\phi \to 2^{{{\log }_{2}N}^5}\le 2^B$$
253		cxpexp	$$⊢\left(2\in ℂ\wedge B\in {\mathbb{N}}_0\right)\to 2^B=2^B$$
254	108 175 253	syl2anc	$$⊢\phi \to 2^B=2^B$$
255	252 254	breqtrd	$$⊢\phi \to 2^{{{\log }_{2}N}^5}\le 2^B$$
256	105 169 176 246 255	ltletrd	$$⊢\phi \to A<2^B$$