Theorem aks6d1c7lem4

Description: In the AKS algorithm there exists a unique prime number p that divides N . (Contributed by metakunt, 16-May-2025)

	Ref	Expression
Hypotheses	aks6d1c7.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
	aks6d1c7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
	aks6d1c7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
	aks6d1c7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks6d1c7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
	aks6d1c7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks6d1c7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
	aks6d1c7.10	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
	aks6d1c7.11	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
	aks6d1c7.12	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
	aks6d1c7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
	aks6d1c7.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
Assertion	aks6d1c7lem4	⊢ ( 𝜑 → ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7.1	⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2		aks6d1c7.2	⊢ 𝑃 = ( chr ‘ 𝐾 )
3		aks6d1c7.3	⊢ ( 𝜑 → 𝐾 ∈ Field )
4		aks6d1c7.4	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		aks6d1c7.5	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6		aks6d1c7.6	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
7		aks6d1c7.7	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8		aks6d1c7.8	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9		aks6d1c7.9	⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
10		aks6d1c7.10	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
11		aks6d1c7.11	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
12		aks6d1c7.12	⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
13		aks6d1c7.13	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
14		aks6d1c7.14	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝐾 ∈ Field )
16	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑃 ∈ ℙ )
17	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑅 ∈ ℕ )
18	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
19	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑃 ∥ 𝑁 )
20	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ( 𝑁 gcd 𝑅 ) = 1 )
21	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
22	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
23	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
24	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
25	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
26		simplr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑝 ∈ ℙ )
27		simpr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑝 ∥ 𝑁 )
28	26 27	jca	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → ( 𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑁 ) )
29	1 2 15 16 17 18 19 20 9 21 22 23 24 25 28	aks6d1c7lem3	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑃 = 𝑝 )
30	29	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑁 ) → 𝑝 = 𝑃 )
31	30	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ 𝑁 → 𝑝 = 𝑃 ) )
32	31	ralrimiva	⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 → 𝑝 = 𝑃 ) )
33	4 7 32	3jca	⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ 𝑁 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 → 𝑝 = 𝑃 ) ) )
34		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∥ 𝑁 ↔ 𝑃 ∥ 𝑁 ) )
35	34	eqreu	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∥ 𝑁 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑁 → 𝑝 = 𝑃 ) ) → ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )
36	33 35	syl	⊢ ( 𝜑 → ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝑁 )