Metamath Proof Explorer

Theorem pockthlem

Description: Lemma for pockthg . (Contributed by Mario Carneiro, 2-Mar-2014)

Ref Expression
Hypotheses pockthg.1 
|- ( ph -> A e. NN )
pockthg.2 
|- ( ph -> B e. NN )
pockthg.3 
|- ( ph -> B < A )
pockthg.4 
|- ( ph -> N = ( ( A x. B ) + 1 ) )
pockthlem.5 
|- ( ph -> P e. Prime )
pockthlem.6 
|- ( ph -> P || N )
pockthlem.7 
|- ( ph -> Q e. Prime )
pockthlem.8 
|- ( ph -> ( Q pCnt A ) e. NN )
pockthlem.9 
|- ( ph -> C e. ZZ )
pockthlem.10 
|- ( ph -> ( ( C ^ ( N - 1 ) ) mod N ) = 1 )
pockthlem.11 
|- ( ph -> ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) = 1 )
Assertion pockthlem 
|- ( ph -> ( Q pCnt A ) <_ ( Q pCnt ( P - 1 ) ) )

Proof

Step Hyp Ref Expression
1 pockthg.1 
 |-  ( ph -> A e. NN )
2 pockthg.2 
 |-  ( ph -> B e. NN )
3 pockthg.3 
 |-  ( ph -> B < A )
4 pockthg.4 
 |-  ( ph -> N = ( ( A x. B ) + 1 ) )
5 pockthlem.5 
 |-  ( ph -> P e. Prime )
6 pockthlem.6 
 |-  ( ph -> P || N )
7 pockthlem.7 
 |-  ( ph -> Q e. Prime )
8 pockthlem.8 
 |-  ( ph -> ( Q pCnt A ) e. NN )
9 pockthlem.9 
 |-  ( ph -> C e. ZZ )
10 pockthlem.10 
 |-  ( ph -> ( ( C ^ ( N - 1 ) ) mod N ) = 1 )
11 pockthlem.11 
 |-  ( ph -> ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) = 1 )
12 prmnn 
 |-  ( Q e. Prime -> Q e. NN )
13 7 12 syl 
 |-  ( ph -> Q e. NN )
14 8 nnnn0d 
 |-  ( ph -> ( Q pCnt A ) e. NN0 )
15 13 14 nnexpcld 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) e. NN )
16 15 nnzd 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) e. ZZ )
17 prmnn 
 |-  ( P e. Prime -> P e. NN )
18 5 17 syl 
 |-  ( ph -> P e. NN )
19 18 nnzd 
 |-  ( ph -> P e. ZZ )
20 gcddvds 
 |-  ( ( C e. ZZ /\ P e. ZZ ) -> ( ( C gcd P ) || C /\ ( C gcd P ) || P ) )
21 9 19 20 syl2anc 
 |-  ( ph -> ( ( C gcd P ) || C /\ ( C gcd P ) || P ) )
22 21 simpld 
 |-  ( ph -> ( C gcd P ) || C )
23 9 19 gcdcld 
 |-  ( ph -> ( C gcd P ) e. NN0 )
24 23 nn0zd 
 |-  ( ph -> ( C gcd P ) e. ZZ )
25 1 2 nnmulcld 
 |-  ( ph -> ( A x. B ) e. NN )
26 nnuz 
 |-  NN = ( ZZ>= ` 1 )
27 25 26 eleqtrdi 
 |-  ( ph -> ( A x. B ) e. ( ZZ>= ` 1 ) )
28 eluzp1p1 
 |-  ( ( A x. B ) e. ( ZZ>= ` 1 ) -> ( ( A x. B ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
29 27 28 syl 
 |-  ( ph -> ( ( A x. B ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
30 4 29 eqeltrd 
 |-  ( ph -> N e. ( ZZ>= ` ( 1 + 1 ) ) )
31 df-2 
 |-  2 = ( 1 + 1 )
