Metamath Proof Explorer

Theorem aks5lem8

Description: Lemma for aks5. Clean up the conclusion. (Contributed by metakunt, 9-Aug-2025)

Ref Expression
Hypotheses aks5lem7.1 
|- ( ph -> ( # ` ( Base ` K ) ) e. NN )
aks5lem7.2 
|- P = ( chr ` K )
aks5lem7.3 
|- ( ph -> K e. Field )
aks5lem7.4 
|- ( ph -> P e. Prime )
aks5lem7.5 
|- ( ph -> R e. NN )
aks5lem7.6 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks5lem7.7 
|- ( ph -> P || N )
aks5lem7.8 
|- ( ph -> ( N gcd R ) = 1 )
aks5lem7.9 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks5lem7.10 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
aks5lem7.11 
|- ( ph -> R || ( ( # ` ( Base ` K ) ) - 1 ) )
aks5lem7.12 
|- ( 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 ) )
aks5lem7.13 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks5lem7.14 
|- S = ( Poly1 ` ( Z/nZ ` N ) )
aks5lem7.15 
|- L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
aks5lem7.16 
|- X = ( var1 ` ( Z/nZ ` N ) )
Assertion aks5lem8 
|- ( ph -> E. p e. Prime E. n e. NN N = ( p ^ n ) )

Proof

Step Hyp Ref Expression
1 aks5lem7.1 
 |-  ( ph -> ( # ` ( Base ` K ) ) e. NN )
2 aks5lem7.2 
 |-  P = ( chr ` K )
3 aks5lem7.3 
 |-  ( ph -> K e. Field )
4 aks5lem7.4 
 |-  ( ph -> P e. Prime )
5 aks5lem7.5 
 |-  ( ph -> R e. NN )
6 aks5lem7.6 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
7 aks5lem7.7 
 |-  ( ph -> P || N )
8 aks5lem7.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks5lem7.9 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10 aks5lem7.10 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11 aks5lem7.11 
 |-  ( ph -> R || ( ( # ` ( Base ` K ) ) - 1 ) )
12 aks5lem7.12 
 |-  ( 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 ) )
13 aks5lem7.13 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
14 aks5lem7.14 
 |-  S = ( Poly1 ` ( Z/nZ ` N ) )
15 aks5lem7.15 
 |-  L = ( ( RSpan ` S ) ` { ( ( R ( .g ` ( mulGrp ` S ) ) X ) ( -g ` S ) ( 1r ` S ) ) } )
16 aks5lem7.16 
 |-  X = ( var1 ` ( Z/nZ ` N ) )
17 simpr 
 |-  ( ( ph /\ p = P ) -> p = P )
18 17 oveq1d 
 |-  ( ( ph /\ p = P ) -> ( p ^ n ) = ( P ^ n ) )
19 18 eqeq2d 
 |-  ( ( ph /\ p = P ) -> ( N = ( p ^ n ) <-> N = ( P ^ n ) ) )
20 19 rexbidv 
 |-  ( ( ph /\ p = P ) -> ( E. n e. NN N = ( p ^ n ) <-> E. n e. NN N = ( P ^ n ) ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 aks5lem7 
 |-  ( ph -> N = ( P ^ ( P pCnt N ) ) )
22 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
23 6 22 syl 
 |-  ( ph -> N e. ZZ )
24 0red 
 |-  ( ph -> 0 e. RR )
25 3re 
 |-  3 e. RR
26 25 a1i 
 |-  ( ph -> 3 e. RR )
27 23 zred 
 |-  ( ph -> N e. RR )
28 3pos 
 |-  0 < 3
29 28 a1i 
 |-  ( ph -> 0 < 3 )
30 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
31 6 30 syl 
 |-  ( ph -> 3 <_ N )
32 24 26 27 29 31 ltletrd 
 |-  ( ph -> 0 < N )
33 23 32 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
34 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
35 33 34 sylibr 
 |-  ( ph -> N e. NN )
36 pcprmpw 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( E. n e. NN0 N = ( P ^ n ) <-> N = ( P ^ ( P pCnt N ) ) ) )
37 4 35 36 syl2anc 
 |-  ( ph -> ( E. n e. NN0 N = ( P ^ n ) <-> N = ( P ^ ( P pCnt N ) ) ) )
38 21 37 mpbird 
 |-  ( ph -> E. n e. NN0 N = ( P ^ n ) )
39 simprl 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> n e. NN0 )
40 39 nn0zd 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> n e. ZZ )
41 simpr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ 0 < n ) -> 0 < n )
42 39 nn0red 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> n e. RR )
43 0red 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> 0 e. RR )
44 42 43 lenltd 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( n <_ 0 <-> -. 0 < n ) )
45 44 bicomd 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( -. 0 < n <-> n <_ 0 ) )
46 45 biimpd 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( -. 0 < n -> n <_ 0 ) )
47 46 imp 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ -. 0 < n ) -> n <_ 0 )
48 simpr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> n <_ 0 )
49 39 adantr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> n e. NN0 )
50 nn0le0eq0 
 |-  ( n e. NN0 -> ( n <_ 0 <-> n = 0 ) )
