aks4d1

Description: Lemma 4.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf , existence of a polynomially bounded number by the digit size of N that asserts the polynomial subspace that we need to search to guarantee that N is prime. Eventually we want to show that the polynomial searching space is bounded by degree B . (Contributed by metakunt, 14-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1.1	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks4d1.2	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
Assertion	aks4d1	$⊢ φ \to \exists r \in (1 \dots B) (N \gcd r = 1 \land {\log_{2} N}^{2} < {od}_{ℤ} (r) (N))$

Proof

Step	Hyp	Ref	Expression
1		aks4d1.1	$⊢ φ \to N \in ℤ_{\geq 3}$
2		aks4d1.2	$⊢ B = ⌈{\log_{2} N}^{5}⌉$
3		oveq2	$⊢ b = a \to N^{b} = N^{a}$
4	3	oveq1d	$⊢ b = a \to N^{b} - 1 = N^{a} - 1$
5	4	cbvprodv	$⊢ \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1) = \prod_{a = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{a} - 1)$
6	5	oveq2i	$⊢ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1) = N^{⌊\log_{2} B⌋} \prod_{a = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{a} - 1)$
7		id	$⊢ h = k \to h = k$
8		oveq2	$⊢ c = b \to N^{c} = N^{b}$
9	8	oveq1d	$⊢ c = b \to N^{c} - 1 = N^{b} - 1$
10	9	cbvprodv	$⊢ \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1) = \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1)$
11	10	oveq2i	$⊢ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1) = N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1)$
12	11	a1i	$⊢ h = k \to N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1) = N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1)$
13	7 12	breq12d	$⊢ h = k \to (h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1) \leftrightarrow k ∥ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1))$
14	13	notbid	$⊢ h = k \to (\neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1) \leftrightarrow \neg k ∥ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1))$
15	14	cbvrabv	$⊢ \{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} = \{k \in (1 \dots B) \| \neg k ∥ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1)\}$
16	15	infeq1i	$⊢ inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) = inf (\{k \in (1 \dots B) \| \neg k ∥ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1)\} ℝ <)$
17	1 6 2 16	aks4d1p4	$⊢ φ \to (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) \in (1 \dots B) \land \neg inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) ∥ N^{⌊\log_{2} B⌋} \prod_{b = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{b} - 1))$
18	17	simpld	$⊢ φ \to inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) \in (1 \dots B)$
19		oveq2	$⊢ r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) \to N \gcd r = N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)$
20	19	adantl	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to N \gcd r = N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)$
21	20	eqeq1d	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to (N \gcd r = 1 \leftrightarrow N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) = 1)$
22		fveq2	$⊢ r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) \to {od}_{ℤ} (r) = {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <))$
23	22	adantl	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to {od}_{ℤ} (r) = {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <))$
24	23	fveq1d	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to {od}_{ℤ} (r) (N) = {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) (N)$
25	24	breq2d	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to ({\log_{2} N}^{2} < {od}_{ℤ} (r) (N) \leftrightarrow {\log_{2} N}^{2} < {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) (N))$
26	21 25	anbi12d	$⊢ (φ \land r = inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) \to ((N \gcd r = 1 \land {\log_{2} N}^{2} < {od}_{ℤ} (r) (N)) \leftrightarrow (N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) = 1 \land {\log_{2} N}^{2} < {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) (N)))$
27	1 6 2 16	aks4d1p8	$⊢ φ \to N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) = 1$
28	1 6 2 16	aks4d1p9	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) (N)$
29	27 28	jca	$⊢ φ \to (N \gcd inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <) = 1 \land {\log_{2} N}^{2} < {od}_{ℤ} (inf (\{h \in (1 \dots B) \| \neg h ∥ N^{⌊\log_{2} B⌋} \prod_{c = 1}^{⌊{\log_{2} N}^{2}⌋} (N^{c} - 1)\} ℝ <)) (N))$
30	18 26 29	rspcedvd	$⊢ φ \to \exists r \in (1 \dots B) (N \gcd r = 1 \land {\log_{2} N}^{2} < {od}_{ℤ} (r) (N))$

Metamath Proof Explorer

Theorem aks4d1

Proof