32 31 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
33 30 32 eleqtrrdi 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
34 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
35 33 34 sylib 
 |-  ( ph -> ( N e. NN /\ 1 < N ) )
36 35 simpld 
 |-  ( ph -> N e. NN )
37 36 nnzd 
 |-  ( ph -> N e. ZZ )
38 21 simprd 
 |-  ( ph -> ( C gcd P ) || P )
39 24 19 37 38 6 dvdstrd 
 |-  ( ph -> ( C gcd P ) || N )
40 36 nnne0d 
 |-  ( ph -> N =/= 0 )
41 simpr 
 |-  ( ( C = 0 /\ N = 0 ) -> N = 0 )
42 41 necon3ai 
 |-  ( N =/= 0 -> -. ( C = 0 /\ N = 0 ) )
43 40 42 syl 
 |-  ( ph -> -. ( C = 0 /\ N = 0 ) )
44 dvdslegcd 
 |-  ( ( ( ( C gcd P ) e. ZZ /\ C e. ZZ /\ N e. ZZ ) /\ -. ( C = 0 /\ N = 0 ) ) -> ( ( ( C gcd P ) || C /\ ( C gcd P ) || N ) -> ( C gcd P ) <_ ( C gcd N ) ) )
45 24 9 37 43 44 syl31anc 
 |-  ( ph -> ( ( ( C gcd P ) || C /\ ( C gcd P ) || N ) -> ( C gcd P ) <_ ( C gcd N ) ) )
46 22 39 45 mp2and 
 |-  ( ph -> ( C gcd P ) <_ ( C gcd N ) )
47 10 oveq1d 
 |-  ( ph -> ( ( ( C ^ ( N - 1 ) ) mod N ) gcd N ) = ( 1 gcd N ) )
48 1z 
 |-  1 e. ZZ
49 eluzp1m1 
 |-  ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
50 48 30 49 sylancr 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
51 50 26 eleqtrrdi 
 |-  ( ph -> ( N - 1 ) e. NN )
52 51 nnnn0d 
 |-  ( ph -> ( N - 1 ) e. NN0 )
53 zexpcl 
 |-  ( ( C e. ZZ /\ ( N - 1 ) e. NN0 ) -> ( C ^ ( N - 1 ) ) e. ZZ )
54 9 52 53 syl2anc 
 |-  ( ph -> ( C ^ ( N - 1 ) ) e. ZZ )
55 modgcd 
 |-  ( ( ( C ^ ( N - 1 ) ) e. ZZ /\ N e. NN ) -> ( ( ( C ^ ( N - 1 ) ) mod N ) gcd N ) = ( ( C ^ ( N - 1 ) ) gcd N ) )
56 54 36 55 syl2anc 
 |-  ( ph -> ( ( ( C ^ ( N - 1 ) ) mod N ) gcd N ) = ( ( C ^ ( N - 1 ) ) gcd N ) )
57 gcdcom 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( 1 gcd N ) = ( N gcd 1 ) )
58 48 37 57 sylancr 
 |-  ( ph -> ( 1 gcd N ) = ( N gcd 1 ) )
59 gcd1 
 |-  ( N e. ZZ -> ( N gcd 1 ) = 1 )
60 37 59 syl 
 |-  ( ph -> ( N gcd 1 ) = 1 )
61 58 60 eqtrd 
 |-  ( ph -> ( 1 gcd N ) = 1 )
62 47 56 61 3eqtr3d 
 |-  ( ph -> ( ( C ^ ( N - 1 ) ) gcd N ) = 1 )
63 rpexp 
 |-  ( ( C e. ZZ /\ N e. ZZ /\ ( N - 1 ) e. NN ) -> ( ( ( C ^ ( N - 1 ) ) gcd N ) = 1 <-> ( C gcd N ) = 1 ) )
