aks4d1p7

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

	Ref	Expression
Hypotheses	aks4d1p7.1	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks4d1p7.2	$⊢ A = N^{⌊\log_{2} B⌋} \prod_{k = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{k} - 1)$
	aks4d1p7.3	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
	aks4d1p7.4	$⊢ R = inf (\{r \in (1 \dots B) \| \neg r ∥ A\} ℝ <)$
Assertion	aks4d1p7	$⊢ φ \to \exists p \in ℙ (p ∥ R \land \neg p ∥ N)$

Proof

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

Metamath Proof Explorer

Theorem aks4d1p7

Proof