aks5lem6

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

	Ref	Expression
Hypotheses	aks5lem6.1	\|- .~ = { <. e , f >. \| ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
	aks5lem6.2	\|- P = ( chr ` K )
	aks5lem6.3	\|- ( ph -> K e. Field )
	aks5lem6.4	\|- ( ph -> P e. Prime )
	aks5lem6.5	\|- ( ph -> R e. NN )
	aks5lem6.6	\|- ( ph -> N e. ( ZZ>= ` 3 ) )
	aks5lem6.7	\|- ( ph -> P \|\| N )
	aks5lem6.8	\|- ( ph -> ( N gcd R ) = 1 )
	aks5lem6.9	\|- A = ( \|_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
	aks5lem6.10	\|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
	aks5lem6.11	\|- ( ph -> ( x e. ( Base ` K ) \|-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
	aks5lem6.12	\|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
	aks5lem6.13	\|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
	aks5lem6.14	\|- S = ( Poly1 ` ( Z/nZ ` N ) )
	aks5lem6.15	\|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
	aks5lem6.16	\|- X = ( var1 ` ( Z/nZ ` N ) )
	aks5lem6.17	\|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
Assertion	aks5lem6	\|- ( ph -> N = ( P ^ ( P pCnt N ) ) )

Proof

Step	Hyp	Ref	Expression
1		aks5lem6.1	\|- .~ = { <. e , f >. \| ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2		aks5lem6.2	\|- P = ( chr ` K )
3		aks5lem6.3	\|- ( ph -> K e. Field )
4		aks5lem6.4	\|- ( ph -> P e. Prime )
5		aks5lem6.5	\|- ( ph -> R e. NN )
6		aks5lem6.6	\|- ( ph -> N e. ( ZZ>= ` 3 ) )
7		aks5lem6.7	\|- ( ph -> P \|\| N )
8		aks5lem6.8	\|- ( ph -> ( N gcd R ) = 1 )
9		aks5lem6.9	\|- A = ( \|_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10		aks5lem6.10	\|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11		aks5lem6.11	\|- ( ph -> ( x e. ( Base ` K ) \|-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
12		aks5lem6.12	\|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
13		aks5lem6.13	\|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
14		aks5lem6.14	\|- S = ( Poly1 ` ( Z/nZ ` N ) )
15		aks5lem6.15	\|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( -g ` S ) ( 1r ` S ) ) } )
16		aks5lem6.16	\|- X = ( var1 ` ( Z/nZ ` N ) )
17		aks5lem6.17	\|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
18		eluzelz	\|- ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
19	6 18	syl	\|- ( ph -> N e. ZZ )
20		0red	\|- ( ph -> 0 e. RR )
21		3re	\|- 3 e. RR
22	21	a1i	\|- ( ph -> 3 e. RR )
23	19	zred	\|- ( ph -> N e. RR )
24		3pos	\|- 0 < 3
25	24	a1i	\|- ( ph -> 0 < 3 )
26		eluzle	\|- ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
27	6 26	syl	\|- ( ph -> 3 <_ N )
28	20 22 23 25 27	ltletrd	\|- ( ph -> 0 < N )
29	19 28	jca	\|- ( ph -> ( N e. ZZ /\ 0 < N ) )
30		elnnz	\|- ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
31	29 30	sylibr	\|- ( ph -> N e. NN )
32	4 31 7	3jca	\|- ( ph -> ( P e. Prime /\ N e. NN /\ P \|\| N ) )
33		eqid	\|- ( S /s ( S ~QG L ) ) = ( S /s ( S ~QG L ) )
34	16	eqcomi	\|- ( var1 ` ( Z/nZ ` N ) ) = X
35	34	a1i	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( var1 ` ( Z/nZ ` N ) ) = X )
36	35	oveq1d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) = ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) )
37	36	oveq2d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) = ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) )
38	37	eceq1d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) )
39		simpr	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
40		eqcom	\|- ( ( var1 ` ( Z/nZ ` N ) ) = X <-> X = ( var1 ` ( Z/nZ ` N ) ) )
41	40	imbi2i	\|- ( ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( var1 ` ( Z/nZ ` N ) ) = X ) <-> ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> X = ( var1 ` ( Z/nZ ` N ) ) ) )
42	35 41	mpbi	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> X = ( var1 ` ( Z/nZ ` N ) ) )
43	42	oveq2d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( N ( .g ` ( mulGrp ` S ) ) X ) = ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) )
44	43	oveq1d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) = ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) )
45	44	eceq1d	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
46	38 39 45	3eqtrd	\|- ( ( ( ph /\ a e. ( 1 ... A ) ) /\ [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
47	46	ex	\|- ( ( ph /\ a e. ( 1 ... A ) ) -> ( [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) -> [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) )
48	47	ralimdva	\|- ( ph -> ( A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( X ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) X ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) ) )
49	17 48	mpd	\|- ( ph -> A. a e. ( 1 ... A ) [ ( N ( .g ` ( mulGrp ` S ) ) ( ( var1 ` ( Z/nZ ` N ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ) ] ( S ~QG L ) = [ ( ( N ( .g ` ( mulGrp ` S ) ) ( var1 ` ( Z/nZ ` N ) ) ) ( +g ` S ) ( ( ZRHom ` S ) ` a ) ) ] ( S ~QG L ) )
50	3 2 32 33 15 5 1 14 49	aks5lem5a	\|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
51	1 2 3 4 5 6 7 8 9 10 11 12 13 50	aks6d1c7	\|- ( ph -> N = ( P ^ ( P pCnt N ) ) )

Metamath Proof Explorer

Theorem aks5lem6

Proof