Theorem aks4d1p1p2

Description: Rewrite A in more suitable form. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p2.1	$$⊢\phi \to N\in \mathbb{N}$$
	aks4d1p1p2.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p1p2.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p1p2.4	$$⊢\phi \to 3\le N$$
Assertion	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)}$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p2.1	$$⊢\phi \to N\in \mathbb{N}$$
2		aks4d1p1p2.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p1p2.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		aks4d1p1p2.4	$$⊢\phi \to 3\le N$$
5	1	nnred	$$⊢\phi \to N\in ℝ$$
6		2re	$$⊢2\in ℝ$$
7	6	a1i	$$⊢\phi \to 2\in ℝ$$
8		2pos	$$⊢0<2$$
9	8	a1i	$$⊢\phi \to 0<2$$
10	1	nngt0d	$$⊢\phi \to 0<N$$
11		1red	$$⊢\phi \to 1\in ℝ$$
12		1lt2	$$⊢1<2$$
13	12	a1i	$$⊢\phi \to 1<2$$
14	11 13	ltned	$$⊢\phi \to 1\ne 2$$
15	14	necomd	$$⊢\phi \to 2\ne 1$$
16	7 9 5 10 15	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
17		5nn0	$$⊢5\in {\mathbb{N}}_0$$
18	17	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
19	16 18	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
20		ceilcl	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
21	19 20	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
22	21	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
23	3	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
24	23	eleq1d	$$⊢\phi \to \left(B\in ℝ\leftrightarrow ⌈{{\log }_{2}N}^5⌉\in ℝ\right)$$
25	22 24	mpbird	$$⊢\phi \to B\in ℝ$$
26		0red	$$⊢\phi \to 0\in ℝ$$
27	18	nn0zd	$$⊢\phi \to 5\in \mathbb{Z}$$
28		3re	$$⊢3\in ℝ$$
29	28	a1i	$$⊢\phi \to 3\in ℝ$$
30		1lt3	$$⊢1<3$$
31	30	a1i	$$⊢\phi \to 1<3$$
32	11 29 5 31 4	ltletrd	$$⊢\phi \to 1<N$$
33	5 10	elrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
34		2rp	$$⊢2\in {ℝ}^{+}$$
35	34 12	pm3.2i	$$⊢\left(2\in {ℝ}^{+}\wedge 1<2\right)$$
36	35	a1i	$$⊢\phi \to \left(2\in {ℝ}^{+}\wedge 1<2\right)$$
37		logbgt0b	$$⊢\left(N\in {ℝ}^{+}\wedge \left(2\in {ℝ}^{+}\wedge 1<2\right)\right)\to \left(0<{\log }_{2}N\leftrightarrow 1<N\right)$$
38	33 36 37	syl2anc	$$⊢\phi \to \left(0<{\log }_{2}N\leftrightarrow 1<N\right)$$
39	32 38	mpbird	$$⊢\phi \to 0<{\log }_{2}N$$
40		expgt0	$$⊢\left({\log }_{2}N\in ℝ\wedge 5\in \mathbb{Z}\wedge 0<{\log }_{2}N\right)\to 0<{{\log }_{2}N}^5$$
41	16 27 39 40	syl3anc	$$⊢\phi \to 0<{{\log }_{2}N}^5$$
42		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
43	19 42	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
44	26 19 22 41 43	ltletrd	$$⊢\phi \to 0<⌈{{\log }_{2}N}^5⌉$$
45	23	breq2d	$$⊢\phi \to \left(0<B\leftrightarrow 0<⌈{{\log }_{2}N}^5⌉\right)$$
46	44 45	mpbird	$$⊢\phi \to 0<B$$
47	7 9 25 46 15	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
48	47	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
49		7re	$$⊢7\in ℝ$$
50	49	a1i	$$⊢\phi \to 7\in ℝ$$
51		1lt7	$$⊢1<7$$
52	51	a1i	$$⊢\phi \to 1<7$$
53	5 4	3lexlogpow5ineq3	$$⊢\phi \to 7<{{\log }_{2}N}^5$$
54	11 50 19 52 53	lttrd	$$⊢\phi \to 1<{{\log }_{2}N}^5$$
55	11 19 22 54 43	ltletrd	$$⊢\phi \to 1<⌈{{\log }_{2}N}^5⌉$$
56	23	breq2d	$$⊢\phi \to \left(1<B\leftrightarrow 1<⌈{{\log }_{2}N}^5⌉\right)$$
57	55 56	mpbird	$$⊢\phi \to 1<B$$
58	25 46	elrpd	$$⊢\phi \to B\in {ℝ}^{+}$$
59		logbgt0b	$$⊢\left(B\in {ℝ}^{+}\wedge \left(2\in {ℝ}^{+}\wedge 1<2\right)\right)\to \left(0<{\log }_{2}B\leftrightarrow 1<B\right)$$
60	58 36 59	syl2anc	$$⊢\phi \to \left(0<{\log }_{2}B\leftrightarrow 1<B\right)$$
61	57 60	mpbird	$$⊢\phi \to 0<{\log }_{2}B$$
62	26 47 61	ltled	$$⊢\phi \to 0\le {\log }_{2}B$$
63		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
64		flge	$$⊢\left({\log }_{2}B\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
65	47 63 64	syl2anc	$$⊢\phi \to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
66	62 65	mpbid	$$⊢\phi \to 0\le ⌊{\log }_{2}B⌋$$
67	48 66	jca	$$⊢\phi \to \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
68		elnn0z	$$⊢⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
69	67 68	sylibr	$$⊢\phi \to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
70	5 69	reexpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in ℝ$$
71		fzfid	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
72	5	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in ℝ$$
73		elfznn	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in \mathbb{N}$$
74	73	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \mathbb{N}$$
75		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
76	74 75	syl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
77	72 76	reexpcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in ℝ$$
78		1red	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in ℝ$$
79	77 78	resubcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in ℝ$$
80	71 79	fprodrecl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in ℝ$$
81	70 80	remulcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in ℝ$$
82	2	a1i	$$⊢\phi \to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
83	82	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)$$
84	81 83	mpbird	$$⊢\phi \to A\in ℝ$$
85	1	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
86	85	nn0ge0d	$$⊢\phi \to 0\le N$$
87	19 11	readdcld	$$⊢\phi \to {{\log }_{2}N}^5+1\in ℝ$$
88	19	ltp1d	$$⊢\phi \to {{\log }_{2}N}^5<{{\log }_{2}N}^5+1$$
89	26 19 87 41 88	lttrd	$$⊢\phi \to 0<{{\log }_{2}N}^5+1$$
90	7 9 87 89 15	relogbcld	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)\in ℝ$$
91	16	resqcld	$$⊢\phi \to {{\log }_{2}N}^2\in ℝ$$
92	91	flcld	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}$$
93	92	zred	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in ℝ$$
94		0lt1	$$⊢0<1$$
95	94	a1i	$$⊢\phi \to 0<1$$
96	7 9 7 9 15	relogbcld	$$⊢\phi \to {\log }_{2}2\in ℝ$$
97	96	resqcld	$$⊢\phi \to {{\log }_{2}2}^2\in ℝ$$
98		2nn0	$$⊢2\in {\mathbb{N}}_0$$
99	98	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
100	11	leidd	$$⊢\phi \to 1\le 1$$
101	7	recnd	$$⊢\phi \to 2\in ℂ$$
102	26 9	gtned	$$⊢\phi \to 2\ne 0$$
103		logbid1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}2=1$$
104	101 102 15 103	syl3anc	$$⊢\phi \to {\log }_{2}2=1$$
105	104	eqcomd	$$⊢\phi \to 1={\log }_{2}2$$
106	100 105	breqtrd	$$⊢\phi \to 1\le {\log }_{2}2$$
107	96 99 106	expge1d	$$⊢\phi \to 1\le {{\log }_{2}2}^2$$
108	105	eqcomd	$$⊢\phi \to {\log }_{2}2=1$$
109	108	oveq1d	$$⊢\phi \to {{\log }_{2}2}^2=1^2$$
110	99	nn0zd	$$⊢\phi \to 2\in \mathbb{Z}$$
111		1exp	$$⊢2\in \mathbb{Z}\to 1^2=1$$
112	110 111	syl	$$⊢\phi \to 1^2=1$$
113	109 112	eqtrd	$$⊢\phi \to {{\log }_{2}2}^2=1$$
114	7	leidd	$$⊢\phi \to 2\le 2$$
115		1nn0	$$⊢1\in {\mathbb{N}}_0$$
116	6 115	nn0addge1i	$$⊢2\le 2+1$$
117		2p1e3	$$⊢2+1=3$$
118	116 117	breqtri	$$⊢2\le 3$$
119	118	a1i	$$⊢\phi \to 2\le 3$$
120	7 29 5 119 4	letrd	$$⊢\phi \to 2\le N$$
121	110 114 7 9 5 10 120	logblebd	$$⊢\phi \to {\log }_{2}2\le {\log }_{2}N$$
122	11 96 16 106 121	letrd	$$⊢\phi \to 1\le {\log }_{2}N$$
123	16 99 122	expge1d	$$⊢\phi \to 1\le {{\log }_{2}N}^2$$
124	113 123	eqbrtrd	$$⊢\phi \to {{\log }_{2}2}^2\le {{\log }_{2}N}^2$$
125		1z	$$⊢1\in \mathbb{Z}$$
126		zsqcl	$$⊢1\in \mathbb{Z}\to 1^2\in \mathbb{Z}$$
127	125 126	ax-mp	$$⊢1^2\in \mathbb{Z}$$
128	127	a1i	$$⊢\phi \to 1^2\in \mathbb{Z}$$
129	109	eleq1d	$$⊢\phi \to \left({{\log }_{2}2}^2\in \mathbb{Z}\leftrightarrow 1^2\in \mathbb{Z}\right)$$
130	128 129	mpbird	$$⊢\phi \to {{\log }_{2}2}^2\in \mathbb{Z}$$
131	91 130	jca	$$⊢\phi \to \left({{\log }_{2}N}^2\in ℝ\wedge {{\log }_{2}2}^2\in \mathbb{Z}\right)$$
132		flge	$$⊢\left({{\log }_{2}N}^2\in ℝ\wedge {{\log }_{2}2}^2\in \mathbb{Z}\right)\to \left({{\log }_{2}2}^2\le {{\log }_{2}N}^2\leftrightarrow {{\log }_{2}2}^2\le ⌊{{\log }_{2}N}^2⌋\right)$$
133	131 132	syl	$$⊢\phi \to \left({{\log }_{2}2}^2\le {{\log }_{2}N}^2\leftrightarrow {{\log }_{2}2}^2\le ⌊{{\log }_{2}N}^2⌋\right)$$
134	124 133	mpbid	$$⊢\phi \to {{\log }_{2}2}^2\le ⌊{{\log }_{2}N}^2⌋$$
135	11 97 93 107 134	letrd	$$⊢\phi \to 1\le ⌊{{\log }_{2}N}^2⌋$$
136	26 11 93 95 135	ltletrd	$$⊢\phi \to 0<⌊{{\log }_{2}N}^2⌋$$
137	92 136	jca	$$⊢\phi \to \left(⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}\wedge 0<⌊{{\log }_{2}N}^2⌋\right)$$
138		elnnz	$$⊢⌊{{\log }_{2}N}^2⌋\in \mathbb{N}\leftrightarrow \left(⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}\wedge 0<⌊{{\log }_{2}N}^2⌋\right)$$
139	138	bicomi	$$⊢\left(⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}\wedge 0<⌊{{\log }_{2}N}^2⌋\right)\leftrightarrow ⌊{{\log }_{2}N}^2⌋\in \mathbb{N}$$
140	139	a1i	$$⊢\phi \to \left(\left(⌊{{\log }_{2}N}^2⌋\in \mathbb{Z}\wedge 0<⌊{{\log }_{2}N}^2⌋\right)\leftrightarrow ⌊{{\log }_{2}N}^2⌋\in \mathbb{N}\right)$$
141	137 140	mpbid	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in \mathbb{N}$$
142	141	nnnn0d	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in {\mathbb{N}}_0$$
143		arisum	$$⊢⌊{{\log }_{2}N}^2⌋\in {\mathbb{N}}_0\to \sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k=\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}$$
144	142 143	syl	$$⊢\phi \to \sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k=\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}$$
145	74	nnred	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in ℝ$$
146	71 145	fsumrecl	$$⊢\phi \to \sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k\in ℝ$$
147	144 146	eqeltrrd	$$⊢\phi \to \frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\in ℝ$$
148	90 147	readdcld	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)\in ℝ$$
149	5 86 148	recxpcld	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}\in ℝ$$
150		4nn0	$$⊢4\in {\mathbb{N}}_0$$
151	150	a1i	$$⊢\phi \to 4\in {\mathbb{N}}_0$$
152	16 151	reexpcld	$$⊢\phi \to {{\log }_{2}N}^4\in ℝ$$
153	152 91	readdcld	$$⊢\phi \to {{\log }_{2}N}^4+{{\log }_{2}N}^2\in ℝ$$
154	153	rehalfcld	$$⊢\phi \to \frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\in ℝ$$
155	90 154	readdcld	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)\in ℝ$$
156	5 86 155	recxpcld	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)}\in ℝ$$
157		reflcl	$$⊢{\log }_{2}B\in ℝ\to ⌊{\log }_{2}B⌋\in ℝ$$
158	47 157	syl	$$⊢\phi \to ⌊{\log }_{2}B⌋\in ℝ$$
159	5 86 158	recxpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in ℝ$$
160	33 146	rpcxpcld	$$⊢\phi \to N^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}\in {ℝ}^{+}$$
161	33 141	aks4d1p1p1	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=N^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}$$
162	161	eleq1d	$$⊢\phi \to \left(\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in {ℝ}^{+}\leftrightarrow N^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}\in {ℝ}^{+}\right)$$
163	160 162	mpbird	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in {ℝ}^{+}$$
164	163	rpregt0d	$$⊢\phi \to \left(\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ\wedge 0<\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\right)$$
165	164	simpld	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ$$
166	159 165	remulcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ$$
167	5 86 90	recxpcld	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\in ℝ$$
168	167 165	remulcld	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ$$
169	71 77	fprodrecl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ$$
170	5 69 86	expge0d	$$⊢\phi \to 0\le N^{⌊{\log }_{2}B⌋}$$
171		nfv	$$⊢Ⅎk\phi$$
172		0red	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 0\in ℝ$$
173	1	nnge1d	$$⊢\phi \to 1\le N$$
174	173	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\le N$$
175	72 76 174	expge1d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\le N^k$$
176	77	recnd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in ℂ$$
177	176	subid1d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-0=N^k$$
178	177	breq2d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to \left(1\le N^k-0\leftrightarrow 1\le N^k\right)$$
179	175 178	mpbird	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\le N^k-0$$
180	78 77 172 179	lesubd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 0\le N^k-1$$
181	77	lem1d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\le N^k$$
182	171 71 79 180 77 181	fprodle	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\le \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
183	80 169 70 170 182	lemul2ad	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
184	82	breq1d	$$⊢\phi \to \left(A\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\leftrightarrow N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\right)$$
185	183 184	mpbird	$$⊢\phi \to A\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
186	72	recnd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in ℂ$$
187		cxpexp	$$⊢\left(N\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to N^k=N^k$$
188	186 76 187	syl2anc	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k=N^k$$
189	188	eqcomd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k=N^k$$
190	189	prodeq2dv	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
191	190	oveq2d	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
192	185 191	breqtrd	$$⊢\phi \to A\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
193	5	recnd	$$⊢\phi \to N\in ℂ$$
194		cxpexp	$$⊢\left(N\in ℂ\wedge ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\right)\to N^{⌊{\log }_{2}B⌋}=N^{⌊{\log }_{2}B⌋}$$
195	193 69 194	syl2anc	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}=N^{⌊{\log }_{2}B⌋}$$
196	195	oveq1d	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
197	196	eqcomd	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
198	192 197	breqtrd	$$⊢\phi \to A\le N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
199	159 167 164	3jca	$$⊢\phi \to \left(N^{⌊{\log }_{2}B⌋}\in ℝ\wedge N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\in ℝ\wedge \left(\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ\wedge 0<\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\right)\right)$$
200	1 3 4	aks4d1p1p3	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}$$
201		ltmul1a	$$⊢\left(\left(N^{⌊{\log }_{2}B⌋}\in ℝ\wedge N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\in ℝ\wedge \left(\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\in ℝ\wedge 0<\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k\right)\right)\wedge N^{⌊{\log }_{2}B⌋}<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\right)\to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
202	199 200 201	syl2anc	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
203	84 166 168 198 202	lelttrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k$$
204	161	oveq2d	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}{N}^k=N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}$$
205	203 204	breqtrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}$$
206	144	oveq2d	$$⊢\phi \to N^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}=N^{\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}}$$
207	206	oveq2d	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\sum _{k=1}^{⌊{{\log }_{2}N}^2⌋}k}=N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}}$$
208	205 207	breqtrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}}$$
209	26 10	gtned	$$⊢\phi \to N\ne 0$$
210	90	recnd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)\in ℂ$$
211	141	nncnd	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in ℂ$$
212	211	sqcld	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2\in ℂ$$
213	212 211	addcld	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋\in ℂ$$
214	213	halfcld	$$⊢\phi \to \frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\in ℂ$$
215	193 209 210 214	cxpaddd	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}=N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}}$$
216	215	eqcomd	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}{N}^{\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}}=N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}$$
217	208 216	breqtrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}$$
218		reflcl	$$⊢{{\log }_{2}N}^2\in ℝ\to ⌊{{\log }_{2}N}^2⌋\in ℝ$$
219	91 218	syl	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\in ℝ$$
220	219	resqcld	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2\in ℝ$$
221	220 219	readdcld	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋\in ℝ$$
222	34	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
223	91 99	reexpcld	$$⊢\phi \to {\left({{\log }_{2}N}^2\right)}^2\in ℝ$$
224		id	$$⊢\phi \to \phi$$
225	142	nn0ge0d	$$⊢\phi \to 0\le ⌊{{\log }_{2}N}^2⌋$$
226		flle	$$⊢{{\log }_{2}N}^2\in ℝ\to ⌊{{\log }_{2}N}^2⌋\le {{\log }_{2}N}^2$$
227	91 226	syl	$$⊢\phi \to ⌊{{\log }_{2}N}^2⌋\le {{\log }_{2}N}^2$$
228	219 91 99 225 227	leexp1ad	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2\le {\left({{\log }_{2}N}^2\right)}^2$$
229	224 228	syl	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2\le {\left({{\log }_{2}N}^2\right)}^2$$
230	16	recnd	$$⊢\phi \to {\log }_{2}N\in ℂ$$
231	230 99 99	expmuld	$$⊢\phi \to {{\log }_{2}N}^{2\cdot 2}={\left({{\log }_{2}N}^2\right)}^2$$
232	231	eqcomd	$$⊢\phi \to {\left({{\log }_{2}N}^2\right)}^2={{\log }_{2}N}^{2\cdot 2}$$
233		2t2e4	$$⊢2\cdot 2=4$$
234	233	oveq2i	$$⊢{{\log }_{2}N}^{2\cdot 2}={{\log }_{2}N}^4$$
235	234	a1i	$$⊢\phi \to {{\log }_{2}N}^{2\cdot 2}={{\log }_{2}N}^4$$
236	232 235	eqtrd	$$⊢\phi \to {\left({{\log }_{2}N}^2\right)}^2={{\log }_{2}N}^4$$
237	223 236	eqled	$$⊢\phi \to {\left({{\log }_{2}N}^2\right)}^2\le {{\log }_{2}N}^4$$
238	220 223 152 229 237	letrd	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2\le {{\log }_{2}N}^4$$
239	220 219 152 91 238 227	le2addd	$$⊢\phi \to {⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋\le {{\log }_{2}N}^4+{{\log }_{2}N}^2$$
240	221 153 222 239	lediv1dd	$$⊢\phi \to \frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\le \frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}$$
241	147 154 90 240	leadd2dd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)\le {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)$$
242	5 32 148 155	cxpled	$$⊢\phi \to \left({\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)\le {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)\leftrightarrow N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}\le N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)}\right)$$
243	241 242	mpbid	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{⌊{{\log }_{2}N}^2⌋}^2+⌊{{\log }_{2}N}^2⌋}{2}\right)}\le N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)}$$
244	84 149 156 217 243	ltletrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)}$$
245	152	recnd	$$⊢\phi \to {{\log }_{2}N}^4\in ℂ$$
246	91	recnd	$$⊢\phi \to {{\log }_{2}N}^2\in ℂ$$
247	245 246 101 102	divdird	$$⊢\phi \to \frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}=\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)$$
248	247	oveq2d	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)={\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)$$
249	248	oveq2d	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4+{{\log }_{2}N}^2}{2}\right)}=N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)}$$
250	244 249	breqtrd	$$⊢\phi \to A<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)}$$
251	245 101 102	divcld	$$⊢\phi \to \frac{{{\log }_{2}N}^4}{2}\in ℂ$$
252	246 101 102	divcld	$$⊢\phi \to \frac{{{\log }_{2}N}^2}{2}\in ℂ$$
253	251 252	addcomd	$$⊢\phi \to \left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)=\left(\frac{{{\log }_{2}N}^2}{2}\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)$$
254	253	oveq2d	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)={\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)$$
255	210 252 251	addassd	$$⊢\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{{{\log }_{2}N}^4}{2}\right)$$
256	255	eqcomd	$$⊢\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{{{\log }_{2}N}^4}{2}\right)$$
257	254 256	eqtrd	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)={\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)$$
258	257	oveq2d	$$⊢\phi \to N^{{\log }_2\left({{\log }_{2}N}^5+1\right)+\left(\frac{{{\log }_{2}N}^4}{2}\right)+\left(\frac{{{\log }_{2}N}^2}{2}\right)}=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)}$$
259	250 258	breqtrd	$$⊢\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)}$$