Theorem aks4d1p1p3

Description: Bound of a ceiling of the binary logarithm to the fifth power. (Contributed by metakunt, 19-Aug-2024)

	Ref	Expression
Hypotheses	aks4d1p1p3.1	$$⊢\phi \to N\in \mathbb{N}$$
	aks4d1p1p3.2	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p1p3.3	$$⊢\phi \to 3\le N$$
Assertion	aks4d1p1p3	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p3.1	$$⊢\phi \to N\in \mathbb{N}$$
2		aks4d1p1p3.2	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
3		aks4d1p1p3.3	$$⊢\phi \to 3\le N$$
4		2re	$$⊢2\in ℝ$$
5	4	a1i	$$⊢\phi \to 2\in ℝ$$
6		2pos	$$⊢0<2$$
7	6	a1i	$$⊢\phi \to 0<2$$
8	1	nnred	$$⊢\phi \to N\in ℝ$$
9	1	nngt0d	$$⊢\phi \to 0<N$$
10		1red	$$⊢\phi \to 1\in ℝ$$
11		1lt2	$$⊢1<2$$
12	11	a1i	$$⊢\phi \to 1<2$$
13	10 12	ltned	$$⊢\phi \to 1\ne 2$$
14	13	necomd	$$⊢\phi \to 2\ne 1$$
15	5 7 8 9 14	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
16		5nn0	$$⊢5\in {\mathbb{N}}_0$$
17	16	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
18	15 17	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
19		ceilcl	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
20	18 19	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
21	20	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
22	2	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
23	22	eleq1d	$$⊢\phi \to \left(B\in ℝ\leftrightarrow ⌈{{\log }_{2}N}^5⌉\in ℝ\right)$$
24	21 23	mpbird	$$⊢\phi \to B\in ℝ$$
25		0red	$$⊢\phi \to 0\in ℝ$$
26		7re	$$⊢7\in ℝ$$
27	26	a1i	$$⊢\phi \to 7\in ℝ$$
28		7pos	$$⊢0<7$$
29	28	a1i	$$⊢\phi \to 0<7$$
30	8 3	3lexlogpow5ineq3	$$⊢\phi \to 7<{{\log }_{2}N}^5$$
31		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
32	18 31	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
33	27 18 21 30 32	ltletrd	$$⊢\phi \to 7<⌈{{\log }_{2}N}^5⌉$$
34	22	eqcomd	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉=B$$
35	33 34	breqtrd	$$⊢\phi \to 7<B$$
36	25 27 24 29 35	lttrd	$$⊢\phi \to 0<B$$
37	5 7 24 36 14	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
38	37	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
39	38	zred	$$⊢\phi \to ⌊{\log }_{2}B⌋\in ℝ$$
40	18 10	readdcld	$$⊢\phi \to {{\log }_{2}N}^5+1\in ℝ$$
41	18	ltp1d	$$⊢\phi \to {{\log }_{2}N}^5<{{\log }_{2}N}^5+1$$
42	27 18 40 30 41	lttrd	$$⊢\phi \to 7<{{\log }_{2}N}^5+1$$
43	25 27 40 29 42	lttrd	$$⊢\phi \to 0<{{\log }_{2}N}^5+1$$
44	5 7 40 43 14	relogbcld	$$⊢\phi \to {\log }_2\left({{\log }_{2}N}^5+1\right)\in ℝ$$
45		flle	$$⊢{\log }_{2}B\in ℝ\to ⌊{\log }_{2}B⌋\le {\log }_{2}B$$
46	37 45	syl	$$⊢\phi \to ⌊{\log }_{2}B⌋\le {\log }_{2}B$$
47		ceilm1lt	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉-1<{{\log }_{2}N}^5$$
48	18 47	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉-1<{{\log }_{2}N}^5$$
49	21 10 18	ltsubaddd	$$⊢\phi \to \left(⌈{{\log }_{2}N}^5⌉-1<{{\log }_{2}N}^5\leftrightarrow ⌈{{\log }_{2}N}^5⌉<{{\log }_{2}N}^5+1\right)$$
50	48 49	mpbid	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉<{{\log }_{2}N}^5+1$$
51	22 50	eqbrtrd	$$⊢\phi \to B<{{\log }_{2}N}^5+1$$
52		2z	$$⊢2\in \mathbb{Z}$$
53	52	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
54	53	uzidd	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 2}$$
55	24 36	elrpd	$$⊢\phi \to B\in {ℝ}^{+}$$
56	40 43	elrpd	$$⊢\phi \to {{\log }_{2}N}^5+1\in {ℝ}^{+}$$
57		logblt	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge B\in {ℝ}^{+}\wedge {{\log }_{2}N}^5+1\in {ℝ}^{+}\right)\to \left(B<{{\log }_{2}N}^5+1\leftrightarrow {\log }_{2}B<{\log }_2\left({{\log }_{2}N}^5+1\right)\right)$$
58	54 55 56 57	syl3anc	$$⊢\phi \to \left(B<{{\log }_{2}N}^5+1\leftrightarrow {\log }_{2}B<{\log }_2\left({{\log }_{2}N}^5+1\right)\right)$$
59	51 58	mpbid	$$⊢\phi \to {\log }_{2}B<{\log }_2\left({{\log }_{2}N}^5+1\right)$$
60	39 37 44 46 59	lelttrd	$$⊢\phi \to ⌊{\log }_{2}B⌋<{\log }_2\left({{\log }_{2}N}^5+1\right)$$
61		3re	$$⊢3\in ℝ$$
62	61	a1i	$$⊢\phi \to 3\in ℝ$$
63		1lt3	$$⊢1<3$$
64	63	a1i	$$⊢\phi \to 1<3$$
65	10 62 8 64 3	ltletrd	$$⊢\phi \to 1<N$$
66	8 65 39 44	cxpltd	$$⊢\phi \to \left(⌊{\log }_{2}B⌋<{\log }_2\left({{\log }_{2}N}^5+1\right)\leftrightarrow N^{⌊{\log }_{2}B⌋}<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}\right)$$
67	60 66	mpbid	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}<N^{{\log }_2\left({{\log }_{2}N}^5+1\right)}$$