Metamath Proof Explorer

Theorem aks6d1c7

Description: N is a prime power if the hypotheses of the AKS algorithm hold. Claim 7 of Theorem 6.1 https://www3.nd.edu/%7eandyp/notes/AKS.pdf . (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 aks6d1c7 
|- ( ph -> N = ( P ^ ( P pCnt 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 simpr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> q = r )
16 7 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> P || N )
17 breq1 
 |-  ( s = P -> ( s || N <-> P || N ) )
18 eqeq1 
 |-  ( s = P -> ( s = r <-> P = r ) )
19 17 18 bibi12d 
 |-  ( s = P -> ( ( s || N <-> s = r ) <-> ( P || N <-> P = r ) ) )
20 nfv 
 |-  F/ s ( p || N <-> p = r )
21 nfv 
 |-  F/ p ( s || N <-> s = r )
22 breq1 
 |-  ( p = s -> ( p || N <-> s || N ) )
23 equequ1 
 |-  ( p = s -> ( p = r <-> s = r ) )
24 22 23 bibi12d 
 |-  ( p = s -> ( ( p || N <-> p = r ) <-> ( s || N <-> s = r ) ) )
25 20 21 24 cbvralw 
 |-  ( A. p e. Prime ( p || N <-> p = r ) <-> A. s e. Prime ( s || N <-> s = r ) )
26 25 biimpi 
 |-  ( A. p e. Prime ( p || N <-> p = r ) -> A. s e. Prime ( s || N <-> s = r ) )
27 26 adantl 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> A. s e. Prime ( s || N <-> s = r ) )
28 4 ad2antrr 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> P e. Prime )
29 19 27 28 rspcdva 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> ( P || N <-> P = r ) )
30 29 biimpd 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> ( P || N -> P = r ) )
31 16 30 mpd 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> P = r )
32 31 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> P = r )
33 32 eqcomd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> r = P )
34 15 33 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> q = P )
35 34 oveq1d 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( q pCnt N ) = ( P pCnt N ) )
36 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
37 6 36 syl 
 |-  ( ph -> N e. ZZ )
38 0red 
 |-  ( ph -> 0 e. RR )
39 3re 
 |-  3 e. RR
40 39 a1i 
 |-  ( ph -> 3 e. RR )
41 37 zred 
 |-  ( ph -> N e. RR )
42 3pos 
 |-  0 < 3
43 42 a1i 
 |-  ( ph -> 0 < 3 )
44 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
45 6 44 syl 
 |-  ( ph -> 3 <_ N )
46 38 40 41 43 45 ltletrd 
 |-  ( ph -> 0 < N )
47 37 46 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
48 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
49 47 48 sylibr 
 |-  ( ph -> N e. NN )
50 pcelnn 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )
51 4 49 50 syl2anc 
 |-  ( ph -> ( ( P pCnt N ) e. NN <-> P || N ) )
52 7 51 mpbird 
 |-  ( ph -> ( P pCnt N ) e. NN )
53 52 nncnd 
 |-  ( ph -> ( P pCnt N ) e. CC )
54 53 mulridd 
 |-  ( ph -> ( ( P pCnt N ) x. 1 ) = ( P pCnt N ) )
55 54 eqcomd 
 |-  ( ph -> ( P pCnt N ) = ( ( P pCnt N ) x. 1 ) )
56 1nn0 
 |-  1 e. NN0
57 56 a1i 
 |-  ( ph -> 1 e. NN0 )
58 pcidlem 
 |-  ( ( P e. Prime /\ 1 e. NN0 ) -> ( P pCnt ( P ^ 1 ) ) = 1 )
59 4 57 58 syl2anc 
 |-  ( ph -> ( P pCnt ( P ^ 1 ) ) = 1 )
60 59 eqcomd 
 |-  ( ph -> 1 = ( P pCnt ( P ^ 1 ) ) )
61 prmnn 
 |-  ( P e. Prime -> P e. NN )
62 4 61 syl 
 |-  ( ph -> P e. NN )
63 62 nncnd 
 |-  ( ph -> P e. CC )
64 63 exp1d 
 |-  ( ph -> ( P ^ 1 ) = P )
