Metamath Proof Explorer

Theorem 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 ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks5.2 
|- X = ( var1 ` ( Z/nZ ` N ) )
aks5.3 
|- S = ( Poly1 ` ( Z/nZ ` N ) )
aks5.4 
|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
aks5.5 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks5.6 
|- ( ph -> R e. NN )
aks5.7 
|- ( ph -> ( N gcd R ) = 1 )
aks5.8 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
aks5.9 
|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
aks5.10 
|- ( ph -> A. a e. ( 1 ... A ) ( a gcd N ) = 1 )
Assertion aks5 
|- ( ph -> E. p e. Prime E. n e. NN N = ( p ^ n ) )

Proof

Step Hyp Ref Expression
1 aks5.1 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
2 aks5.2 
 |-  X = ( var1 ` ( Z/nZ ` N ) )
3 aks5.3 
 |-  S = ( Poly1 ` ( Z/nZ ` N ) )
4 aks5.4 
 |-  L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
5 aks5.5 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
6 aks5.6 
 |-  ( ph -> R e. NN )
7 aks5.7 
 |-  ( ph -> ( N gcd R ) = 1 )
8 aks5.8 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
9 aks5.9 
 |-  ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
10 aks5.10 
 |-  ( ph -> A. a e. ( 1 ... A ) ( a gcd N ) = 1 )
11 simprl 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) )
12 simplr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> q e. Prime )
13 12 ad2antrr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> q e. Prime )
14 prmnn 
 |-  ( q e. Prime -> q e. NN )
15 13 14 syl 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> q e. NN )
16 6 ad2antrr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> R e. NN )
17 12 14 syl 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> q e. NN )
18 17 nnzd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> q e. ZZ )
19 16 nnzd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> R e. ZZ )
20 18 19 gcdcomd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( q gcd R ) = ( R gcd q ) )
21 5 ad2antrr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> N e. ( ZZ>= ` 3 ) )
22 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
23 21 22 syl 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> N e. ZZ )
24 19 18 23 3jca 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( R e. ZZ /\ q e. ZZ /\ N e. ZZ ) )
25 19 23 gcdcomd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( R gcd N ) = ( N gcd R ) )
26 7 ad2antrr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( N gcd R ) = 1 )
27 25 26 eqtrd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( R gcd N ) = 1 )
28 simpr 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> q || N )
29 27 28 jca 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( ( R gcd N ) = 1 /\ q || N ) )
30 rpdvds 
 |-  ( ( ( R e. ZZ /\ q e. ZZ /\ N e. ZZ ) /\ ( ( R gcd N ) = 1 /\ q || N ) ) -> ( R gcd q ) = 1 )
31 24 29 30 syl2anc 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( R gcd q ) = 1 )
32 20 31 eqtrd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( q gcd R ) = 1 )
33 odzcl 
 |-  ( ( R e. NN /\ q e. ZZ /\ ( q gcd R ) = 1 ) -> ( ( odZ ` R ) ` q ) e. NN )
34 16 18 32 33 syl3anc 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> ( ( odZ ` R ) ` q ) e. NN )
35 34 ad2antrr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( ( odZ ` R ) ` q ) e. NN )
36 35 nnnn0d 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( ( odZ ` R ) ` q ) e. NN0 )
37 15 36 nnexpcld 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( q ^ ( ( odZ ` R ) ` q ) ) e. NN )
38 11 37 eqeltrd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( # ` ( Base ` k ) ) e. NN )
39 eqid 
 |-  ( chr ` k ) = ( chr ` k )
40 simplr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> k e. Field )
41 simprr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( chr ` k ) = q )
42 41 13 eqeltrd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( chr ` k ) e. Prime )
43 6 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> R e. NN )
44 5 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> N e. ( ZZ>= ` 3 ) )
45 simpllr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> q || N )
46 41 45 eqbrtrd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( chr ` k ) || N )
47 7 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( N gcd R ) = 1 )
48 8 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
49 15 nnzd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> q e. ZZ )
50 32 ad2antrr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( q gcd R ) = 1 )
51 odzid 
 |-  ( ( R e. NN /\ q e. ZZ /\ ( q gcd R ) = 1 ) -> R || ( ( q ^ ( ( odZ ` R ) ` q ) ) - 1 ) )
52 43 49 50 51 syl3anc 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> R || ( ( q ^ ( ( odZ ` R ) ` q ) ) - 1 ) )
53 11 eqcomd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( q ^ ( ( odZ ` R ) ` q ) ) = ( # ` ( Base ` k ) ) )
54 53 oveq1d 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> ( ( q ^ ( ( odZ ` R ) ` q ) ) - 1 ) = ( ( # ` ( Base ` k ) ) - 1 ) )
55 52 54 breqtrd 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> R || ( ( # ` ( Base ` k ) ) - 1 ) )
56 9 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
57 10 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> A. a e. ( 1 ... A ) ( a gcd N ) = 1 )
58 38 39 40 42 43 44 46 47 1 48 55 56 57 3 4 2 aks5lem8 
 |-  ( ( ( ( ( ph /\ q e. Prime ) /\ q || N ) /\ k e. Field ) /\ ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) ) -> E. p e. Prime E. n e. NN N = ( p ^ n ) )
59 12 34 exfinfldd 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> E. k e. Field ( ( # ` ( Base ` k ) ) = ( q ^ ( ( odZ ` R ) ` q ) ) /\ ( chr ` k ) = q ) )
60 58 59 r19.29a 
 |-  ( ( ( ph /\ q e. Prime ) /\ q || N ) -> E. p e. Prime E. n e. NN N = ( p ^ n ) )
61 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
62 5 61 syl 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
63 exprmfct 
 |-  ( N e. ( ZZ>= ` 2 ) -> E. q e. Prime q || N )
64 62 63 syl 
 |-  ( ph -> E. q e. Prime q || N )
65 60 64 r19.29a 
 |-  ( ph -> E. p e. Prime E. n e. NN N = ( p ^ n ) )