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

Metamath Proof Explorer

Theorem aks4d1p7

Proof