65 64 oveq2d 
 |-  ( ph -> ( P pCnt ( P ^ 1 ) ) = ( P pCnt P ) )
66 60 65 eqtrd 
 |-  ( ph -> 1 = ( P pCnt P ) )
67 66 oveq2d 
 |-  ( ph -> ( ( P pCnt N ) x. 1 ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
68 55 67 eqtrd 
 |-  ( ph -> ( P pCnt N ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
69 68 adantr 
 |-  ( ( ph /\ r e. Prime ) -> ( P pCnt N ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt N ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
71 28 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> P e. Prime )
72 nnq 
 |-  ( P e. NN -> P e. QQ )
73 62 72 syl 
 |-  ( ph -> P e. QQ )
74 62 nnne0d 
 |-  ( ph -> P =/= 0 )
75 73 74 jca 
 |-  ( ph -> ( P e. QQ /\ P =/= 0 ) )
76 75 adantr 
 |-  ( ( ph /\ r e. Prime ) -> ( P e. QQ /\ P =/= 0 ) )
77 76 ad3antrrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P e. QQ /\ P =/= 0 ) )
78 52 nnzd 
 |-  ( ph -> ( P pCnt N ) e. ZZ )
79 78 adantr 
 |-  ( ( ph /\ r e. Prime ) -> ( P pCnt N ) e. ZZ )
80 79 adantr 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> ( P pCnt N ) e. ZZ )
81 80 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( P pCnt N ) e. ZZ )
82 81 adantr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt N ) e. ZZ )
83 pcexp 
 |-  ( ( P e. Prime /\ ( P e. QQ /\ P =/= 0 ) /\ ( P pCnt N ) e. ZZ ) -> ( P pCnt ( P ^ ( P pCnt N ) ) ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
84 71 77 82 83 syl3anc 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt ( P ^ ( P pCnt N ) ) ) = ( ( P pCnt N ) x. ( P pCnt P ) ) )
85 84 eqcomd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( ( P pCnt N ) x. ( P pCnt P ) ) = ( P pCnt ( P ^ ( P pCnt N ) ) ) )
86 70 85 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt N ) = ( P pCnt ( P ^ ( P pCnt N ) ) ) )
87 34 eqcomd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> P = q )
88 87 oveq1d 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt ( P ^ ( P pCnt N ) ) ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
89 86 88 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( P pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
90 35 89 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ q = r ) -> ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
91 breq1 
 |-  ( s = q -> ( s || N <-> q || N ) )
92 equequ1 
 |-  ( s = q -> ( s = r <-> q = r ) )
93 91 92 bibi12d 
 |-  ( s = q -> ( ( s || N <-> s = r ) <-> ( q || N <-> q = r ) ) )
94 27 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> A. s e. Prime ( s || N <-> s = r ) )
95 simpr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> q e. Prime )
96 93 94 95 rspcdva 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( q || N <-> q = r ) )
97 96 bicomd 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( q = r <-> q || N ) )
98 97 notbid 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( -. q = r <-> -. q || N ) )
99 98 biimpa 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> -. q || N )
100 95 adantr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> q e. Prime )
101 49 adantr 
 |-  ( ( ph /\ r e. Prime ) -> N e. NN )
102 101 ad3antrrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> N e. NN )
103 pceq0 
 |-  ( ( q e. Prime /\ N e. NN ) -> ( ( q pCnt N ) = 0 <-> -. q || N ) )
104 100 102 103 syl2anc 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( ( q pCnt N ) = 0 <-> -. q || N ) )
105 99 104 mpbird 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( q pCnt N ) = 0 )
106 neqne 
 |-  ( -. q = r -> q =/= r )
