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 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aks5.2 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5.3 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5.4 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
aks5.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks5.6 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks5.7 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks5.8 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
aks5.9 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
aks5.10 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) ( 𝑎 gcd 𝑁 ) = 1 )
Assertion aks5 ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 aks5.1 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
2 aks5.2 ⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
3 aks5.3 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
4 aks5.4 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
5 aks5.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
6 aks5.6 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
7 aks5.7 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
8 aks5.8 ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
9 aks5.9 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
10 aks5.10 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) ( 𝑎 gcd 𝑁 ) = 1 )
11 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑞 ∈ ℙ )
13 12 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑞 ∈ ℙ )
14 prmnn ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℕ )
15 13 14 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑞 ∈ ℕ )
16 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑅 ∈ ℕ )
17 12 14 syl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑞 ∈ ℕ )
18 17 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑞 ∈ ℤ )
19 16 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑅 ∈ ℤ )
20 18 19 gcdcomd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑞 gcd 𝑅 ) = ( 𝑅 gcd 𝑞 ) )
21 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
22 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
23 21 22 syl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
24 19 18 23 3jca ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑅 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
25 19 23 gcdcomd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑅 gcd 𝑁 ) = ( 𝑁 gcd 𝑅 ) )
26 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑁 gcd 𝑅 ) = 1 )
27 25 26 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑅 gcd 𝑁 ) = 1 )
28 simpr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → 𝑞 ∥ 𝑁 )
29 27 28 jca ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( ( 𝑅 gcd 𝑁 ) = 1 ∧ 𝑞 ∥ 𝑁 ) )
30 rpdvds ⊢ ( ( ( 𝑅 ∈ ℤ ∧ 𝑞 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑅 gcd 𝑁 ) = 1 ∧ 𝑞 ∥ 𝑁 ) ) → ( 𝑅 gcd 𝑞 ) = 1 )
31 24 29 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑅 gcd 𝑞 ) = 1 )
32 20 31 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( 𝑞 gcd 𝑅 ) = 1 )
33 odzcl ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑞 ∈ ℤ ∧ ( 𝑞 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ∈ ℕ )
34 16 18 32 33 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ∈ ℕ )
35 34 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ∈ ℕ )
36 35 nnnn0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ∈ ℕ0 )
37 15 36 nnexpcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∈ ℕ )
38 11 37 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ♯ ‘ ( Base ‘ 𝑘 ) ) ∈ ℕ )
39 eqid ⊢ ( chr ‘ 𝑘 ) = ( chr ‘ 𝑘 )
40 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑘 ∈ Field )
41 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( chr ‘ 𝑘 ) = 𝑞 )
42 41 13 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( chr ‘ 𝑘 ) ∈ ℙ )
43 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑅 ∈ ℕ )
44 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
45 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑞 ∥ 𝑁 )
46 41 45 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( chr ‘ 𝑘 ) ∥ 𝑁 )
47 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
48 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
49 15 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑞 ∈ ℤ )
50 32 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( 𝑞 gcd 𝑅 ) = 1 )
51 odzid ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑞 ∈ ℤ ∧ ( 𝑞 gcd 𝑅 ) = 1 ) → 𝑅 ∥ ( ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) − 1 ) )
52 43 49 50 51 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑅 ∥ ( ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) − 1 ) )
53 11 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) = ( ♯ ‘ ( Base ‘ 𝑘 ) ) )
54 53 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ( ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) − 1 ) = ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) − 1 ) )
55 52 54 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → 𝑅 ∥ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) − 1 ) )
56 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
57 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) ( 𝑎 gcd 𝑁 ) = 1 )
58 38 39 40 42 43 44 46 47 1 48 55 56 57 3 4 2 aks5lem8 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) ∧ 𝑘 ∈ Field ) ∧ ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )
59 12 34 exfinfldd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ∃ 𝑘 ∈ Field ( ( ♯ ‘ ( Base ‘ 𝑘 ) ) = ( 𝑞 ↑ ( ( odℤ ‘ 𝑅 ) ‘ 𝑞 ) ) ∧ ( chr ‘ 𝑘 ) = 𝑞 ) )
60 58 59 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ ℙ ) ∧ 𝑞 ∥ 𝑁 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )
61 uzuzle23 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
62 5 61 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
63 exprmfct ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑞 ∈ ℙ 𝑞 ∥ 𝑁 )
64 62 63 syl ⊢ ( 𝜑 → ∃ 𝑞 ∈ ℙ 𝑞 ∥ 𝑁 )
65 60 64 r19.29a ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )