Theorem aks4d1p2

Description: Technical lemma for existence of non-divisor. (Contributed by metakunt, 27-Oct-2024)

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

Proof

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