107 106 adantl 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> q =/= r )
108 16 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> P || N )
109 28 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> P e. Prime )
110 19 94 109 rspcdva 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( P || N <-> P = r ) )
111 110 biimpd 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( P || N -> P = r ) )
112 108 111 mpd 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> P = r )
113 112 adantr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> P = r )
114 113 eqcomd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> r = P )
115 107 114 neeqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> q =/= P )
116 115 neneqd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> -. q = P )
117 prmuz2 
 |-  ( q e. Prime -> q e. ( ZZ>= ` 2 ) )
118 117 adantl 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> q e. ( ZZ>= ` 2 ) )
119 118 adantr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> q e. ( ZZ>= ` 2 ) )
120 28 ad2antrr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> P e. Prime )
121 dvdsprm 
 |-  ( ( q e. ( ZZ>= ` 2 ) /\ P e. Prime ) -> ( q || P <-> q = P ) )
122 119 120 121 syl2anc 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( q || P <-> q = P ) )
123 116 122 mtbird 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> -. q || P )
124 62 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> P e. NN )
125 124 nnzd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> P e. ZZ )
126 52 adantr 
 |-  ( ( ph /\ r e. Prime ) -> ( P pCnt N ) e. NN )
127 126 adantr 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> ( P pCnt N ) e. NN )
128 127 adantr 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( P pCnt N ) e. NN )
129 128 adantr 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( P pCnt N ) e. NN )
130 prmdvdsexp 
 |-  ( ( q e. Prime /\ P e. ZZ /\ ( P pCnt N ) e. NN ) -> ( q || ( P ^ ( P pCnt N ) ) <-> q || P ) )
131 100 125 129 130 syl3anc 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( q || ( P ^ ( P pCnt N ) ) <-> q || P ) )
132 123 131 mtbird 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> -. q || ( P ^ ( P pCnt N ) ) )
133 120 102 pccld 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( P pCnt N ) e. NN0 )
134 124 133 nnexpcld 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( P ^ ( P pCnt N ) ) e. NN )
135 pceq0 
 |-  ( ( q e. Prime /\ ( P ^ ( P pCnt N ) ) e. NN ) -> ( ( q pCnt ( P ^ ( P pCnt N ) ) ) = 0 <-> -. q || ( P ^ ( P pCnt N ) ) ) )
136 100 134 135 syl2anc 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( ( q pCnt ( P ^ ( P pCnt N ) ) ) = 0 <-> -. q || ( P ^ ( P pCnt N ) ) ) )
137 132 136 mpbird 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( q pCnt ( P ^ ( P pCnt N ) ) ) = 0 )
138 137 eqcomd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> 0 = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
139 105 138 eqtrd 
 |-  ( ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) /\ -. q = r ) -> ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
140 90 139 pm2.61dan 
 |-  ( ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) /\ q e. Prime ) -> ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
141 140 ralrimiva 
 |-  ( ( ( ph /\ r e. Prime ) /\ A. p e. Prime ( p || N <-> p = r ) ) -> A. q e. Prime ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
142 1 2 3 4 5 6 7 8 9 10 11 12 13 14 aks6d1c7lem4 
 |-  ( ph -> E! p e. Prime p || N )
143 reu6 
 |-  ( E! p e. Prime p || N <-> E. r e. Prime A. p e. Prime ( p || N <-> p = r ) )
144 142 143 sylib 
 |-  ( ph -> E. r e. Prime A. p e. Prime ( p || N <-> p = r ) )
145 141 144 r19.29a 
 |-  ( ph -> A. q e. Prime ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) )
146 49 nnnn0d 
 |-  ( ph -> N e. NN0 )
147 62 nnnn0d 
 |-  ( ph -> P e. NN0 )
148 4 49 pccld 
 |-  ( ph -> ( P pCnt N ) e. NN0 )
149 147 148 nn0expcld 
 |-  ( ph -> ( P ^ ( P pCnt N ) ) e. NN0 )
150 pc11 
 |-  ( ( N e. NN0 /\ ( P ^ ( P pCnt N ) ) e. NN0 ) -> ( N = ( P ^ ( P pCnt N ) ) <-> A. q e. Prime ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) ) )
151 146 149 150 syl2anc 
 |-  ( ph -> ( N = ( P ^ ( P pCnt N ) ) <-> A. q e. Prime ( q pCnt N ) = ( q pCnt ( P ^ ( P pCnt N ) ) ) ) )
152 145 151 mpbird 
 |-  ( ph -> N = ( P ^ ( P pCnt N ) ) )