Theorem aks4d1lem1

Description: Technical lemma to reduce proof size. (Contributed by metakunt, 14-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1lem1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1lem1.2	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
Assertion	aks4d1lem1	$$⊢\phi \to \left(B\in \mathbb{N}\wedge 9<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1lem1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1lem1.2	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
3		2re	$$⊢2\in ℝ$$
4	3	a1i	$$⊢\phi \to 2\in ℝ$$
5		2pos	$$⊢0<2$$
6	5	a1i	$$⊢\phi \to 0<2$$
7		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
8	1 7	syl	$$⊢\phi \to N\in \mathbb{Z}$$
9	8	zred	$$⊢\phi \to N\in ℝ$$
10		0red	$$⊢\phi \to 0\in ℝ$$
11		3re	$$⊢3\in ℝ$$
12	11	a1i	$$⊢\phi \to 3\in ℝ$$
13		3pos	$$⊢0<3$$
14	13	a1i	$$⊢\phi \to 0<3$$
15		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
16	1 15	syl	$$⊢\phi \to 3\le N$$
17	10 12 9 14 16	ltletrd	$$⊢\phi \to 0<N$$
18		1red	$$⊢\phi \to 1\in ℝ$$
19		1lt2	$$⊢1<2$$
20	19	a1i	$$⊢\phi \to 1<2$$
21	18 20	ltned	$$⊢\phi \to 1\ne 2$$
22	21	necomd	$$⊢\phi \to 2\ne 1$$
23	4 6 9 17 22	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
24		5nn0	$$⊢5\in {\mathbb{N}}_0$$
25	24	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
26	23 25	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
27	26	ceilcld	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
28		9re	$$⊢9\in ℝ$$
29	28	a1i	$$⊢\phi \to 9\in ℝ$$
30	27	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
31		9pos	$$⊢0<9$$
32	31	a1i	$$⊢\phi \to 0<9$$
33	9 16	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}N}^5$$
34		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
35	26 34	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
36	29 26 30 33 35	ltletrd	$$⊢\phi \to 9<⌈{{\log }_{2}N}^5⌉$$
37	10 29 30 32 36	lttrd	$$⊢\phi \to 0<⌈{{\log }_{2}N}^5⌉$$
38	27 37	jca	$$⊢\phi \to \left(⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}\wedge 0<⌈{{\log }_{2}N}^5⌉\right)$$
39		elnnz	$$⊢⌈{{\log }_{2}N}^5⌉\in \mathbb{N}\leftrightarrow \left(⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}\wedge 0<⌈{{\log }_{2}N}^5⌉\right)$$
40	38 39	sylibr	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{N}$$
41	2	eleq1i	$$⊢B\in \mathbb{N}\leftrightarrow ⌈{{\log }_{2}N}^5⌉\in \mathbb{N}$$
42	40 41	sylibr	$$⊢\phi \to B\in \mathbb{N}$$
43	2	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
44	36 43	breqtrrd	$$⊢\phi \to 9<B$$
45	42 44	jca	$$⊢\phi \to \left(B\in \mathbb{N}\wedge 9<B\right)$$