64 9 37 51 63 syl3anc 
 |-  ( ph -> ( ( ( C ^ ( N - 1 ) ) gcd N ) = 1 <-> ( C gcd N ) = 1 ) )
65 62 64 mpbid 
 |-  ( ph -> ( C gcd N ) = 1 )
66 46 65 breqtrd 
 |-  ( ph -> ( C gcd P ) <_ 1 )
67 18 nnne0d 
 |-  ( ph -> P =/= 0 )
68 simpr 
 |-  ( ( C = 0 /\ P = 0 ) -> P = 0 )
69 68 necon3ai 
 |-  ( P =/= 0 -> -. ( C = 0 /\ P = 0 ) )
70 67 69 syl 
 |-  ( ph -> -. ( C = 0 /\ P = 0 ) )
71 gcdn0cl 
 |-  ( ( ( C e. ZZ /\ P e. ZZ ) /\ -. ( C = 0 /\ P = 0 ) ) -> ( C gcd P ) e. NN )
72 9 19 70 71 syl21anc 
 |-  ( ph -> ( C gcd P ) e. NN )
73 nnle1eq1 
 |-  ( ( C gcd P ) e. NN -> ( ( C gcd P ) <_ 1 <-> ( C gcd P ) = 1 ) )
74 72 73 syl 
 |-  ( ph -> ( ( C gcd P ) <_ 1 <-> ( C gcd P ) = 1 ) )
75 66 74 mpbid 
 |-  ( ph -> ( C gcd P ) = 1 )
76 odzcl 
 |-  ( ( P e. NN /\ C e. ZZ /\ ( C gcd P ) = 1 ) -> ( ( odZ ` P ) ` C ) e. NN )
77 18 9 75 76 syl3anc 
 |-  ( ph -> ( ( odZ ` P ) ` C ) e. NN )
78 77 nnzd 
 |-  ( ph -> ( ( odZ ` P ) ` C ) e. ZZ )
79 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
80 5 79 syl 
 |-  ( ph -> P e. ( ZZ>= ` 2 ) )
81 80 32 eleqtrdi 
 |-  ( ph -> P e. ( ZZ>= ` ( 1 + 1 ) ) )
82 eluzp1m1 
 |-  ( ( 1 e. ZZ /\ P e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( P - 1 ) e. ( ZZ>= ` 1 ) )
83 48 81 82 sylancr 
 |-  ( ph -> ( P - 1 ) e. ( ZZ>= ` 1 ) )
84 83 26 eleqtrrdi 
 |-  ( ph -> ( P - 1 ) e. NN )
85 84 nnzd 
 |-  ( ph -> ( P - 1 ) e. ZZ )
86 1 nnzd 
 |-  ( ph -> A e. ZZ )
87 51 nnzd 
 |-  ( ph -> ( N - 1 ) e. ZZ )
88 pcdvds 
 |-  ( ( Q e. Prime /\ A e. NN ) -> ( Q ^ ( Q pCnt A ) ) || A )
89 7 1 88 syl2anc 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) || A )
90 2 nnzd 
 |-  ( ph -> B e. ZZ )
91 dvdsmul1 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A || ( A x. B ) )
92 86 90 91 syl2anc 
 |-  ( ph -> A || ( A x. B ) )
93 4 oveq1d 
 |-  ( ph -> ( N - 1 ) = ( ( ( A x. B ) + 1 ) - 1 ) )
94 25 nncnd 
 |-  ( ph -> ( A x. B ) e. CC )
95 ax-1cn 
 |-  1 e. CC
96 pncan 
 |-  ( ( ( A x. B ) e. CC /\ 1 e. CC ) -> ( ( ( A x. B ) + 1 ) - 1 ) = ( A x. B ) )
97 94 95 96 sylancl 
 |-  ( ph -> ( ( ( A x. B ) + 1 ) - 1 ) = ( A x. B ) )
98 93 97 eqtrd 
 |-  ( ph -> ( N - 1 ) = ( A x. B ) )
99 92 98 breqtrrd 
 |-  ( ph -> A || ( N - 1 ) )
100 16 86 87 89 99 dvdstrd 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) || ( N - 1 ) )
101 15 nnne0d 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) =/= 0 )
102 dvdsval2 
 |-  ( ( ( Q ^ ( Q pCnt A ) ) e. ZZ /\ ( Q ^ ( Q pCnt A ) ) =/= 0 /\ ( N - 1 ) e. ZZ ) -> ( ( Q ^ ( Q pCnt A ) ) || ( N - 1 ) <-> ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. ZZ ) )
