Theorem aks4d1p7

Description: Technical step in AKS lemma 4.1 (Contributed by metakunt, 31-Oct-2024)

	Ref	Expression
Hypotheses	aks4d1p7.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks4d1p7.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
	aks4d1p7.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
	aks4d1p7.4	$$⊢R=sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
Assertion	aks4d1p7	$$⊢\phi \to \exists p\in \mathbb{P}\left(p\parallel R\wedge \neg p\parallel N\right)$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p7.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
2		aks4d1p7.2	$$⊢A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
3		aks4d1p7.3	$$⊢B=⌈{{\log }_{2}N}^5⌉$$
4		aks4d1p7.4	$$⊢R=sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
5	1	adantr	$$⊢\left(\phi \wedge \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\right)\to N\in {\mathbb{Z}}_{\ge 3}$$
6		breq1	$$⊢p=q\to \left(p\parallel R\leftrightarrow q\parallel R\right)$$
7		breq1	$$⊢p=q\to \left(p\parallel N\leftrightarrow q\parallel N\right)$$
8	6 7	imbi12d	$$⊢p=q\to \left(\left(p\parallel R\to p\parallel N\right)\leftrightarrow \left(q\parallel R\to q\parallel N\right)\right)$$
9	8	cbvralvw	$$⊢\forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\leftrightarrow \forall q\in \mathbb{P}\left(q\parallel R\to q\parallel N\right)$$
10	9	biimpi	$$⊢\forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\to \forall q\in \mathbb{P}\left(q\parallel R\to q\parallel N\right)$$
11	10	adantl	$$⊢\left(\phi \wedge \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\right)\to \forall q\in \mathbb{P}\left(q\parallel R\to q\parallel N\right)$$
12	5 2 3 4 11	aks4d1p7d1	$$⊢\left(\phi \wedge \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\right)\to R\parallel N^{⌊{\log }_{2}B⌋}$$
13	4	a1i	$$⊢\phi \to R=sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)$$
14		ltso	$$⊢<\mathrm{Or}ℝ$$
15	14	a1i	$$⊢\phi \to <\mathrm{Or}ℝ$$
16		fzfid	$$⊢\phi \to \left(1\dots B\right)\in \mathrm{Fin}$$
17		ssrab2	$$⊢\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\subseteq \left(1\dots B\right)$$
18	17	a1i	$$⊢\phi \to \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\subseteq \left(1\dots B\right)$$
19	16 18	ssfid	$$⊢\phi \to \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\in \mathrm{Fin}$$
20	1 2 3	aks4d1p3	$$⊢\phi \to \exists r\in \left(1\dots B\right)\neg r\parallel A$$
21		rabn0	$$⊢\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\ne \varnothing \leftrightarrow \exists r\in \left(1\dots B\right)\neg r\parallel A$$
22	20 21	sylibr	$$⊢\phi \to \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\ne \varnothing$$
23		elfznn	$$⊢o\in \left(1\dots B\right)\to o\in \mathbb{N}$$
24	23	adantl	$$⊢\left(\phi \wedge o\in \left(1\dots B\right)\right)\to o\in \mathbb{N}$$
25	24	nnred	$$⊢\left(\phi \wedge o\in \left(1\dots B\right)\right)\to o\in ℝ$$
26	25	ex	$$⊢\phi \to \left(o\in \left(1\dots B\right)\to o\in ℝ\right)$$
27	26	ssrdv	$$⊢\phi \to \left(1\dots B\right)\subseteq ℝ$$
28	18 27	sstrd	$$⊢\phi \to \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\subseteq ℝ$$
29	19 22 28	3jca	$$⊢\phi \to \left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\in \mathrm{Fin}\wedge \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\ne \varnothing \wedge \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\subseteq ℝ\right)$$
30		fiinfcl	$$⊢\left(<\mathrm{Or}ℝ\wedge \left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\in \mathrm{Fin}\wedge \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\ne \varnothing \wedge \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\subseteq ℝ\right)\right)\to sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)\in \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}$$
31	15 29 30	syl2anc	$$⊢\phi \to sup\left(\left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\},ℝ,<\right)\in \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}$$
32	13 31	eqeltrd	$$⊢\phi \to R\in \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}$$
33		breq1	$$⊢r=R\to \left(r\parallel A\leftrightarrow R\parallel A\right)$$
34	33	notbid	$$⊢r=R\to \left(\neg r\parallel A\leftrightarrow \neg R\parallel A\right)$$
35	34	elrab	$$⊢R\in \left\{r\in \left(1\dots B\right)|\neg r\parallel A\right\}\leftrightarrow \left(R\in \left(1\dots B\right)\wedge \neg R\parallel A\right)$$
36	32 35	sylib	$$⊢\phi \to \left(R\in \left(1\dots B\right)\wedge \neg R\parallel A\right)$$
37	36	simprd	$$⊢\phi \to \neg R\parallel A$$
38	1 2 3 4	aks4d1p4	$$⊢\phi \to \left(R\in \left(1\dots B\right)\wedge \neg R\parallel A\right)$$
39	38	simpld	$$⊢\phi \to R\in \left(1\dots B\right)$$
40	39	elfzelzd	$$⊢\phi \to R\in \mathbb{Z}$$
41		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
42	1 41	syl	$$⊢\phi \to N\in \mathbb{Z}$$
43		2re	$$⊢2\in ℝ$$
44	43	a1i	$$⊢\phi \to 2\in ℝ$$
45		2pos	$$⊢0<2$$
46	45	a1i	$$⊢\phi \to 0<2$$
47	3	a1i	$$⊢\phi \to B=⌈{{\log }_{2}N}^5⌉$$
48	42	zred	$$⊢\phi \to N\in ℝ$$
49		0red	$$⊢\phi \to 0\in ℝ$$
50		3re	$$⊢3\in ℝ$$
51	50	a1i	$$⊢\phi \to 3\in ℝ$$
52		3pos	$$⊢0<3$$
53	52	a1i	$$⊢\phi \to 0<3$$
54		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
55	1 54	syl	$$⊢\phi \to 3\le N$$
56	49 51 48 53 55	ltletrd	$$⊢\phi \to 0<N$$
57		1red	$$⊢\phi \to 1\in ℝ$$
58		1lt2	$$⊢1<2$$
59	58	a1i	$$⊢\phi \to 1<2$$
60	57 59	ltned	$$⊢\phi \to 1\ne 2$$
61	60	necomd	$$⊢\phi \to 2\ne 1$$
62	44 46 48 56 61	relogbcld	$$⊢\phi \to {\log }_{2}N\in ℝ$$
63		5nn0	$$⊢5\in {\mathbb{N}}_0$$
64	63	a1i	$$⊢\phi \to 5\in {\mathbb{N}}_0$$
65	62 64	reexpcld	$$⊢\phi \to {{\log }_{2}N}^5\in ℝ$$
66	65	ceilcld	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in \mathbb{Z}$$
67	66	zred	$$⊢\phi \to ⌈{{\log }_{2}N}^5⌉\in ℝ$$
68	47 67	eqeltrd	$$⊢\phi \to B\in ℝ$$
69		9re	$$⊢9\in ℝ$$
70	69	a1i	$$⊢\phi \to 9\in ℝ$$
71		9pos	$$⊢0<9$$
72	71	a1i	$$⊢\phi \to 0<9$$
73	48 55	3lexlogpow5ineq4	$$⊢\phi \to 9<{{\log }_{2}N}^5$$
74	65	ceilged	$$⊢\phi \to {{\log }_{2}N}^5\le ⌈{{\log }_{2}N}^5⌉$$
75	70 65 67 73 74	ltletrd	$$⊢\phi \to 9<⌈{{\log }_{2}N}^5⌉$$
76	75 47	breqtrrd	$$⊢\phi \to 9<B$$
77	49 70 68 72 76	lttrd	$$⊢\phi \to 0<B$$
78	44 46 68 77 61	relogbcld	$$⊢\phi \to {\log }_{2}B\in ℝ$$
79	78	flcld	$$⊢\phi \to ⌊{\log }_{2}B⌋\in \mathbb{Z}$$
80	44	recnd	$$⊢\phi \to 2\in ℂ$$
81	49 46	gtned	$$⊢\phi \to 2\ne 0$$
82		logb1	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 2\ne 1\right)\to {\log }_{2}1=0$$
83	80 81 61 82	syl3anc	$$⊢\phi \to {\log }_{2}1=0$$
84	83	eqcomd	$$⊢\phi \to 0={\log }_{2}1$$
85		2z	$$⊢2\in \mathbb{Z}$$
86	85	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
87	44	leidd	$$⊢\phi \to 2\le 2$$
88		0lt1	$$⊢0<1$$
89	88	a1i	$$⊢\phi \to 0<1$$
90		1lt9	$$⊢1<9$$
91	90	a1i	$$⊢\phi \to 1<9$$
92	57 70 91	ltled	$$⊢\phi \to 1\le 9$$
93	70 68 76	ltled	$$⊢\phi \to 9\le B$$
94	57 70 68 92 93	letrd	$$⊢\phi \to 1\le B$$
95	86 87 57 89 68 77 94	logblebd	$$⊢\phi \to {\log }_{2}1\le {\log }_{2}B$$
96	84 95	eqbrtrd	$$⊢\phi \to 0\le {\log }_{2}B$$
97		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
98		flge	$$⊢\left({\log }_{2}B\in ℝ\wedge 0\in \mathbb{Z}\right)\to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
99	78 97 98	syl2anc	$$⊢\phi \to \left(0\le {\log }_{2}B\leftrightarrow 0\le ⌊{\log }_{2}B⌋\right)$$
100	96 99	mpbid	$$⊢\phi \to 0\le ⌊{\log }_{2}B⌋$$
101	79 100	jca	$$⊢\phi \to \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
102		elnn0z	$$⊢⌊{\log }_{2}B⌋\in {\mathbb{N}}_0\leftrightarrow \left(⌊{\log }_{2}B⌋\in \mathbb{Z}\wedge 0\le ⌊{\log }_{2}B⌋\right)$$
103	101 102	sylibr	$$⊢\phi \to ⌊{\log }_{2}B⌋\in {\mathbb{N}}_0$$
104	42 103	zexpcld	$$⊢\phi \to N^{⌊{\log }_{2}B⌋}\in \mathbb{Z}$$
105		fzfid	$$⊢\phi \to \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\in \mathrm{Fin}$$
106	42	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N\in \mathbb{Z}$$
107		elfznn	$$⊢k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\to k\in \mathbb{N}$$
108	107	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in \mathbb{N}$$
109	108	nnnn0d	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to k\in {\mathbb{N}}_0$$
110	106 109	zexpcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k\in \mathbb{Z}$$
111		1zzd	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to 1\in \mathbb{Z}$$
112	110 111	zsubcld	$$⊢\left(\phi \wedge k\in \left(1\dots ⌊{{\log }_{2}N}^2⌋\right)\right)\to N^k-1\in \mathbb{Z}$$
113	105 112	fprodzcl	$$⊢\phi \to \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}$$
114		dvdsmultr1	$$⊢\left(R\in \mathbb{Z}\wedge N^{⌊{\log }_{2}B⌋}\in \mathbb{Z}\wedge \prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\in \mathbb{Z}\right)\to \left(R\parallel N^{⌊{\log }_{2}B⌋}\to R\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\right)$$
115	40 104 113 114	syl3anc	$$⊢\phi \to \left(R\parallel N^{⌊{\log }_{2}B⌋}\to R\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\right)$$
116	115	imp	$$⊢\left(\phi \wedge R\parallel N^{⌊{\log }_{2}B⌋}\right)\to R\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
117	2	a1i	$$⊢\phi \to A=N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)$$
118	117	breq2d	$$⊢\phi \to \left(R\parallel A\leftrightarrow R\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\right)$$
119	118	adantr	$$⊢\left(\phi \wedge R\parallel N^{⌊{\log }_{2}B⌋}\right)\to \left(R\parallel A\leftrightarrow R\parallel N^{⌊{\log }_{2}B⌋}\prod _{k=1}^{⌊{{\log }_{2}N}^2⌋}\left(N^k-1\right)\right)$$
120	116 119	mpbird	$$⊢\left(\phi \wedge R\parallel N^{⌊{\log }_{2}B⌋}\right)\to R\parallel A$$
121	120	ex	$$⊢\phi \to \left(R\parallel N^{⌊{\log }_{2}B⌋}\to R\parallel A\right)$$
122	121	con3d	$$⊢\phi \to \left(\neg R\parallel A\to \neg R\parallel N^{⌊{\log }_{2}B⌋}\right)$$
123	37 122	mpd	$$⊢\phi \to \neg R\parallel N^{⌊{\log }_{2}B⌋}$$
124	123	adantr	$$⊢\left(\phi \wedge \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)\right)\to \neg R\parallel N^{⌊{\log }_{2}B⌋}$$
125	12 124	pm2.65da	$$⊢\phi \to \neg \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)$$
126		ianor	$$⊢\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \left(\neg p\parallel R\vee \neg \neg p\parallel N\right)$$
127		notnotb	$$⊢p\parallel N\leftrightarrow \neg \neg p\parallel N$$
128	127	orbi2i	$$⊢\left(\neg p\parallel R\vee p\parallel N\right)\leftrightarrow \left(\neg p\parallel R\vee \neg \neg p\parallel N\right)$$
129	128	bicomi	$$⊢\left(\neg p\parallel R\vee \neg \neg p\parallel N\right)\leftrightarrow \left(\neg p\parallel R\vee p\parallel N\right)$$
130	126 129	bitri	$$⊢\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \left(\neg p\parallel R\vee p\parallel N\right)$$
131		df-or	$$⊢\left(\neg p\parallel R\vee p\parallel N\right)\leftrightarrow \left(\neg \neg p\parallel R\to p\parallel N\right)$$
132	130 131	bitri	$$⊢\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \left(\neg \neg p\parallel R\to p\parallel N\right)$$
133		notnotb	$$⊢p\parallel R\leftrightarrow \neg \neg p\parallel R$$
134	133	imbi1i	$$⊢\left(p\parallel R\to p\parallel N\right)\leftrightarrow \left(\neg \neg p\parallel R\to p\parallel N\right)$$
135	134	bicomi	$$⊢\left(\neg \neg p\parallel R\to p\parallel N\right)\leftrightarrow \left(p\parallel R\to p\parallel N\right)$$
136	132 135	bitri	$$⊢\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \left(p\parallel R\to p\parallel N\right)$$
137	136	ralbii	$$⊢\forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)$$
138	137	notbii	$$⊢\neg \forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \neg \forall p\in \mathbb{P}\left(p\parallel R\to p\parallel N\right)$$
139	125 138	sylibr	$$⊢\phi \to \neg \forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)$$
140		ralnex	$$⊢\forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \neg \exists p\in \mathbb{P}\left(p\parallel R\wedge \neg p\parallel N\right)$$
141	140	con2bii	$$⊢\exists p\in \mathbb{P}\left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \neg \forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)$$
142	141	bicomi	$$⊢\neg \forall p\in \mathbb{P}\neg \left(p\parallel R\wedge \neg p\parallel N\right)\leftrightarrow \exists p\in \mathbb{P}\left(p\parallel R\wedge \neg p\parallel N\right)$$
143	139 142	sylib	$$⊢\phi \to \exists p\in \mathbb{P}\left(p\parallel R\wedge \neg p\parallel N\right)$$