aks5

Description: The AKS Primality test, given an integer N greater than or equal to 3, find a coprime R such that R is big enough. Then, if a bunch of polynomial equalities in the residue ring hold then N is a prime power. Currently depends on the axiom ax-exfinfld , since we currently do not have the existence of finite fields in the database. (Contributed by metakunt, 16-Aug-2025)

	Ref	Expression
Hypotheses	aks5.1	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
	aks5.2	$⊢ X = {var}_{1} (ℤ / N ℤ)$
	aks5.3	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
	aks5.4	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} X) -_{S} 1_{S}\})$
	aks5.5	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks5.6	$⊢ φ \to R \in ℕ$
	aks5.7	$⊢ φ \to N \gcd R = 1$
	aks5.8	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
	aks5.9	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
	aks5.10	$⊢ φ \to \forall a \in (1 \dots A) a \gcd N = 1$
Assertion	aks5	$⊢ φ \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$

Proof

Step	Hyp	Ref	Expression
1		aks5.1	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
2		aks5.2	$⊢ X = {var}_{1} (ℤ / N ℤ)$
3		aks5.3	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
4		aks5.4	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} X) -_{S} 1_{S}\})$
5		aks5.5	$⊢ φ \to N \in ℤ_{\geq 3}$
6		aks5.6	$⊢ φ \to R \in ℕ$
7		aks5.7	$⊢ φ \to N \gcd R = 1$
8		aks5.8	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
9		aks5.9	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
10		aks5.10	$⊢ φ \to \forall a \in (1 \dots A) a \gcd N = 1$
11		simprl	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to \|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)}$
12		simplr	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q \in ℙ$
13	12	ad2antrr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q \in ℙ$
14		prmnn	$⊢ q \in ℙ \to q \in ℕ$
15	13 14	syl	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q \in ℕ$
16	6	ad2antrr	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to R \in ℕ$
17	12 14	syl	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q \in ℕ$
18	17	nnzd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q \in ℤ$
19	16	nnzd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to R \in ℤ$
20	18 19	gcdcomd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q \gcd R = R \gcd q$
21	5	ad2antrr	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to N \in ℤ_{\geq 3}$
22		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
23	21 22	syl	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to N \in ℤ$
24	19 18 23	3jca	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to (R \in ℤ \land q \in ℤ \land N \in ℤ)$
25	19 23	gcdcomd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to R \gcd N = N \gcd R$
26	7	ad2antrr	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to N \gcd R = 1$
27	25 26	eqtrd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to R \gcd N = 1$
28		simpr	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q ∥ N$
29	27 28	jca	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to (R \gcd N = 1 \land q ∥ N)$
30		rpdvds	$⊢ ((R \in ℤ \land q \in ℤ \land N \in ℤ) \land (R \gcd N = 1 \land q ∥ N)) \to R \gcd q = 1$
31	24 29 30	syl2anc	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to R \gcd q = 1$
32	20 31	eqtrd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to q \gcd R = 1$
33		odzcl	$⊢ (R \in ℕ \land q \in ℤ \land q \gcd R = 1) \to {od}_{ℤ} (R) (q) \in ℕ$
34	16 18 32 33	syl3anc	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to {od}_{ℤ} (R) (q) \in ℕ$
35	34	ad2antrr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to {od}_{ℤ} (R) (q) \in ℕ$
36	35	nnnn0d	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to {od}_{ℤ} (R) (q) \in ℕ_{0}$
37	15 36	nnexpcld	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q^{{od}_{ℤ} (R) (q)} \in ℕ$
38	11 37	eqeltrd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to \|{Base}_{k}\| \in ℕ$
39		eqid	$⊢ chr (k) = chr (k)$
40		simplr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to k \in Field$
41		simprr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to chr (k) = q$
42	41 13	eqeltrd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to chr (k) \in ℙ$
43	6	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to R \in ℕ$
44	5	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to N \in ℤ_{\geq 3}$
45		simpllr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q ∥ N$
46	41 45	eqbrtrd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to chr (k) ∥ N$
47	7	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to N \gcd R = 1$
48	8	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
49	15	nnzd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q \in ℤ$
50	32	ad2antrr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q \gcd R = 1$
51		odzid	$⊢ (R \in ℕ \land q \in ℤ \land q \gcd R = 1) \to R ∥ (q^{{od}_{ℤ} (R) (q)} - 1)$
52	43 49 50 51	syl3anc	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to R ∥ (q^{{od}_{ℤ} (R) (q)} - 1)$
53	11	eqcomd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q^{{od}_{ℤ} (R) (q)} = \|{Base}_{k}\|$
54	53	oveq1d	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to q^{{od}_{ℤ} (R) (q)} - 1 = \|{Base}_{k}\| - 1$
55	52 54	breqtrd	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to R ∥ (\|{Base}_{k}\| - 1)$
56	9	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
57	10	ad4antr	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to \forall a \in (1 \dots A) a \gcd N = 1$
58	38 39 40 42 43 44 46 47 1 48 55 56 57 3 4 2	aks5lem8	$⊢ ((((φ \land q \in ℙ) \land q ∥ N) \land k \in Field) \land (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)) \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$
59	12 34	exfinfldd	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to \exists k \in Field (\|{Base}_{k}\| = q^{{od}_{ℤ} (R) (q)} \land chr (k) = q)$
60	58 59	r19.29a	$⊢ ((φ \land q \in ℙ) \land q ∥ N) \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$
61		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
62	5 61	syl	$⊢ φ \to N \in ℤ_{\geq 2}$
63		exprmfct	$⊢ N \in ℤ_{\geq 2} \to \exists q \in ℙ q ∥ N$
64	62 63	syl	$⊢ φ \to \exists q \in ℙ q ∥ N$
65	60 64	r19.29a	$⊢ φ \to \exists p \in ℙ \exists n \in ℕ N = p^{n}$

Metamath Proof Explorer

Theorem aks5

Proof