103 16 101 87 102 syl3anc 
 |-  ( ph -> ( ( Q ^ ( Q pCnt A ) ) || ( N - 1 ) <-> ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. ZZ ) )
104 100 103 mpbid 
 |-  ( ph -> ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. ZZ )
105 peano2zm 
 |-  ( ( C ^ ( N - 1 ) ) e. ZZ -> ( ( C ^ ( N - 1 ) ) - 1 ) e. ZZ )
106 54 105 syl 
 |-  ( ph -> ( ( C ^ ( N - 1 ) ) - 1 ) e. ZZ )
107 36 nnred 
 |-  ( ph -> N e. RR )
108 35 simprd 
 |-  ( ph -> 1 < N )
109 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
110 107 108 109 syl2anc 
 |-  ( ph -> ( 1 mod N ) = 1 )
111 10 110 eqtr4d 
 |-  ( ph -> ( ( C ^ ( N - 1 ) ) mod N ) = ( 1 mod N ) )
112 1zzd 
 |-  ( ph -> 1 e. ZZ )
113 moddvds 
 |-  ( ( N e. NN /\ ( C ^ ( N - 1 ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( C ^ ( N - 1 ) ) mod N ) = ( 1 mod N ) <-> N || ( ( C ^ ( N - 1 ) ) - 1 ) ) )
114 36 54 112 113 syl3anc 
 |-  ( ph -> ( ( ( C ^ ( N - 1 ) ) mod N ) = ( 1 mod N ) <-> N || ( ( C ^ ( N - 1 ) ) - 1 ) ) )
115 111 114 mpbid 
 |-  ( ph -> N || ( ( C ^ ( N - 1 ) ) - 1 ) )
116 19 37 106 6 115 dvdstrd 
 |-  ( ph -> P || ( ( C ^ ( N - 1 ) ) - 1 ) )
117 odzdvds 
 |-  ( ( ( P e. NN /\ C e. ZZ /\ ( C gcd P ) = 1 ) /\ ( N - 1 ) e. NN0 ) -> ( P || ( ( C ^ ( N - 1 ) ) - 1 ) <-> ( ( odZ ` P ) ` C ) || ( N - 1 ) ) )
118 18 9 75 52 117 syl31anc 
 |-  ( ph -> ( P || ( ( C ^ ( N - 1 ) ) - 1 ) <-> ( ( odZ ` P ) ` C ) || ( N - 1 ) ) )
119 116 118 mpbid 
 |-  ( ph -> ( ( odZ ` P ) ` C ) || ( N - 1 ) )
120 51 nncnd 
 |-  ( ph -> ( N - 1 ) e. CC )
121 15 nncnd 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) e. CC )
122 120 121 101 divcan1d 
 |-  ( ph -> ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( Q pCnt A ) ) ) = ( N - 1 ) )
123 119 122 breqtrrd 
 |-  ( ph -> ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( Q pCnt A ) ) ) )
124 nprmdvds1 
 |-  ( P e. Prime -> -. P || 1 )
125 5 124 syl 
 |-  ( ph -> -. P || 1 )
126 13 nnzd 
 |-  ( ph -> Q e. ZZ )
127 iddvdsexp 
 |-  ( ( Q e. ZZ /\ ( Q pCnt A ) e. NN ) -> Q || ( Q ^ ( Q pCnt A ) ) )
