Theorem aks4d1p6

Description: The maximal prime power exponent is smaller than the binary logarithm floor of B . (Contributed by metakunt, 30-Oct-2024)

	Ref	Expression
Hypotheses	aks4d1p6.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1p6.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p6.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p6.4	$$⊢R=inf\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
	aks4d1p6.5	$$⊢\phi \to P\in \mathbb{P}$$
	aks4d1p6.6	$$⊢\phi \to P\parallel R$$
	aks4d1p6.7	$$⊢K=P\mathrm{pCnt}R$$
Assertion	aks4d1p6	$$⊢\phi \to K\le ⌊{\log }_{2}B⌋$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p6.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1p6.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p6.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		aks4d1p6.4	$$⊢R=inf\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
5		aks4d1p6.5	$$⊢\phi \to P\in \mathbb{P}$$
6		aks4d1p6.6	$$⊢\phi \to P\parallel R$$
7		aks4d1p6.7	$$⊢K=P\mathrm{pCnt}R$$
8	7	a1i	$$⊢\phi \to K=P\mathrm{pCnt}R$$
9	1 2 3 4	aks4d1p4	$$⊢\phi \to \left(R\in \left(1\dots B\right)\wedge \neg R\parallel A\right)$$
10	9	simpld	$$⊢\phi \to R\in \left(1\dots B\right)$$
11		elfznn	$$⊢R\in \left(1\dots B\right)\to R\in \mathbb{N}$$
12	10 11	syl	$$⊢\phi \to R\in \mathbb{N}$$
13	5 12	pccld	$$⊢\phi \to P\mathrm{pCnt}R\in {\mathbb{N}}_0$$
14	8 13	eqeltrd	$$⊢\phi \to K\in {\mathbb{N}}_0$$
15	14	nn0zd	$$⊢\phi \to K\in \mathbb{Z}$$
16	15	zred	$$⊢\phi \to K\in ℝ$$
17		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
18	5 17	syl	$$⊢\phi \to P\in \mathbb{N}$$
19	18	nnred	$$⊢\phi \to P\in ℝ$$
20	18	nngt0d	$$⊢\phi \to 0<P$$
21	3	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
22		2re	$$⊢2\in ℝ$$
23	22	a1i	$$⊢\phi \to 2\in ℝ$$
24		2pos	$$⊢0<2$$
25	24	a1i	$$⊢\phi \to 0<2$$
26		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
27	1 26	syl	$$⊢\phi \to N\in \mathbb{Z}$$
28	27	zred	$$⊢\phi \to N\in ℝ$$
29		0red	$$⊢\phi \to 0\in ℝ$$
30		3re	$$⊢3\in ℝ$$
31	30	a1i	$$⊢\phi \to 3\in ℝ$$
32		3pos	$$⊢0<3$$
33	32	a1i	$$⊢\phi \to 0<3$$
34		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
35	1 34	syl	$$⊢\phi \to 3\le N$$
36	29 31 28 33 35	ltletrd	$$⊢\phi \to 0<N$$
37		1red	$$⊢\phi \to 1\in ℝ$$
38		1lt2	$$⊢1<2$$
39	38	a1i	$$⊢\phi \to 1<2$$
40	37 39	ltned	$$⊢\phi \to 1\ne 2$$
41	40	necomd	$$⊢\phi \to 2\ne 1$$
42	23 25 28 36 41	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
43		5nn0	$$⊢5\in {\mathbb{N}}_0$$
44	43	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
45	42 44	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
46		ceilcl	$$⊢{{\log }_{2}N}^5\in ℝ\to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
47	45 46	syl	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
48	21 47	eqeltrd	$$⊢\phi \to B\in \mathbb{Z}$$
49	48	zred	$$⊢\phi \to B\in ℝ$$
50		9re	$$⊢9\in ℝ$$
51	50	a1i	$$⊢\phi \to 9\in ℝ$$
52		9pos	$$⊢0<9$$
53	52	a1i	$$⊢\phi \to 0<9$$
54	28 35	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}N}^5$$
55	29 51 45 53 54	lttrd	$$⊢\phi \to 0<{{\log }_{2}N}^5$$
56		ceilge	$$⊢{{\log }_{2}N}^5\in ℝ\to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
57	45 56	syl	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
58	57 21	breqtrrd	$$⊢\phi \to {{\log }_{2}N}^5\le B$$
59	29 45 49 55 58	ltletrd	$$⊢\phi \to 0<B$$
60	48 59	jca	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge 0<B\right)$$
61		elnnz	$$⊢B\in \mathbb{N}\leftrightarrow \left(B\in \mathbb{Z}\wedge 0<B\right)$$
62	60 61	sylibr	$$⊢\phi \to B\in \mathbb{N}$$
63	62	nnred	$$⊢\phi \to B\in ℝ$$
64	62	nngt0d	$$⊢\phi \to 0<B$$
65		2z	$$⊢2\in \mathbb{Z}$$
66	65	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
67	66	zred	$$⊢\phi \to 2\in ℝ$$
68		prmuz2	$$⊢P\in \mathbb{P}\to P\in {\mathbb{Z}}_{\ge 2}$$
69	5 68	syl	$$⊢\phi \to P\in {\mathbb{Z}}_{\ge 2}$$
70		eluzle	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to 2\le P$$
71	69 70	syl	$$⊢\phi \to 2\le P$$
72	37 67 19 39 71	ltletrd	$$⊢\phi \to 1<P$$
73	37 72	ltned	$$⊢\phi \to 1\ne P$$
74	73	necomd	$$⊢\phi \to P\ne 1$$
75	19 20 63 64 74	relogbcld	$$⊢\phi \to {\log }_{P}B\in ℝ$$
76	67 25 63 64 41	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
77	18	nnrpd	$$⊢\phi \to P\in {ℝ}^{+}$$
78	77	rpcnd	$$⊢\phi \to P\in ℂ$$
79	77	rpne0d	$$⊢\phi \to P\ne 0$$
80	78 79 15	cxpexpzd	$$⊢\phi \to P^K=P^K$$
81	19 14	reexpcld	$$⊢\phi \to P^K\in ℝ$$
82	12	nnred	$$⊢\phi \to R\in ℝ$$
83	8	oveq2d	$$⊢\phi \to P^K=P^{P\mathrm{pCnt}R}$$
84		pcdvds	$$⊢\left(P\in \mathbb{P}\wedge R\in \mathbb{N}\right)\to P^{P\mathrm{pCnt}R}\parallel R$$
85	5 12 84	syl2anc	$$⊢\phi \to P^{P\mathrm{pCnt}R}\parallel R$$
86	18	nnzd	$$⊢\phi \to P\in \mathbb{Z}$$
87		zexpcl	$$⊢\left(P\in \mathbb{Z}\wedge P\mathrm{pCnt}R\in {\mathbb{N}}_0\right)\to P^{P\mathrm{pCnt}R}\in \mathbb{Z}$$
88	86 13 87	syl2anc	$$⊢\phi \to P^{P\mathrm{pCnt}R}\in \mathbb{Z}$$
89		dvdsle	$$⊢\left(P^{P\mathrm{pCnt}R}\in \mathbb{Z}\wedge R\in \mathbb{N}\right)\to \left(P^{P\mathrm{pCnt}R}\parallel R\to P^{P\mathrm{pCnt}R}\le R\right)$$
90	88 12 89	syl2anc	$$⊢\phi \to \left(P^{P\mathrm{pCnt}R}\parallel R\to P^{P\mathrm{pCnt}R}\le R\right)$$
91	85 90	mpd	$$⊢\phi \to P^{P\mathrm{pCnt}R}\le R$$
92	83 91	eqbrtrd	$$⊢\phi \to P^K\le R$$
93		elfzle2	$$⊢R\in \left(1\dots B\right)\to R\le B$$
94	10 93	syl	$$⊢\phi \to R\le B$$
95	81 82 63 92 94	letrd	$$⊢\phi \to P^K\le B$$
96	79 74	nelprd	$$⊢\phi \to \neg P\in \left\{0,1\right\}$$
97	78 96	eldifd	$$⊢\phi \to P\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
98	63	recnd	$$⊢\phi \to B\in ℂ$$
99	29 64	ltned	$$⊢\phi \to 0\ne B$$
100	99	necomd	$$⊢\phi \to B\ne 0$$
101	100	neneqd	$$⊢\phi \to \neg B=0$$
102		elsng	$$⊢B\in \mathbb{N}\to \left(B\in \left\{0\right\}\leftrightarrow B=0\right)$$
103	62 102	syl	$$⊢\phi \to \left(B\in \left\{0\right\}\leftrightarrow B=0\right)$$
104	101 103	mtbird	$$⊢\phi \to \neg B\in \left\{0\right\}$$
105	98 104	eldifd	$$⊢\phi \to B\in \left(ℂ\setminus \left\{0\right\}\right)$$
106		cxplogb	$$⊢\left(P\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge B\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to P^{{\log }_{P}B}=B$$
107	97 105 106	syl2anc	$$⊢\phi \to P^{{\log }_{P}B}=B$$
108	95 107	breqtrrd	$$⊢\phi \to P^K\le P^{{\log }_{P}B}$$
109	80 108	eqbrtrd	$$⊢\phi \to P^K\le P^{{\log }_{P}B}$$
110	77	rpred	$$⊢\phi \to P\in ℝ$$
111	37 67 110 39 71	ltletrd	$$⊢\phi \to 1<P$$
112	110 111 16 75	cxpled	$$⊢\phi \to \left(K\le {\log }_{P}B\leftrightarrow P^K\le P^{{\log }_{P}B}\right)$$
113	109 112	mpbird	$$⊢\phi \to K\le {\log }_{P}B$$
114	23 39	rplogcld	$$⊢\phi \to \log 2\in {ℝ}^{+}$$
115	110 111	rplogcld	$$⊢\phi \to \log P\in {ℝ}^{+}$$
116	62	nnrpd	$$⊢\phi \to B\in {ℝ}^{+}$$
117	116	relogcld	$$⊢\phi \to \log B\in ℝ$$
118	62	nnge1d	$$⊢\phi \to 1\le B$$
119	63 118	logge0d	$$⊢\phi \to 0\le \log B$$
120		2rp	$$⊢2\in {ℝ}^{+}$$
121	120	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
122	121 77	logled	$$⊢\phi \to \left(2\le P\leftrightarrow \log 2\le \log P\right)$$
123	71 122	mpbid	$$⊢\phi \to \log 2\le \log P$$
124	114 115 117 119 123	lediv2ad	$$⊢\phi \to \frac{\log B}{\log P}\le \frac{\log B}{\log 2}$$
125		relogbval	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge B\in {ℝ}^{+}\right)\to {\log }_{P}B=\frac{\log B}{\log P}$$
126	69 116 125	syl2anc	$$⊢\phi \to {\log }_{P}B=\frac{\log B}{\log P}$$
127	126	eqcomd	$$⊢\phi \to \frac{\log B}{\log P}={\log }_{P}B$$
128	66	uzidd	$$⊢\phi \to 2\in {\mathbb{Z}}_{\ge 2}$$
129		relogbval	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge B\in {ℝ}^{+}\right)\to {\log }_{2}B=\frac{\log B}{\log 2}$$
130	128 116 129	syl2anc	$$⊢\phi \to {\log }_{2}B=\frac{\log B}{\log 2}$$
131	130	eqcomd	$$⊢\phi \to \frac{\log B}{\log 2}={\log }_{2}B$$
132	124 127 131	3brtr3d	$$⊢\phi \to {\log }_{P}B\le {\log }_{2}B$$
133	16 75 76 113 132	letrd	$$⊢\phi \to K\le {\log }_{2}B$$
134		flge	$$⊢\left({\log }_{2}B\in ℝ\wedge K\in \mathbb{Z}\right)\to \left(K\le {\log }_{2}B\leftrightarrow K\le ⌊{\log }_{2}B⌋\right)$$
135	76 15 134	syl2anc	$$⊢\phi \to \left(K\le {\log }_{2}B\leftrightarrow K\le ⌊{\log }_{2}B⌋\right)$$
136	133 135	mpbid	$$⊢\phi \to K\le ⌊{\log }_{2}B⌋$$