Theorem aks4d1p1

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 21-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1p1.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p1.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
Assertion	aks4d1p1	$$⊢\phi \to A<2^B$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1p1.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p1.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		3nn	$$⊢3\in \mathbb{N}$$
5	4	a1i	$$⊢\left(\phi \wedge 3<N\right)\to 3\in \mathbb{N}$$
6	1	adantr	$$⊢\left(\phi \wedge 3<N\right)\to N\in {\mathbb{Z}}_{\ge 3}$$
7		eluznn	$$⊢\left(3\in \mathbb{N}\wedge N\in {\mathbb{Z}}_{\ge 3}\right)\to N\in \mathbb{N}$$
8	5 6 7	syl2anc	$$⊢\left(\phi \wedge 3<N\right)\to N\in \mathbb{N}$$
9		3p1e4	$$⊢3+1=4$$
10		simpr	$$⊢\left(\phi \wedge 3<N\right)\to 3<N$$
11		3z	$$⊢3\in \mathbb{Z}$$
12	11	a1i	$$⊢\left(\phi \wedge 3<N\right)\to 3\in \mathbb{Z}$$
13		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
14	1 13	syl	$$⊢\phi \to N\in \mathbb{Z}$$
15	14	adantr	$$⊢\left(\phi \wedge 3<N\right)\to N\in \mathbb{Z}$$
16	12 15	zltp1led	$$⊢\left(\phi \wedge 3<N\right)\to \left(3<N\leftrightarrow 3+1\le N\right)$$
17	10 16	mpbid	$$⊢\left(\phi \wedge 3<N\right)\to 3+1\le N$$
18	9 17	eqbrtrrid	$$⊢\left(\phi \wedge 3<N\right)\to 4\le N$$
19		eqid	$$⊢{\log }_2\left({{\log }_{2}N}^5+1\right)={\log }_2\left({{\log }_{2}N}^5+1\right)$$
20		eqid	$$⊢{{\log }_{2}N}^2={{\log }_{2}N}^2$$
21		eqid	$$⊢{{\log }_{2}N}^4={{\log }_{2}N}^4$$
22	8 2 3 18 19 20 21	aks4d1p1p5	$$⊢\left(\phi \wedge 3<N\right)\to A<2^B$$
23	22	ex	$$⊢\phi \to \left(3<N\to A<2^B\right)$$
24		simp2	$$⊢\left(\phi \wedge 3=N\wedge k\in \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)\right)\to 3=N$$
25	24	eqcomd	$$⊢\left(\phi \wedge 3=N\wedge k\in \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)\right)\to N=3$$
26	25	oveq1d	$$⊢\left(\phi \wedge 3=N\wedge k\in \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)\right)\to N^k=3^k$$
27	26	oveq1d	$$⊢\left(\phi \wedge 3=N\wedge k\in \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)\right)\to N^k-1=3^k-1$$
28	27	3expa	$$⊢\left(\left(\phi \wedge 3=N\right)\wedge k\in \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)\right)\to N^k-1=3^k-1$$
29	28	prodeq2dv	$$⊢\left(\phi \wedge 3=N\right)\to \prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(N^k-1\right)=\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)$$
30	29	oveq2d	$$⊢\left(\phi \wedge 3=N\right)\to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(N^k-1\right)=3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)$$
31		2rp	$$⊢2\in {ℝ}^{+}$$
32	31	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
33		1red	$$⊢\phi \to 1\in ℝ$$
34		1lt2	$$⊢1<2$$
35	34	a1i	$$⊢\phi \to 1<2$$
36	33 35	ltned	$$⊢\phi \to 1\ne 2$$
37	36	necomd	$$⊢\phi \to 2\ne 1$$
38	11	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
39	32 37 38	relogbexpd	$$⊢\phi \to {\log }_2{2}^3=3$$
40	39	eqcomd	$$⊢\phi \to 3={\log }_2{2}^3$$
41		cu2	$$⊢2^3=8$$
42	41	a1i	$$⊢\phi \to 2^3=8$$
43	42	oveq2d	$$⊢\phi \to {\log }_2{2}^3={\log }_{2}8$$
44	40 43	eqtrd	$$⊢\phi \to 3={\log }_{2}8$$
45		2z	$$⊢2\in \mathbb{Z}$$
46	45	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
47	46	zred	$$⊢\phi \to 2\in ℝ$$
48	47	leidd	$$⊢\phi \to 2\le 2$$
49		8re	$$⊢8\in ℝ$$
50	49	a1i	$$⊢\phi \to 8\in ℝ$$
51		8pos	$$⊢0<8$$
52	51	a1i	$$⊢\phi \to 0<8$$
53	32	rpgt0d	$$⊢\phi \to 0<2$$
54		3re	$$⊢3\in ℝ$$
55	54	a1i	$$⊢\phi \to 3\in ℝ$$
56	4	nngt0i	$$⊢0<3$$
57	56	a1i	$$⊢\phi \to 0<3$$
58	47 53 55 57 37	relogbcld	$$⊢\phi \to {\log }_{2}3\in ℝ$$
59		5nn0	$$⊢5\in {\mathbb{N}}_0$$
60	59	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
61	58 60	reexpcld	$$⊢\phi \to {{\log }_{2}3}^5\in ℝ$$
62		ceilcl	$$⊢{{\log }_{2}3}^5\in ℝ\to ⌈{{\log }_{2}3}^5⌉\in \mathbb{Z}$$
63	61 62	syl	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in \mathbb{Z}$$
64	63	zred	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in ℝ$$
65		0red	$$⊢\phi \to 0\in ℝ$$
66		9re	$$⊢9\in ℝ$$
67	66	a1i	$$⊢\phi \to 9\in ℝ$$
68	50	lep1d	$$⊢\phi \to 8\le 8+1$$
69		8p1e9	$$⊢8+1=9$$
70	69	a1i	$$⊢\phi \to 8+1=9$$
71	68 70	breqtrd	$$⊢\phi \to 8\le 9$$
72		2re	$$⊢2\in ℝ$$
73	72	a1i	$$⊢\phi \to 2\in ℝ$$
74		2pos	$$⊢0<2$$
75	74	a1i	$$⊢\phi \to 0<2$$
76		3pos	$$⊢0<3$$
77	76	a1i	$$⊢\phi \to 0<3$$
78	73 75 55 77 37	relogbcld	$$⊢\phi \to {\log }_{2}3\in ℝ$$
79	78 60	reexpcld	$$⊢\phi \to {{\log }_{2}3}^5\in ℝ$$
80	79 62	syl	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in \mathbb{Z}$$
81	80	zred	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in ℝ$$
82	55	leidd	$$⊢\phi \to 3\le 3$$
83	55 82	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}3}^5$$
84	67 79 83	ltled	$$⊢\phi \to 9\le {{\log }_{2}3}^5$$
85		ceilge	$$⊢{{\log }_{2}3}^5\in ℝ\to {{\log }_{2}3}^5\le ⌈{{\log }_{2}3}^5⌉$$
86	79 85	syl	$$⊢\phi \to {{\log }_{2}3}^5\le ⌈{{\log }_{2}3}^5⌉$$
87	67 79 81 84 86	letrd	$$⊢\phi \to 9\le ⌈{{\log }_{2}3}^5⌉$$
88	50 67 64 71 87	letrd	$$⊢\phi \to 8\le ⌈{{\log }_{2}3}^5⌉$$
89	65 50 64 52 88	ltletrd	$$⊢\phi \to 0<⌈{{\log }_{2}3}^5⌉$$
90	46 48 50 52 64 89 88	logblebd	$$⊢\phi \to {\log }_{2}8\le {\log }_2⌈{{\log }_{2}3}^5⌉$$
91	44 90	eqbrtrd	$$⊢\phi \to 3\le {\log }_2⌈{{\log }_{2}3}^5⌉$$
92	79 33	readdcld	$$⊢\phi \to {{\log }_{2}3}^5+1\in ℝ$$
93		1nn0	$$⊢1\in {\mathbb{N}}_0$$
94		6nn	$$⊢6\in \mathbb{N}$$
95	93 94	decnncl	$$⊢16\in \mathbb{N}$$
96	95	a1i	$$⊢\phi \to 16\in \mathbb{N}$$
97	96	nnred	$$⊢\phi \to 16\in ℝ$$
98		ceilm1lt	$$⊢{{\log }_{2}3}^5\in ℝ\to ⌈{{\log }_{2}3}^5⌉-1<{{\log }_{2}3}^5$$
99	79 98	syl	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉-1<{{\log }_{2}3}^5$$
100	81 33 79	ltsubaddd	$$⊢\phi \to \left(⌈{{\log }_{2}3}^5⌉-1<{{\log }_{2}3}^5\leftrightarrow ⌈{{\log }_{2}3}^5⌉<{{\log }_{2}3}^5+1\right)$$
101	99 100	mpbid	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉<{{\log }_{2}3}^5+1$$
102		3lexlogpow5ineq5	$$⊢{{\log }_{2}3}^5\le 15$$
103	102	a1i	$$⊢\phi \to {{\log }_{2}3}^5\le 15$$
104		5p1e6	$$⊢5+1=6$$
105		eqid	$$⊢15=15$$
106	93 59 104 105	decsuc	$$⊢15+1=16$$
107	106	a1i	$$⊢\phi \to 15+1=16$$
108	97	recnd	$$⊢\phi \to 16\in ℂ$$
109		1cnd	$$⊢\phi \to 1\in ℂ$$
110		5nn	$$⊢5\in \mathbb{N}$$
111	93 110	decnncl	$$⊢15\in \mathbb{N}$$
112	111	a1i	$$⊢\phi \to 15\in \mathbb{N}$$
113	112	nncnd	$$⊢\phi \to 15\in ℂ$$
114	108 109 113	subadd2d	$$⊢\phi \to \left(16-1=15\leftrightarrow 15+1=16\right)$$
115	107 114	mpbird	$$⊢\phi \to 16-1=15$$
116	115	eqcomd	$$⊢\phi \to 15=16-1$$
117	103 116	breqtrd	$$⊢\phi \to {{\log }_{2}3}^5\le 16-1$$
118		leaddsub	$$⊢\left({{\log }_{2}3}^5\in ℝ\wedge 1\in ℝ\wedge 16\in ℝ\right)\to \left({{\log }_{2}3}^5+1\le 16\leftrightarrow {{\log }_{2}3}^5\le 16-1\right)$$
119	79 33 97 118	syl3anc	$$⊢\phi \to \left({{\log }_{2}3}^5+1\le 16\leftrightarrow {{\log }_{2}3}^5\le 16-1\right)$$
120	117 119	mpbird	$$⊢\phi \to {{\log }_{2}3}^5+1\le 16$$
121	81 92 97 101 120	ltletrd	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉<16$$
122		eqid	$$⊢16=16$$
123		2exp4	$$⊢2^4=16$$
124	122 123	eqtr4i	$$⊢16=2^4$$
125	124	a1i	$$⊢\phi \to 16=2^4$$
126	121 125	breqtrd	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉<2^4$$
127	46	uzidd	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 2}$$
128	64 89	elrpd	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in {ℝ}^{+}$$
129		4z	$$⊢4\in \mathbb{Z}$$
130	129	a1i	$$⊢\phi \to 4\in \mathbb{Z}$$
131	32 130	rpexpcld	$$⊢\phi \to 2^4\in {ℝ}^{+}$$
132		logblt	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge ⌈{{\log }_{2}3}^5⌉\in {ℝ}^{+}\wedge 2^4\in {ℝ}^{+}\right)\to \left(⌈{{\log }_{2}3}^5⌉<2^4\leftrightarrow {\log }_2⌈{{\log }_{2}3}^5⌉<{\log }_2{2}^4\right)$$
133	127 128 131 132	syl3anc	$$⊢\phi \to \left(⌈{{\log }_{2}3}^5⌉<2^4\leftrightarrow {\log }_2⌈{{\log }_{2}3}^5⌉<{\log }_2{2}^4\right)$$
134	126 133	mpbid	$$⊢\phi \to {\log }_2⌈{{\log }_{2}3}^5⌉<{\log }_2{2}^4$$
135	32 37 130	relogbexpd	$$⊢\phi \to {\log }_2{2}^4=4$$
136	9	eqcomi	$$⊢4=3+1$$
137	136	a1i	$$⊢\phi \to 4=3+1$$
138	135 137	eqtrd	$$⊢\phi \to {\log }_2{2}^4=3+1$$
139	134 138	breqtrd	$$⊢\phi \to {\log }_2⌈{{\log }_{2}3}^5⌉<3+1$$
140	91 139	jca	$$⊢\phi \to \left(3\le {\log }_2⌈{{\log }_{2}3}^5⌉\wedge {\log }_2⌈{{\log }_{2}3}^5⌉<3+1\right)$$
141	73 75 55 57 37	relogbcld	$$⊢\phi \to {\log }_{2}3\in ℝ$$
142	141 60	reexpcld	$$⊢\phi \to {{\log }_{2}3}^5\in ℝ$$
143	142 62	syl	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in \mathbb{Z}$$
144	143	zred	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in ℝ$$
145		9pos	$$⊢0<9$$
146	145	a1i	$$⊢\phi \to 0<9$$
147	65 67 144 146 87	ltletrd	$$⊢\phi \to 0<⌈{{\log }_{2}3}^5⌉$$
148	73 75 144 147 37	relogbcld	$$⊢\phi \to {\log }_2⌈{{\log }_{2}3}^5⌉\in ℝ$$
149		flbi	$$⊢\left({\log }_2⌈{{\log }_{2}3}^5⌉\in ℝ\wedge 3\in \mathbb{Z}\right)\to \left(⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋=3\leftrightarrow \left(3\le {\log }_2⌈{{\log }_{2}3}^5⌉\wedge {\log }_2⌈{{\log }_{2}3}^5⌉<3+1\right)\right)$$
150	148 38 149	syl2anc	$$⊢\phi \to \left(⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋=3\leftrightarrow \left(3\le {\log }_2⌈{{\log }_{2}3}^5⌉\wedge {\log }_2⌈{{\log }_{2}3}^5⌉<3+1\right)\right)$$
151	140 150	mpbird	$$⊢\phi \to ⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋=3$$
152	151	oveq2d	$$⊢\phi \to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}=3^3$$
153	78	resqcld	$$⊢\phi \to {{\log }_{2}3}^2\in ℝ$$
154		3lexlogpow2ineq2	$$⊢\left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$
155	154	a1i	$$⊢\phi \to \left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$
156	155	simpld	$$⊢\phi \to 2<{{\log }_{2}3}^2$$
157	73 153 156	ltled	$$⊢\phi \to 2\le {{\log }_{2}3}^2$$
158	155	simprd	$$⊢\phi \to {{\log }_{2}3}^2<3$$
159		df-3	$$⊢3=2+1$$
160	159	a1i	$$⊢\phi \to 3=2+1$$
161	158 160	breqtrd	$$⊢\phi \to {{\log }_{2}3}^2<2+1$$
162	157 161	jca	$$⊢\phi \to \left(2\le {{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<2+1\right)$$
163	141	resqcld	$$⊢\phi \to {{\log }_{2}3}^2\in ℝ$$
164		flbi	$$⊢\left({{\log }_{2}3}^2\in ℝ\wedge 2\in \mathbb{Z}\right)\to \left(⌊{{\log }_{2}3}^2⌋=2\leftrightarrow \left(2\le {{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<2+1\right)\right)$$
165	163 46 164	syl2anc	$$⊢\phi \to \left(⌊{{\log }_{2}3}^2⌋=2\leftrightarrow \left(2\le {{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<2+1\right)\right)$$
166	162 165	mpbird	$$⊢\phi \to ⌊{{\log }_{2}3}^2⌋=2$$
167	166	oveq2d	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)=\left(1\dots 2\right)$$
168	167	prodeq1d	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)=\prod _{k=1}^2\left(3^k-1\right)$$
169		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
170	169 46	jca	$$⊢\phi \to \left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)$$
171		1le2	$$⊢1\le 2$$
172	171	a1i	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 1\le 2$$
173		eluz	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to \left(2\in {\mathbb{Z}}_{\ge 1}\leftrightarrow 1\le 2\right)$$
174	172 173	mpbird	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 2\in {\mathbb{Z}}_{\ge 1}$$
175	170 174	syl	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 1}$$
176		3cn	$$⊢3\in ℂ$$
177	176	a1i	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to 3\in ℂ$$
178		elfznn	$$⊢k\in \left(1\dots 2\right)\to k\in \mathbb{N}$$
179	178	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to k\in \mathbb{N}$$
180	179	nnnn0d	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to k\in {\mathbb{N}}_0$$
181	177 180	expcld	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to 3^k\in ℂ$$
182		1cnd	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to 1\in ℂ$$
183	181 182	subcld	$$⊢\left(\phi \wedge k\in \left(1\dots 2\right)\right)\to 3^k-1\in ℂ$$
184		oveq2	$$⊢k=2\to 3^k=3^2$$
185	184	oveq1d	$$⊢k=2\to 3^k-1=3^2-1$$
186	175 183 185	fprodm1	$$⊢\phi \to \prod _{k=1}^2\left(3^k-1\right)=\prod _{k=1}^{2-1}\left(3^k-1\right)\left(3^2-1\right)$$
187		2m1e1	$$⊢2-1=1$$
188	187	a1i	$$⊢\phi \to 2-1=1$$
189	188	oveq2d	$$⊢\phi \to \left(1\dots 2-1\right)=\left(1\dots 1\right)$$
190	189	prodeq1d	$$⊢\phi \to \prod _{k=1}^{2-1}\left(3^k-1\right)=\prod _{k=1}^1\left(3^k-1\right)$$
191	55	recnd	$$⊢\phi \to 3\in ℂ$$
192	93	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
193	191 192	expcld	$$⊢\phi \to 3^1\in ℂ$$
194	193 109	subcld	$$⊢\phi \to 3^1-1\in ℂ$$
195	169 194	jca	$$⊢\phi \to \left(1\in \mathbb{Z}\wedge 3^1-1\in ℂ\right)$$
196		oveq2	$$⊢k=1\to 3^k=3^1$$
197	196	oveq1d	$$⊢k=1\to 3^k-1=3^1-1$$
198	197	fprod1	$$⊢\left(1\in \mathbb{Z}\wedge 3^1-1\in ℂ\right)\to \prod _{k=1}^1\left(3^k-1\right)=3^1-1$$
199	195 198	syl	$$⊢\phi \to \prod _{k=1}^1\left(3^k-1\right)=3^1-1$$
200	190 199	eqtrd	$$⊢\phi \to \prod _{k=1}^{2-1}\left(3^k-1\right)=3^1-1$$
201	200	oveq1d	$$⊢\phi \to \prod _{k=1}^{2-1}\left(3^k-1\right)\left(3^2-1\right)=\left(3^1-1\right)\left(3^2-1\right)$$
202	186 201	eqtrd	$$⊢\phi \to \prod _{k=1}^2\left(3^k-1\right)=\left(3^1-1\right)\left(3^2-1\right)$$
203	168 202	eqtrd	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)=\left(3^1-1\right)\left(3^2-1\right)$$
204	152 203	oveq12d	$$⊢\phi \to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)=3^3\left(3^1-1\right)\left(3^2-1\right)$$
205		3nn0	$$⊢3\in {\mathbb{N}}_0$$
206	205	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
207	55 206	reexpcld	$$⊢\phi \to 3^3\in ℝ$$
208	55 192	reexpcld	$$⊢\phi \to 3^1\in ℝ$$
209	208 33	resubcld	$$⊢\phi \to 3^1-1\in ℝ$$
210	55	resqcld	$$⊢\phi \to 3^2\in ℝ$$
211	210 33	resubcld	$$⊢\phi \to 3^2-1\in ℝ$$
212	209 211	remulcld	$$⊢\phi \to \left(3^1-1\right)\left(3^2-1\right)\in ℝ$$
213	207 212	remulcld	$$⊢\phi \to 3^3\left(3^1-1\right)\left(3^2-1\right)\in ℝ$$
214		9nn0	$$⊢9\in {\mathbb{N}}_0$$
215	214	a1i	$$⊢\phi \to 9\in {\mathbb{N}}_0$$
216	73 215	reexpcld	$$⊢\phi \to 2^9\in ℝ$$
217	216 33	resubcld	$$⊢\phi \to 2^9-1\in ℝ$$
218		elnnz	$$⊢⌈{{\log }_{2}3}^5⌉\in \mathbb{N}\leftrightarrow \left(⌈{{\log }_{2}3}^5⌉\in \mathbb{Z}\wedge 0<⌈{{\log }_{2}3}^5⌉\right)$$
219	143 147 218	sylanbrc	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in \mathbb{N}$$
220	219	orcd	$$⊢\phi \to \left(⌈{{\log }_{2}3}^5⌉\in \mathbb{N}\vee ⌈{{\log }_{2}3}^5⌉=0\right)$$
221		elnn0	$$⊢⌈{{\log }_{2}3}^5⌉\in {\mathbb{N}}_0\leftrightarrow \left(⌈{{\log }_{2}3}^5⌉\in \mathbb{N}\vee ⌈{{\log }_{2}3}^5⌉=0\right)$$
222	221	a1i	$$⊢\phi \to \left(⌈{{\log }_{2}3}^5⌉\in {\mathbb{N}}_0\leftrightarrow \left(⌈{{\log }_{2}3}^5⌉\in \mathbb{N}\vee ⌈{{\log }_{2}3}^5⌉=0\right)\right)$$
223	220 222	mpbird	$$⊢\phi \to ⌈{{\log }_{2}3}^5⌉\in {\mathbb{N}}_0$$
224	73 223	reexpcld	$$⊢\phi \to 2^{⌈{{\log }_{2}3}^5⌉}\in ℝ$$
225		8cn	$$⊢8\in ℂ$$
226		2cn	$$⊢2\in ℂ$$
227		8t2e16	$$⊢8\cdot 2=16$$
228	225 226 227	mulcomli	$$⊢2\cdot 8=16$$
229	228	a1i	$$⊢\phi \to 2\cdot 8=16$$
230	229	oveq2d	$$⊢\phi \to 272\cdot 8=27\cdot 16$$
231		6nn0	$$⊢6\in {\mathbb{N}}_0$$
232	93 231	deccl	$$⊢16\in {\mathbb{N}}_0$$
233		2nn0	$$⊢2\in {\mathbb{N}}_0$$
234		7nn0	$$⊢7\in {\mathbb{N}}_0$$
235		eqid	$$⊢27=27$$
236	93 93	deccl	$$⊢11\in {\mathbb{N}}_0$$
237		0nn0	$$⊢0\in {\mathbb{N}}_0$$
238	233	dec0h	$$⊢2=02$$
239		eqid	$$⊢11=11$$
240	232	nn0cni	$$⊢16\in ℂ$$
241	240	mul02i	$$⊢0\cdot 16=0$$
242		ax-1cn	$$⊢1\in ℂ$$
243	176 242 9	addcomli	$$⊢1+3=4$$
244	241 243	oveq12i	$$⊢0\cdot 16+1+3=0+4$$
245		4cn	$$⊢4\in ℂ$$
246	245	addlidi	$$⊢0+4=4$$
247	244 246	eqtri	$$⊢0\cdot 16+1+3=4$$
248	93	dec0h	$$⊢1=01$$
249		2t1e2	$$⊢2\cdot 1=2$$
250		0p1e1	$$⊢0+1=1$$
251	249 250	oveq12i	$$⊢2\cdot 1+0+1=2+1$$
252		2p1e3	$$⊢2+1=3$$
253	251 252	eqtri	$$⊢2\cdot 1+0+1=3$$
254		6cn	$$⊢6\in ℂ$$
255		6t2e12	$$⊢6\cdot 2=12$$
256	254 226 255	mulcomli	$$⊢2\cdot 6=12$$
257	93 233 252 256	decsuc	$$⊢2\cdot 6+1=13$$
258	93 231 237 93 122 248 233 205 93 253 257	decma2c	$$⊢2\cdot 16+1=33$$
259	237 233 93 93 238 239 232 205 205 247 258	decmac	$$⊢2\cdot 16+11=43$$
260		4nn0	$$⊢4\in {\mathbb{N}}_0$$
261		7cn	$$⊢7\in ℂ$$
262	261	mulridi	$$⊢7\cdot 1=7$$
263	262	oveq1i	$$⊢7\cdot 1+4=7+4$$
264		7p4e11	$$⊢7+4=11$$
265	263 264	eqtri	$$⊢7\cdot 1+4=11$$
266		7t6e42	$$⊢7\cdot 6=42$$
267	234 93 231 122 233 260 265 266	decmul2c	$$⊢7\cdot 16=112$$
268	232 233 234 235 233 236 259 267	decmul1c	$$⊢27\cdot 16=432$$
269	268	a1i	$$⊢\phi \to 27\cdot 16=432$$
270	230 269	eqtrd	$$⊢\phi \to 272\cdot 8=432$$
271	260 205	deccl	$$⊢43\in {\mathbb{N}}_0$$
272	59 93	deccl	$$⊢51\in {\mathbb{N}}_0$$
273		2lt10	$$⊢2<10$$
274		3lt10	$$⊢3<10$$
275		4lt5	$$⊢4<5$$
276	260 59 205 93 274 275	decltc	$$⊢43<51$$
277	271 272 233 93 273 276	decltc	$$⊢432<511$$
278	277	a1i	$$⊢\phi \to 432<511$$
279	270 278	eqbrtrd	$$⊢\phi \to 272\cdot 8<511$$
280		3exp3	$$⊢3^3=27$$
281	280	a1i	$$⊢\phi \to 3^3=27$$
282	281	eqcomd	$$⊢\phi \to 27=3^3$$
283	191	exp1d	$$⊢\phi \to 3^1=3$$
284	283	oveq1d	$$⊢\phi \to 3^1-1=3-1$$
285		3m1e2	$$⊢3-1=2$$
286	285	a1i	$$⊢\phi \to 3-1=2$$
287	284 286	eqtr2d	$$⊢\phi \to 2=3^1-1$$
288		sq3	$$⊢3^2=9$$
289	288	a1i	$$⊢\phi \to 3^2=9$$
290	289	oveq1d	$$⊢\phi \to 3^2-1=9-1$$
291		9m1e8	$$⊢9-1=8$$
292	291	a1i	$$⊢\phi \to 9-1=8$$
293	290 292	eqtr2d	$$⊢\phi \to 8=3^2-1$$
294	287 293	oveq12d	$$⊢\phi \to 2\cdot 8=\left(3^1-1\right)\left(3^2-1\right)$$
295	282 294	oveq12d	$$⊢\phi \to 272\cdot 8=3^3\left(3^1-1\right)\left(3^2-1\right)$$
296		df-9	$$⊢9=8+1$$
297	296	a1i	$$⊢\phi \to 9=8+1$$
298	297	oveq2d	$$⊢\phi \to 2^9=2^{8+1}$$
299	287 194	eqeltrd	$$⊢\phi \to 2\in ℂ$$
300		8nn0	$$⊢8\in {\mathbb{N}}_0$$
301	300	a1i	$$⊢\phi \to 8\in {\mathbb{N}}_0$$
302	299 192 301	expaddd	$$⊢\phi \to 2^{8+1}=2^8{2}^1$$
303	298 302	eqtrd	$$⊢\phi \to 2^9=2^8{2}^1$$
304		2exp8	$$⊢2^8=256$$
305	304	a1i	$$⊢\phi \to 2^8=256$$
306	305	oveq1d	$$⊢\phi \to 2^8{2}^1=2562^1$$
307	299	exp1d	$$⊢\phi \to 2^1=2$$
308	307	oveq2d	$$⊢\phi \to 2562^1=256\cdot 2$$
309	306 308	eqtrd	$$⊢\phi \to 2^8{2}^1=256\cdot 2$$
310	233 59	deccl	$$⊢25\in {\mathbb{N}}_0$$
311		eqid	$$⊢256=256$$
312		eqid	$$⊢25=25$$
313		2t2e4	$$⊢2\cdot 2=4$$
314	313 250	oveq12i	$$⊢2\cdot 2+0+1=4+1$$
315		4p1e5	$$⊢4+1=5$$
316	314 315	eqtri	$$⊢2\cdot 2+0+1=5$$
317		5t2e10	$$⊢5\cdot 2=10$$
318	93 237 250 317	decsuc	$$⊢5\cdot 2+1=11$$
319	233 59 237 93 312 248 233 93 93 316 318	decmac	$$⊢25\cdot 2+1=51$$
320	233 310 231 311 233 93 319 255	decmul1c	$$⊢256\cdot 2=512$$
321	320	a1i	$$⊢\phi \to 256\cdot 2=512$$
322	309 321	eqtrd	$$⊢\phi \to 2^8{2}^1=512$$
323	303 322	eqtrd	$$⊢\phi \to 2^9=512$$
324	323	oveq1d	$$⊢\phi \to 2^9-1=512-1$$
325		1p1e2	$$⊢1+1=2$$
326		eqid	$$⊢511=511$$
327	272 93 325 326	decsuc	$$⊢511+1=512$$
328	272 233	deccl	$$⊢512\in {\mathbb{N}}_0$$
329	328	nn0cni	$$⊢512\in ℂ$$
330	272 93	deccl	$$⊢511\in {\mathbb{N}}_0$$
331	330	nn0cni	$$⊢511\in ℂ$$
332	329 242 331	subadd2i	$$⊢512-1=511\leftrightarrow 511+1=512$$
333	327 332	mpbir	$$⊢512-1=511$$
334	333	a1i	$$⊢\phi \to 512-1=511$$
335	324 334	eqtr2d	$$⊢\phi \to 511=2^9-1$$
336	279 295 335	3brtr3d	$$⊢\phi \to 3^3\left(3^1-1\right)\left(3^2-1\right)<2^9-1$$
337	216	ltm1d	$$⊢\phi \to 2^9-1<2^9$$
338	215	nn0zd	$$⊢\phi \to 9\in \mathbb{Z}$$
339	73 338 143 35	leexp2d	$$⊢\phi \to \left(9\le ⌈{{\log }_{2}3}^5⌉\leftrightarrow 2^9\le 2^{⌈{{\log }_{2}3}^5⌉}\right)$$
340	87 339	mpbid	$$⊢\phi \to 2^9\le 2^{⌈{{\log }_{2}3}^5⌉}$$
341	217 216 224 337 340	ltletrd	$$⊢\phi \to 2^9-1<2^{⌈{{\log }_{2}3}^5⌉}$$
342	213 217 224 336 341	lttrd	$$⊢\phi \to 3^3\left(3^1-1\right)\left(3^2-1\right)<2^{⌈{{\log }_{2}3}^5⌉}$$
343	204 342	eqbrtrd	$$⊢\phi \to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)<2^{⌈{{\log }_{2}3}^5⌉}$$
344	343	adantr	$$⊢\left(\phi \wedge 3=N\right)\to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(3^k-1\right)<2^{⌈{{\log }_{2}3}^5⌉}$$
345	30 344	eqbrtrd	$$⊢\left(\phi \wedge 3=N\right)\to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(N^k-1\right)<2^{⌈{{\log }_{2}3}^5⌉}$$
346		simpr	$$⊢\left(\phi \wedge 3=N\right)\to 3=N$$
347		oveq2	$$⊢3=N\to {\log }_{2}3={\log }_{2}N$$
348	347	adantl	$$⊢\left(\phi \wedge 3=N\right)\to {\log }_{2}3={\log }_{2}N$$
349	348	oveq1d	$$⊢\left(\phi \wedge 3=N\right)\to {{\log }_{2}3}^5={{\log }_{2}N}^5$$
350	349	fveq2d	$$⊢\left(\phi \wedge 3=N\right)\to ⌈{{\log }_{2}3}^5⌉=⌈{{\log }_{2}N}^5⌉$$
351	3	a1i	$$⊢\left(\phi \wedge 3=N\right)\to B=⌈{{\log }_{2}N}^5⌉$$
352	351	eqcomd	$$⊢\left(\phi \wedge 3=N\right)\to ⌈{{\log }_{2}N}^5⌉=B$$
353	350 352	eqtrd	$$⊢\left(\phi \wedge 3=N\right)\to ⌈{{\log }_{2}3}^5⌉=B$$
354	353	oveq2d	$$⊢\left(\phi \wedge 3=N\right)\to {\log }_2⌈{{\log }_{2}3}^5⌉={\log }_{2}B$$
355	354	fveq2d	$$⊢\left(\phi \wedge 3=N\right)\to ⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋=⌊{\log }_{2}B⌋$$
356	346 355	oveq12d	$$⊢\left(\phi \wedge 3=N\right)\to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}=N^{⌊{\log }_{2}B⌋}$$
357	346	oveq2d	$$⊢\left(\phi \wedge 3=N\right)\to {\log }_{2}3={\log }_{2}N$$
358	357	oveq1d	$$⊢\left(\phi \wedge 3=N\right)\to {{\log }_{2}3}^2={{\log }_{2}N}^2$$
359	358	fveq2d	$$⊢\left(\phi \wedge 3=N\right)\to ⌊{{\log }_{2}3}^2⌋=⌊{{\log }_{2}N}^2⌋$$
360	359	oveq2d	$$⊢\left(\phi \wedge 3=N\right)\to \left(1\dots ⌊{{\log }_{2}3}^2⌋\right)=\left(1\dots ⌊{{\log }_{2}N}^2⌋\right)$$
361	360	prodeq1d	$$⊢\left(\phi \wedge 3=N\right)\to \prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(N^k-1\right)=\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
362	356 361	oveq12d	$$⊢\left(\phi \wedge 3=N\right)\to 3^{⌊{\log }_2⌈{{\log }_{2}3}^5⌉⌋}\prod _{k=1}^{⌊{{\log }_{2}3}^2⌋}\left(N^k-1\right)=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
363	350	oveq2d	$$⊢\left(\phi \wedge 3=N\right)\to 2^{⌈{{\log }_{2}3}^5⌉}=2^{⌈{{\log }_{2}N}^5⌉}$$
364	345 362 363	3brtr3d	$$⊢\left(\phi \wedge 3=N\right)\to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)<2^{⌈{{\log }_{2}N}^5⌉}$$
365	2	a1i	$$⊢\left(\phi \wedge 3=N\right)\to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
366	365	eqcomd	$$⊢\left(\phi \wedge 3=N\right)\to N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)=A$$
367	3	oveq2i	$$⊢2^B=2^{⌈{{\log }_{2}N}^5⌉}$$
368	367	a1i	$$⊢\left(\phi \wedge 3=N\right)\to 2^B=2^{⌈{{\log }_{2}N}^5⌉}$$
369	368	eqcomd	$$⊢\left(\phi \wedge 3=N\right)\to 2^{⌈{{\log }_{2}N}^5⌉}=2^B$$
370	364 366 369	3brtr3d	$$⊢\left(\phi \wedge 3=N\right)\to A<2^B$$
371	370	ex	$$⊢\phi \to \left(3=N\to A<2^B\right)$$
372		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
373	1 372	syl	$$⊢\phi \to 3\le N$$
374	14	zred	$$⊢\phi \to N\in ℝ$$
375	55 374	leloed	$$⊢\phi \to \left(3\le N\leftrightarrow \left(3<N\vee 3=N\right)\right)$$
376	373 375	mpbid	$$⊢\phi \to \left(3<N\vee 3=N\right)$$
377	23 371 376	mpjaod	$$⊢\phi \to A<2^B$$