128 126 8 127 syl2anc 
 |-  ( ph -> Q || ( Q ^ ( Q pCnt A ) ) )
129 126 16 87 128 100 dvdstrd 
 |-  ( ph -> Q || ( N - 1 ) )
130 13 nnne0d 
 |-  ( ph -> Q =/= 0 )
131 dvdsval2 
 |-  ( ( Q e. ZZ /\ Q =/= 0 /\ ( N - 1 ) e. ZZ ) -> ( Q || ( N - 1 ) <-> ( ( N - 1 ) / Q ) e. ZZ ) )
132 126 130 87 131 syl3anc 
 |-  ( ph -> ( Q || ( N - 1 ) <-> ( ( N - 1 ) / Q ) e. ZZ ) )
133 129 132 mpbid 
 |-  ( ph -> ( ( N - 1 ) / Q ) e. ZZ )
134 52 nn0ge0d 
 |-  ( ph -> 0 <_ ( N - 1 ) )
135 51 nnred 
 |-  ( ph -> ( N - 1 ) e. RR )
136 13 nnred 
 |-  ( ph -> Q e. RR )
137 13 nngt0d 
 |-  ( ph -> 0 < Q )
138 ge0div 
 |-  ( ( ( N - 1 ) e. RR /\ Q e. RR /\ 0 < Q ) -> ( 0 <_ ( N - 1 ) <-> 0 <_ ( ( N - 1 ) / Q ) ) )
139 135 136 137 138 syl3anc 
 |-  ( ph -> ( 0 <_ ( N - 1 ) <-> 0 <_ ( ( N - 1 ) / Q ) ) )
140 134 139 mpbid 
 |-  ( ph -> 0 <_ ( ( N - 1 ) / Q ) )
141 elnn0z 
 |-  ( ( ( N - 1 ) / Q ) e. NN0 <-> ( ( ( N - 1 ) / Q ) e. ZZ /\ 0 <_ ( ( N - 1 ) / Q ) ) )
142 133 140 141 sylanbrc 
 |-  ( ph -> ( ( N - 1 ) / Q ) e. NN0 )
143 zexpcl 
 |-  ( ( C e. ZZ /\ ( ( N - 1 ) / Q ) e. NN0 ) -> ( C ^ ( ( N - 1 ) / Q ) ) e. ZZ )
144 9 142 143 syl2anc 
 |-  ( ph -> ( C ^ ( ( N - 1 ) / Q ) ) e. ZZ )
145 peano2zm 
 |-  ( ( C ^ ( ( N - 1 ) / Q ) ) e. ZZ -> ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) e. ZZ )
146 144 145 syl 
 |-  ( ph -> ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) e. ZZ )
147 dvdsgcd 
 |-  ( ( P e. ZZ /\ ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) e. ZZ /\ N e. ZZ ) -> ( ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) /\ P || N ) -> P || ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) ) )
148 19 146 37 147 syl3anc 
 |-  ( ph -> ( ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) /\ P || N ) -> P || ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) ) )
149 6 148 mpan2d 
 |-  ( ph -> ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) -> P || ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) ) )
150 odzdvds 
 |-  ( ( ( P e. NN /\ C e. ZZ /\ ( C gcd P ) = 1 ) /\ ( ( N - 1 ) / Q ) e. NN0 ) -> ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) <-> ( ( odZ ` P ) ` C ) || ( ( N - 1 ) / Q ) ) )
151 18 9 75 142 150 syl31anc 
 |-  ( ph -> ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) <-> ( ( odZ ` P ) ` C ) || ( ( N - 1 ) / Q ) ) )
152 13 nncnd 
 |-  ( ph -> Q e. CC )
153 8 nnzd 
 |-  ( ph -> ( Q pCnt A ) e. ZZ )
