Metamath Proof Explorer

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 
|- .~ = { <. 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 ) ) ) }
aks6d1c7.2 
|- P = ( chr ` K )
aks6d1c7.3 
|- ( ph -> K e. Field )
aks6d1c7.4 
|- ( ph -> P e. Prime )
aks6d1c7.5 
|- ( ph -> R e. NN )
aks6d1c7.6 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks6d1c7.7 
|- ( ph -> P || N )
aks6d1c7.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c7.9 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks6d1c7.10 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
aks6d1c7.11 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c7.12 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c7.13 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks6d1c7.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
Assertion aks6d1c7lem4 
|- ( ph -> E! p e. Prime p || N )

Proof

Step Hyp Ref Expression
1 aks6d1c7.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 aks6d1c7.2 
 |-  P = ( chr ` K )
3 aks6d1c7.3 
 |-  ( ph -> K e. Field )
4 aks6d1c7.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c7.5 
 |-  ( ph -> R e. NN )
6 aks6d1c7.6 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
7 aks6d1c7.7 
 |-  ( ph -> P || N )
8 aks6d1c7.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c7.9 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10 aks6d1c7.10 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11 aks6d1c7.11 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
12 aks6d1c7.12 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
13 aks6d1c7.13 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
14 aks6d1c7.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 3 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> K e. Field )
16 4 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> P e. Prime )
17 5 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> R e. NN )
18 6 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> N e. ( ZZ>= ` 3 ) )
19 7 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> P || N )
20 8 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> ( N gcd R ) = 1 )
21 10 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
22 11 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
23 12 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
24 13 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
25 14 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
26 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> p e. Prime )
27 simpr 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> p || N )
28 26 27 jca 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> ( p e. Prime /\ p || N ) )
29 1 2 15 16 17 18 19 20 9 21 22 23 24 25 28 aks6d1c7lem3 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> P = p )
30 29 eqcomd 
 |-  ( ( ( ph /\ p e. Prime ) /\ p || N ) -> p = P )
31 30 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( p || N -> p = P ) )
32 31 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p || N -> p = P ) )
33 4 7 32 3jca 
 |-  ( ph -> ( P e. Prime /\ P || N /\ A. p e. Prime ( p || N -> p = P ) ) )
34 breq1 
 |-  ( p = P -> ( p || N <-> P || N ) )
35 34 eqreu 
 |-  ( ( P e. Prime /\ P || N /\ A. p e. Prime ( p || N -> p = P ) ) -> E! p e. Prime p || N )
36 33 35 syl 
 |-  ( ph -> E! p e. Prime p || N )