aks5lem6

Description: Connect results of section 5 and Theorem 6.1 AKS. (Contributed by metakunt, 25-Jun-2025)

	Ref	Expression
Hypotheses	aks5lem6.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks5lem6.2	$⊢ P = chr (K)$
	aks5lem6.3	$⊢ φ \to K \in Field$
	aks5lem6.4	$⊢ φ \to P \in ℙ$
	aks5lem6.5	$⊢ φ \to R \in ℕ$
	aks5lem6.6	$⊢ φ \to N \in ℤ_{\geq 3}$
	aks5lem6.7	$⊢ φ \to P ∥ N$
	aks5lem6.8	$⊢ φ \to N \gcd R = 1$
	aks5lem6.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
	aks5lem6.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
	aks5lem6.11	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks5lem6.12	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks5lem6.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
	aks5lem6.14	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
	aks5lem6.15	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) -_{S} 1_{S}\})$
	aks5lem6.16	$⊢ X = {var}_{1} (ℤ / N ℤ)$
	aks5lem6.17	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
Assertion	aks5lem6	$⊢ φ \to N = P^{P pCnt N}$

Proof

Step	Hyp	Ref	Expression
1		aks5lem6.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
2		aks5lem6.2	$⊢ P = chr (K)$
3		aks5lem6.3	$⊢ φ \to K \in Field$
4		aks5lem6.4	$⊢ φ \to P \in ℙ$
5		aks5lem6.5	$⊢ φ \to R \in ℕ$
6		aks5lem6.6	$⊢ φ \to N \in ℤ_{\geq 3}$
7		aks5lem6.7	$⊢ φ \to P ∥ N$
8		aks5lem6.8	$⊢ φ \to N \gcd R = 1$
9		aks5lem6.9	$⊢ A = ⌊\sqrt{ϕ (R)} \log_{2} N⌋$
10		aks5lem6.10	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
11		aks5lem6.11	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
12		aks5lem6.12	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
13		aks5lem6.13	$⊢ φ \to \forall b \in (1 \dots A) b \gcd N = 1$
14		aks5lem6.14	$⊢ S = {Poly}_{1} (ℤ / N ℤ)$
15		aks5lem6.15	$⊢ L = RSpan (S) (\{(R \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) -_{S} 1_{S}\})$
16		aks5lem6.16	$⊢ X = {var}_{1} (ℤ / N ℤ)$
17		aks5lem6.17	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
18		eluzelz	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ$
19	6 18	syl	$⊢ φ \to N \in ℤ$
20		0red	$⊢ φ \to 0 \in ℝ$
21		3re	$⊢ 3 \in ℝ$
22	21	a1i	$⊢ φ \to 3 \in ℝ$
23	19	zred	$⊢ φ \to N \in ℝ$
24		3pos	$⊢ 0 < 3$
25	24	a1i	$⊢ φ \to 0 < 3$
26		eluzle	$⊢ N \in ℤ_{\geq 3} \to 3 \leq N$
27	6 26	syl	$⊢ φ \to 3 \leq N$
28	20 22 23 25 27	ltletrd	$⊢ φ \to 0 < N$
29	19 28	jca	$⊢ φ \to (N \in ℤ \land 0 < N)$
30		elnnz	$⊢ N \in ℕ \leftrightarrow (N \in ℤ \land 0 < N)$
31	29 30	sylibr	$⊢ φ \to N \in ℕ$
32	4 31 7	3jca	$⊢ φ \to (P \in ℙ \land N \in ℕ \land P ∥ N)$
33		eqid	$⊢ S /_{𝑠} (S ~_{QG} L) = S /_{𝑠} (S ~_{QG} L)$
34	16	eqcomi	$⊢ {var}_{1} (ℤ / N ℤ) = X$
35	34	a1i	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to {var}_{1} (ℤ / N ℤ) = X$
36	35	oveq1d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to {var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a) = X +_{S} ℤRHom (S) (a)$
37	36	oveq2d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)) = N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a))$
38	37	eceq1d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L)$
39		simpr	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
40		eqcom	$⊢ {var}_{1} (ℤ / N ℤ) = X \leftrightarrow X = {var}_{1} (ℤ / N ℤ)$
41	40	imbi2i	$⊢ (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to {var}_{1} (ℤ / N ℤ) = X) \leftrightarrow (((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to X = {var}_{1} (ℤ / N ℤ))$
42	35 41	mpbi	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to X = {var}_{1} (ℤ / N ℤ)$
43	42	oveq2d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to N \cdot_{{mulGrp}_{S}} X = N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)$
44	43	oveq1d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to (N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a) = (N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a)$
45	44	eceq1d	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
46	38 39 45	3eqtrd	$⊢ ((φ \land a \in (1 \dots A)) \land [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
47	46	ex	$⊢ (φ \land a \in (1 \dots A)) \to ([(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) \to [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L))$
48	47	ralimdva	$⊢ φ \to (\forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} (X +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} X) +_{S} ℤRHom (S) (a))] (S ~_{QG} L) \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L))$
49	17 48	mpd	$⊢ φ \to \forall a \in (1 \dots A) [(N \cdot_{{mulGrp}_{S}} ({var}_{1} (ℤ / N ℤ) +_{S} ℤRHom (S) (a)))] (S ~_{QG} L) = [((N \cdot_{{mulGrp}_{S}} {var}_{1} (ℤ / N ℤ)) +_{S} ℤRHom (S) (a))] (S ~_{QG} L)$
50	3 2 32 33 15 5 1 14 49	aks5lem5a	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
51	1 2 3 4 5 6 7 8 9 10 11 12 13 50	aks6d1c7	$⊢ φ \to N = P^{P pCnt N}$

Metamath Proof Explorer

Theorem aks5lem6

Proof