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