Theorem aks5lem8

Description: Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025)

	Ref	Expression
Hypotheses	aks5lem7.1	⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ )
	aks5lem7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks5lem7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks5lem7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks5lem7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks5lem7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
	aks5lem7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks5lem7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks5lem7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
	aks5lem7.10	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
	aks5lem7.11	⊢ ( 𝜑 → 𝑅 ∥ ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
	aks5lem7.12	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
	aks5lem7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
	aks5lem7.14	⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
	aks5lem7.15	⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
	aks5lem7.16	⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
Assertion	aks5lem8	⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		aks5lem7.1	⊢ ( 𝜑 → ( ♯ ‘ ( Base ‘ 𝐾 ) ) ∈ ℕ )
2		aks5lem7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
3		aks5lem7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
4		aks5lem7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		aks5lem7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6		aks5lem7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7		aks5lem7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8		aks5lem7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9		aks5lem7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10		aks5lem7.10	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11		aks5lem7.11	⊢ ( 𝜑 → 𝑅 ∥ ( ( ♯ ‘ ( Base ‘ 𝐾 ) ) − 1 ) )
12		aks5lem7.12	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( 𝑋 ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( +g ‘ 𝑆 ) ( ( ℤRHom ‘ 𝑆 ) ‘ 𝑎 ) ) ] ( 𝑆 ~QG 𝐿 ) )
13		aks5lem7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14		aks5lem7.14	⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
15		aks5lem7.15	⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑋 ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
16		aks5lem7.16	⊢ 𝑋 = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
18	17	oveq1d	⊢ ( ( 𝜑 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ↑ 𝑛 ) = ( 𝑃 ↑ 𝑛 ) )
19	18	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑝 = 𝑃 ) → ( 𝑁 = ( 𝑝 ↑ 𝑛 ) ↔ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) )
20	19	rexbidv	⊢ ( ( 𝜑 ∧ 𝑝 = 𝑃 ) → ( ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	aks5lem7	⊢ ( 𝜑 → 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) )
22		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
23	6 22	syl	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
24		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
25		3re	⊢ 3 ∈ ℝ
26	25	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
27	23	zred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28		3pos	⊢ 0 < 3
29	28	a1i	⊢ ( 𝜑 → 0 < 3 )
30		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
31	6 30	syl	⊢ ( 𝜑 → 3 ≤ 𝑁 )
32	24 26 27 29 31	ltletrd	⊢ ( 𝜑 → 0 < 𝑁 )
33	23 32	jca	⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
34		elnnz	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
35	33 34	sylibr	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
36		pcprmpw	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ0 𝑁 = ( 𝑃 ↑ 𝑛 ) ↔ 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
37	4 35 36	syl2anc	⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ0 𝑁 = ( 𝑃 ↑ 𝑛 ) ↔ 𝑁 = ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
38	21 37	mpbird	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 𝑁 = ( 𝑃 ↑ 𝑛 ) )
39		simprl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℕ0 )
40	39	nn0zd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℤ )
41		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 0 < 𝑛 ) → 0 < 𝑛 )
42	39	nn0red	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℝ )
43		0red	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 0 ∈ ℝ )
44	42 43	lenltd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑛 ≤ 0 ↔ ¬ 0 < 𝑛 ) )
45	44	bicomd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( ¬ 0 < 𝑛 ↔ 𝑛 ≤ 0 ) )
46	45	biimpd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( ¬ 0 < 𝑛 → 𝑛 ≤ 0 ) )
47	46	imp	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ ¬ 0 < 𝑛 ) → 𝑛 ≤ 0 )
48		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → 𝑛 ≤ 0 )
49	39	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → 𝑛 ∈ ℕ0 )
50		nn0le0eq0	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 ≤ 0 ↔ 𝑛 = 0 ) )
51	50	bicomd	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 = 0 ↔ 𝑛 ≤ 0 ) )
52	49 51	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → ( 𝑛 = 0 ↔ 𝑛 ≤ 0 ) )
53	48 52	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → 𝑛 = 0 )
54		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑁 = ( 𝑃 ↑ 𝑛 ) )
55		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑛 = 0 )
56	55	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 0 ) )
57	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑃 ∈ ℙ )
58		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
59	57 58	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑃 ∈ ℕ )
60	59	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑃 ∈ ℂ )
61	60	exp0d	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → ( 𝑃 ↑ 0 ) = 1 )
62	56 61	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → ( 𝑃 ↑ 𝑛 ) = 1 )
63	54 62	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑁 = 1 )
64		1red	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 1 ∈ ℝ )
65		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
66	35	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
67		1lt3	⊢ 1 < 3
68	67	a1i	⊢ ( 𝜑 → 1 < 3 )
69	65 26 66 68 31	ltletrd	⊢ ( 𝜑 → 1 < 𝑁 )
70	69	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 1 < 𝑁 )
71	70	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 1 < 𝑁 )
72	64 71	ltned	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 1 ≠ 𝑁 )
73	72	necomd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 𝑁 ≠ 1 )
74	73	neneqd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → ¬ 𝑁 = 1 )
75	63 74	pm2.21dd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 = 0 ) → 0 < 𝑛 )
76	75	ex	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑛 = 0 → 0 < 𝑛 ) )
77	76	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → ( 𝑛 = 0 → 0 < 𝑛 ) )
78	53 77	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ 𝑛 ≤ 0 ) → 0 < 𝑛 )
79	78	ex	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑛 ≤ 0 → 0 < 𝑛 ) )
80	79	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ ¬ 0 < 𝑛 ) → ( 𝑛 ≤ 0 → 0 < 𝑛 ) )
81	47 80	mpd	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) ∧ ¬ 0 < 𝑛 ) → 0 < 𝑛 )
82	41 81	pm2.61dan	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 0 < 𝑛 )
83	40 82	jca	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → ( 𝑛 ∈ ℤ ∧ 0 < 𝑛 ) )
84		elnnz	⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℤ ∧ 0 < 𝑛 ) )
85	83 84	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 𝑛 ∈ ℕ )
86		simprr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ 𝑁 = ( 𝑃 ↑ 𝑛 ) ) ) → 𝑁 = ( 𝑃 ↑ 𝑛 ) )
87	38 85 86	reximssdv	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑃 ↑ 𝑛 ) )
88	4 20 87	rspcedvd	⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ∃ 𝑛 ∈ ℕ 𝑁 = ( 𝑝 ↑ 𝑛 ) )