51 50 bicomd 
 |-  ( n e. NN0 -> ( n = 0 <-> n <_ 0 ) )
52 49 51 syl 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> ( n = 0 <-> n <_ 0 ) )
53 48 52 mpbird 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> n = 0 )
54 simplrr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> N = ( P ^ n ) )
55 simpr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> n = 0 )
56 55 oveq2d 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> ( P ^ n ) = ( P ^ 0 ) )
57 4 ad2antrr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> P e. Prime )
58 prmnn 
 |-  ( P e. Prime -> P e. NN )
59 57 58 syl 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> P e. NN )
60 59 nncnd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> P e. CC )
61 60 exp0d 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> ( P ^ 0 ) = 1 )
62 56 61 eqtrd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> ( P ^ n ) = 1 )
63 54 62 eqtrd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> N = 1 )
64 1red 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> 1 e. RR )
65 1red 
 |-  ( ph -> 1 e. RR )
66 35 nnred 
 |-  ( ph -> N e. RR )
67 1lt3 
 |-  1 < 3
68 67 a1i 
 |-  ( ph -> 1 < 3 )
69 65 26 66 68 31 ltletrd 
 |-  ( ph -> 1 < N )
70 69 adantr 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> 1 < N )
71 70 adantr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> 1 < N )
72 64 71 ltned 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> 1 =/= N )
73 72 necomd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> N =/= 1 )
74 73 neneqd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> -. N = 1 )
75 63 74 pm2.21dd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n = 0 ) -> 0 < n )
76 75 ex 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( n = 0 -> 0 < n ) )
77 76 adantr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> ( n = 0 -> 0 < n ) )
78 53 77 mpd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ n <_ 0 ) -> 0 < n )
79 78 ex 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( n <_ 0 -> 0 < n ) )
80 79 adantr 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ -. 0 < n ) -> ( n <_ 0 -> 0 < n ) )
81 47 80 mpd 
 |-  ( ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) /\ -. 0 < n ) -> 0 < n )
82 41 81 pm2.61dan 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> 0 < n )
83 40 82 jca 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> ( n e. ZZ /\ 0 < n ) )
84 elnnz 
 |-  ( n e. NN <-> ( n e. ZZ /\ 0 < n ) )
85 83 84 sylibr 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> n e. NN )
86 simprr 
 |-  ( ( ph /\ ( n e. NN0 /\ N = ( P ^ n ) ) ) -> N = ( P ^ n ) )
87 38 85 86 reximssdv 
 |-  ( ph -> E. n e. NN N = ( P ^ n ) )
88 4 20 87 rspcedvd 
 |-  ( ph -> E. p e. Prime E. n e. NN N = ( p ^ n ) )