154 152 130 153 expm1d 
 |-  ( ph -> ( Q ^ ( ( Q pCnt A ) - 1 ) ) = ( ( Q ^ ( Q pCnt A ) ) / Q ) )
155 154 oveq2d 
 |-  ( ph -> ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) = ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( ( Q ^ ( Q pCnt A ) ) / Q ) ) )
156 135 15 nndivred 
 |-  ( ph -> ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. RR )
157 156 recnd 
 |-  ( ph -> ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. CC )
158 157 121 152 130 divassd 
 |-  ( ph -> ( ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( Q pCnt A ) ) ) / Q ) = ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( ( Q ^ ( Q pCnt A ) ) / Q ) ) )
159 122 oveq1d 
 |-  ( ph -> ( ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( Q pCnt A ) ) ) / Q ) = ( ( N - 1 ) / Q ) )
160 155 158 159 3eqtr2d 
 |-  ( ph -> ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) = ( ( N - 1 ) / Q ) )
161 160 breq2d 
 |-  ( ph -> ( ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) <-> ( ( odZ ` P ) ` C ) || ( ( N - 1 ) / Q ) ) )
162 151 161 bitr4d 
 |-  ( ph -> ( P || ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) <-> ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) ) )
163 11 breq2d 
 |-  ( ph -> ( P || ( ( ( C ^ ( ( N - 1 ) / Q ) ) - 1 ) gcd N ) <-> P || 1 ) )
164 149 162 163 3imtr3d 
 |-  ( ph -> ( ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) -> P || 1 ) )
165 125 164 mtod 
 |-  ( ph -> -. ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) )
166 prmpwdvds 
 |-  ( ( ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) e. ZZ /\ ( ( odZ ` P ) ` C ) e. ZZ ) /\ ( Q e. Prime /\ ( Q pCnt A ) e. NN ) /\ ( ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( Q pCnt A ) ) ) /\ -. ( ( odZ ` P ) ` C ) || ( ( ( N - 1 ) / ( Q ^ ( Q pCnt A ) ) ) x. ( Q ^ ( ( Q pCnt A ) - 1 ) ) ) ) ) -> ( Q ^ ( Q pCnt A ) ) || ( ( odZ ` P ) ` C ) )
167 104 78 7 8 123 165 166 syl222anc 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) || ( ( odZ ` P ) ` C ) )
168 odzphi 
 |-  ( ( P e. NN /\ C e. ZZ /\ ( C gcd P ) = 1 ) -> ( ( odZ ` P ) ` C ) || ( phi ` P ) )
169 18 9 75 168 syl3anc 
 |-  ( ph -> ( ( odZ ` P ) ` C ) || ( phi ` P ) )
170 phiprm 
 |-  ( P e. Prime -> ( phi ` P ) = ( P - 1 ) )
171 5 170 syl 
 |-  ( ph -> ( phi ` P ) = ( P - 1 ) )
172 169 171 breqtrd 
 |-  ( ph -> ( ( odZ ` P ) ` C ) || ( P - 1 ) )
173 16 78 85 167 172 dvdstrd 
 |-  ( ph -> ( Q ^ ( Q pCnt A ) ) || ( P - 1 ) )
174 pcdvdsb 
 |-  ( ( Q e. Prime /\ ( P - 1 ) e. ZZ /\ ( Q pCnt A ) e. NN0 ) -> ( ( Q pCnt A ) <_ ( Q pCnt ( P - 1 ) ) <-> ( Q ^ ( Q pCnt A ) ) || ( P - 1 ) ) )
175 7 85 14 174 syl3anc 
 |-  ( ph -> ( ( Q pCnt A ) <_ ( Q pCnt ( P - 1 ) ) <-> ( Q ^ ( Q pCnt A ) ) || ( P - 1 ) ) )
176 173 175 mpbird 
 |-  ( ph -> ( Q pCnt A ) <_ ( Q pCnt ( P - 1 ) ) )