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	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
	aks6d1c7.2	$$⊢P=\mathrm{chr}\left(K\right)$$
	aks6d1c7.3	$$⊢\phi \to K\in \mathrm{Field}$$
	aks6d1c7.4	$$⊢\phi \to P\in \mathbb{P}$$
	aks6d1c7.5	$$⊢\phi \to R\in \mathbb{N}$$
	aks6d1c7.6	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
	aks6d1c7.7	$$⊢\phi \to P\parallel N$$
	aks6d1c7.8	$$⊢\phi \to N\gcd R=1$$
	aks6d1c7.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
	aks6d1c7.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
	aks6d1c7.11	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
	aks6d1c7.12	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
	aks6d1c7.13	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
	aks6d1c7.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
Assertion	aks6d1c7lem4	$$⊢\phi \to \exists !p\in \mathbb{P}p\parallel N$$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c7.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨e,f⟩|\left(e\in \mathbb{N}\wedge f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}\wedge \forall y\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)e{\cdot }_{{\mathrm{mulGrp}}_K}{\mathrm{eval}}_1\left(K\right)\left(f\right)\left(y\right)={\mathrm{eval}}_1\left(K\right)\left(f\right)\left(e{\cdot }_{{\mathrm{mulGrp}}_K}y\right)\right)\right\}$$
2		aks6d1c7.2	$$⊢P=\mathrm{chr}\left(K\right)$$
3		aks6d1c7.3	$$⊢\phi \to K\in \mathrm{Field}$$
4		aks6d1c7.4	$$⊢\phi \to P\in \mathbb{P}$$
5		aks6d1c7.5	$$⊢\phi \to R\in \mathbb{N}$$
6		aks6d1c7.6	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 3}$$
7		aks6d1c7.7	$$⊢\phi \to P\parallel N$$
8		aks6d1c7.8	$$⊢\phi \to N\gcd R=1$$
9		aks6d1c7.9	$$⊢A=⌊\sqrt{\mathrm{\varphi }\left(R\right)}{\log }_{2}N⌋$$
10		aks6d1c7.10	$$⊢\phi \to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
11		aks6d1c7.11	$$⊢\phi \to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
12		aks6d1c7.12	$$⊢\phi \to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
13		aks6d1c7.13	$$⊢\phi \to \forall b\in \left(1\dots A\right)b\gcd N=1$$
14		aks6d1c7.14	$$⊢\phi \to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
15	3	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to K\in \mathrm{Field}$$
16	4	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to P\in \mathbb{P}$$
17	5	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to R\in \mathbb{N}$$
18	6	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to N\in {\mathbb{Z}}_{\ge 3}$$
19	7	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to P\parallel N$$
20	8	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to N\gcd R=1$$
21	10	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to {{\log }_{2}N}^2<{\mathrm{od}}_{\mathbb{Z}}\left(R\right)\left(N\right)$$
22	11	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to \left(x\in {\mathrm{Base}}_K⟼P{\cdot }_{{\mathrm{mulGrp}}_K}x\right)\in \left(K\mathrm{RingIso}K\right)$$
23	12	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to M\in \left({\mathrm{mulGrp}}_K\mathrm{PrimRoots}R\right)$$
24	13	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to \forall b\in \left(1\dots A\right)b\gcd N=1$$
25	14	ad2antrr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to \forall a\in \left(1\dots A\right)N\underset{\dot{}}{\sim }\left({\mathrm{var}}_1\left(K\right){+}_{{\mathrm{Poly}}_1\left(K\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(K\right)\right)\left(\mathrm{\mathbb{Z}RHom}\left(K\right)\left(a\right)\right)\right)$$
26		simplr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to p\in \mathbb{P}$$
27		simpr	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to p\parallel N$$
28	26 27	jca	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to \left(p\in \mathbb{P}\wedge p\parallel N\right)$$
29	1 2 15 16 17 18 19 20 9 21 22 23 24 25 28	aks6d1c7lem3	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to P=p$$
30	29	eqcomd	$$⊢\left(\left(\phi \wedge p\in \mathbb{P}\right)\wedge p\parallel N\right)\to p=P$$
31	30	ex	$$⊢\left(\phi \wedge p\in \mathbb{P}\right)\to \left(p\parallel N\to p=P\right)$$
32	31	ralrimiva	$$⊢\phi \to \forall p\in \mathbb{P}\left(p\parallel N\to p=P\right)$$
33	4 7 32	3jca	$$⊢\phi \to \left(P\in \mathbb{P}\wedge P\parallel N\wedge \forall p\in \mathbb{P}\left(p\parallel N\to p=P\right)\right)$$
34		breq1	$$⊢p=P\to \left(p\parallel N\leftrightarrow P\parallel N\right)$$
35	34	eqreu	$$⊢\left(P\in \mathbb{P}\wedge P\parallel N\wedge \forall p\in \mathbb{P}\left(p\parallel N\to p=P\right)\right)\to \exists !p\in \mathbb{P}p\parallel N$$
36	33 35	syl	$$⊢\phi \to \exists !p\in \mathbb{P}p\parallel N$$